doc: change "module homomorphism" to "linear map" (#20481)

We change all occurrences of "module homomorphism" in docstrings to "linear map". See here: #20452 (comment)



Co-authored-by: Mitchell Lee <[email protected]>

Mathlib/Algebra/DirectSum/Algebra.lean

@@ -129,7 +129,7 @@ theorem algHom_ext' ⦃f g : (⨁ i, A i) →ₐ[R] B⦄
 theorem algHom_ext ⦃f g : (⨁ i, A i) →ₐ[R] B⦄ (h : ∀ i x, f (of A i x) = g (of A i x)) : f = g :=
   algHom_ext' R A fun i => LinearMap.ext <| h i
 
-/-- The piecewise multiplication from the `Mul` instance, as a bundled linear homomorphism.
+/-- The piecewise multiplication from the `Mul` instance, as a bundled linear map.
 
 This is the graded version of `LinearMap.mul`, and the linear version of `DirectSum.gMulHom` -/
 @[simps]

Mathlib/LinearAlgebra/Prod.lean

@@ -993,7 +993,7 @@ variable {R S G H I : Type*}
   [AddCommMonoid H] [Module S H]
   [AddCommMonoid I] [Module S I]
 
-/-- **Vertical line test** for module homomorphisms.
+/-- **Vertical line test** for linear maps.
 
 Let `f : G → H × I` be a linear (or semilinear) map to a product. Assume that `f` is surjective on
 the first factor and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` at
@@ -1019,18 +1019,18 @@ lemma LinearMap.exists_range_eq_graph {f : G →ₛₗ[σ] H × I} (hf₁ : Surj
   simpa only [mem_range, Eq.comm, ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, mem_graph_iff,
     coe_mk, AddHom.coe_mk, AddMonoidHom.coe_coe, Set.mem_range] using hf' x
 
-/-- **Vertical line test** for module homomorphisms.
+/-- **Vertical line test** for linear maps.
 
 Let `G ≤ H × I` be a submodule of a product of modules. Assume that `G` maps bijectively to the
-first factor. Then `G` is the graph of some module homomorphism `f : H →ₗ[R] I`. -/
+first factor. Then `G` is the graph of some linear map `f : H →ₗ[R] I`. -/
 lemma Submodule.exists_eq_graph {G : Submodule S (H × I)} (hf₁ : Bijective (Prod.fst ∘ G.subtype)) :
     ∃ f : H →ₗ[S] I, G = LinearMap.graph f := by
   simpa only [range_subtype] using LinearMap.exists_range_eq_graph hf₁.surjective
       (fun a b h ↦ congr_arg (Prod.snd ∘ G.subtype) (hf₁.injective h))
 
 /-- **Line test** for module isomorphisms.
 
-Let `f : G → H × I` be a homomorphism to a product of modules. Assume that `f` is surjective onto
+Let `f : G → H × I` be a (semi)linear map to a product of modules. Assume that `f` is surjective onto
 both factors and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` and every
 "horizontal line" `{(h, i) | h : H}` at most once. Then the image of `f` is the graph of some
 module isomorphism `f' : H ≃ I`. -/

Mathlib/RingTheory/Flat/EquationalCriterion.lean

@@ -25,9 +25,9 @@ The equational criterion for flatness can be stated in the following form
 (`Module.Flat.iff_forall_exists_factorization`). Let $M$ be an $R$-module. Then the following two
 conditions are equivalent:
 * $M$ is flat.
-* For all finite index types $\iota$, all elements $f \in R^{\iota}$, and all homomorphisms
+* For all finite index types $\iota$, all elements $f \in R^{\iota}$, and all linear maps
 $x \colon R^{\iota} \to M$ such that $x(f) = 0$, there exist a finite index type $\kappa$ and module
-homomorphisms $a \colon R^{\iota} \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such
+linear maps $a \colon R^{\iota} \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such
 that $x = y \circ a$ and $a(f) = 0$.
 
 Of course, the module $R^\iota$ in this statement can be replaced by an arbitrary free module
@@ -36,12 +36,12 @@ Of course, the module $R^\iota$ in this statement can be replaced by an arbitrar
 We also have the following strengthening of the equational criterion for flatness
 (`Module.Flat.exists_factorization_of_comp_eq_zero_of_free`): Let $M$ be a
 flat module. Let $K$ and $N$ be finite $R$-modules with $N$ free, and let $f \colon K \to N$ and
-$x \colon N \to M$ be homomorphisms such that $x \circ f = 0$. Then there exist a finite index type
-$\kappa$ and module homomorphisms $a \colon N \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such
+$x \colon N \to M$ be linear maps such that $x \circ f = 0$. Then there exist a finite index type
+$\kappa$ and $R$-linear maps $a \colon N \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such
 that $x = y \circ a$ and $a \circ f = 0$. We recover the usual equational criterion for flatness if
 $K = R$ and $N = R^\iota$. This is used in the proof of Lazard's theorem.
 
-We conclude that every homomorphism from a finitely presented module to a flat module factors
+We conclude that every linear map from a finitely presented module to a flat module factors
 through a finite free module (`Module.Flat.exists_factorization_of_isFinitelyPresented`).
 
 ## References
@@ -103,12 +103,12 @@ Let $M$ be a module over a commutative ring $R$. The following are equivalent:
 * For all ideals $I \subseteq R$, the map $I \otimes M \to M$ is injective.
 * Every $\sum_i f_i \otimes x_i$ that vanishes in $R \otimes M$ vanishes trivially.
 * Every relation $\sum_i f_i x_i = 0$ in $M$ is trivial.
-* For all finite index types $\iota$, all elements $f \in R^{\iota}$, and all homomorphisms
+* For all finite index types $\iota$, all elements $f \in R^{\iota}$, and all linear maps
 $x \colon R^{\iota} \to M$ such that $x(f) = 0$, there exist a finite index type $\kappa$ and module
-homomorphisms $a \colon R^{\iota} \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such
+linear maps $a \colon R^{\iota} \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such
 that $x = y \circ a$ and $a(f) = 0$.
-* For all finite free modules $N$, all elements $f \in N$, and all homomorphisms $x \colon N \to M$
-such that $x(f) = 0$, there exist a finite index type $\kappa$ and module homomorphisms
+* For all finite free modules $N$, all elements $f \in N$, and all linear maps $x \colon N \to M$
+such that $x(f) = 0$, there exist a finite index type $\kappa$ and $R$-linear maps
 $a \colon N \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such that $x = y \circ a$ and
 $a(f) = 0$. -/
 theorem tfae_equational_criterion : List.TFAE [
@@ -203,8 +203,8 @@ theorem of_forall_isTrivialRelation (hfx : ∀ {ι : Type u} [Fintype ι] {f : 
 [Stacks 00HK](https://stacks.math.columbia.edu/tag/00HK), alternate form.
 
 A module $M$ is flat if and only if for all finite free modules $R^\iota$,
-all $f \in R^{\iota}$, and all homomorphisms $x \colon R^{\iota} \to M$ such that $x(f) = 0$, there
-exist a finite free module $R^\kappa$ and homomorphisms $a \colon R^{\iota} \to R^{\kappa}$ and
+all $f \in R^{\iota}$, and all linear maps $x \colon R^{\iota} \to M$ such that $x(f) = 0$, there
+exist a finite free module $R^\kappa$ and linear maps $a \colon R^{\iota} \to R^{\kappa}$ and
 $y \colon R^{\kappa} \to M$ such that $x = y \circ a$ and $a(f) = 0$. -/
 theorem iff_forall_exists_factorization : Flat R M ↔
     ∀ {ι : Type u} [Fintype ι] {f : ι →₀ R} {x : (ι →₀ R) →ₗ[R] M}, x f = 0 →
@@ -215,8 +215,8 @@ theorem iff_forall_exists_factorization : Flat R M ↔
 [Stacks 00HK](https://stacks.math.columbia.edu/tag/00HK), forward direction, alternate form.
 
 Let $M$ be a flat module. Let $R^\iota$ be a finite free module, let $f \in R^{\iota}$ be an
-element, and let $x \colon R^{\iota} \to M$ be a homomorphism such that $x(f) = 0$. Then there
-exist a finite free module $R^\kappa$ and homomorphisms $a \colon R^{\iota} \to R^{\kappa}$ and
+element, and let $x \colon R^{\iota} \to M$ be a linear map such that $x(f) = 0$. Then there
+exist a finite free module $R^\kappa$ and linear maps $a \colon R^{\iota} \to R^{\kappa}$ and
 $y \colon R^{\kappa} \to M$ such that $x = y \circ a$ and $a(f) = 0$. -/
 theorem exists_factorization_of_apply_eq_zero [Flat R M] {ι : Type u} [_root_.Finite ι]
     {f : ι →₀ R} {x : (ι →₀ R) →ₗ[R] M} (h : x f = 0) :
@@ -228,8 +228,8 @@ theorem exists_factorization_of_apply_eq_zero [Flat R M] {ι : Type u} [_root_.F
 [Stacks 00HK](https://stacks.math.columbia.edu/tag/00HK), backward direction, alternate form.
 
 Let $M$ be a module over a commutative ring $R$. Suppose that for all finite free modules $R^\iota$,
-all $f \in R^{\iota}$, and all homomorphisms $x \colon R^{\iota} \to M$ such that $x(f) = 0$, there
-exist a finite free module $R^\kappa$ and homomorphisms $a \colon R^{\iota} \to R^{\kappa}$ and
+all $f \in R^{\iota}$, and all linear maps $x \colon R^{\iota} \to M$ such that $x(f) = 0$, there
+exist a finite free module $R^\kappa$ and linear maps $a \colon R^{\iota} \to R^{\kappa}$ and
 $y \colon R^{\kappa} \to M$ such that $x = y \circ a$ and $a(f) = 0$. Then $M$ is flat. -/
 theorem of_forall_exists_factorization (h : ∀ {ι : Type u} [Fintype ι] {f : ι →₀ R}
     {x : (ι →₀ R) →ₗ[R] M}, x f = 0 →
@@ -240,8 +240,8 @@ theorem of_forall_exists_factorization (h : ∀ {ι : Type u} [Fintype ι] {f :
 forward direction, second alternate form.
 
 Let $M$ be a flat module over a commutative ring $R$. Let $N$ be a finite free module over $R$,
-let $f \in N$, and let $x \colon N \to M$ be a homomorphism such that $x(f) = 0$. Then there exist a
-finite index type $\kappa$ and module homomorphisms $a \colon N \to R^{\kappa}$ and
+let $f \in N$, and let $x \colon N \to M$ be a linear map such that $x(f) = 0$. Then there exist a
+finite index type $\kappa$ and $R$-linear maps $a \colon N \to R^{\kappa}$ and
 $y \colon R^{\kappa} \to M$ such that $x = y \circ a$ and $a(f) = 0$. -/
 theorem exists_factorization_of_apply_eq_zero_of_free [Flat R M] {N : Type u} [AddCommGroup N]
     [Module R N] [Free R N] [Module.Finite R N] {f : N} {x : N →ₗ[R] M} (h : x f = 0) :
@@ -250,8 +250,8 @@ theorem exists_factorization_of_apply_eq_zero_of_free [Flat R M] {N : Type u} [A
   exact ((tfae_equational_criterion R M).out 0 5 rfl rfl).mp ‹Flat R M› h
 
 /-- Let $M$ be a flat module. Let $K$ and $N$ be finite $R$-modules with $N$
-free, and let $f \colon K \to N$ and $x \colon N \to M$ be homomorphisms such that
-$x \circ f = 0$. Then there exist a finite index type $\kappa$ and module homomorphisms
+free, and let $f \colon K \to N$ and $x \colon N \to M$ be linear maps such that
+$x \circ f = 0$. Then there exist a finite index type $\kappa$ and $R$-linear maps
 $a \colon N \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such that $x = y \circ a$ and
 $a \circ f = 0$. -/
 theorem exists_factorization_of_comp_eq_zero_of_free [Flat R M] {K N : Type u} [AddCommGroup K]
@@ -276,7 +276,7 @@ theorem exists_factorization_of_comp_eq_zero_of_free [Flat R M] {K N : Type u} [
   convert this ⊤ Finite.fg_top
   simp only [top_le_iff, ker_eq_top]
 
-/-- Every homomorphism from a finitely presented module to a flat module factors through a finite
+/-- Every linear map from a finitely presented module to a flat module factors through a finite
 free module. -/
 theorem exists_factorization_of_isFinitelyPresented [Flat R M] {P : Type u} [AddCommGroup P]
     [Module R P] [FinitePresentation R P] (h₁ : P →ₗ[R] M) :

Mathlib/RingTheory/Flat/FaithfullyFlat.lean

@@ -55,7 +55,7 @@ variable (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M]
 
 /--
 A module `M` over a commutative ring `R` is *faithfully flat* if it is flat and,
-for all `R`-module homomorphism `f : N → N'` such that `id ⊗ f = 0`, we have `f = 0`.
+for all `R`-linear maps `f : N → N'` such that `id ⊗ f = 0`, we have `f = 0`.
 -/
 @[mk_iff] class FaithfullyFlat extends Module.Flat R M : Prop where
   submodule_ne_top : ∀ ⦃m : Ideal R⦄ (_ : Ideal.IsMaximal m), m • (⊤ : Submodule R M) ≠ ⊤

Mathlib/Topology/Germ.lean

@@ -17,7 +17,7 @@ with respect to the neighbourhood filter `𝓝 x`.
 * `Filter.Germ.value φ f`: value associated to the germ `φ` at a point `x`, w.r.t. the
 neighbourhood filter at `x`. This is the common value of all representatives of `φ` at `x`.
 * `Filter.Germ.valueOrderRingHom` and friends: the map `Germ (𝓝 x) E → E` is a
-monoid homomorphism, 𝕜-module homomorphism, ring homomorphism, monotone ring homomorphism
+monoid homomorphism, 𝕜-linear map, ring homomorphism, monotone ring homomorphism
 
 * `RestrictGermPredicate`: given a predicate on germs `P : Π x : X, germ (𝓝 x) Y → Prop` and
 `A : set X`, build a new predicate on germs `restrictGermPredicate P A` such that