more

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/Algebra/Module/SnakeLemma.lean

@@ -13,9 +13,9 @@ The snake lemma is proven in `Algebra/Homology/ShortComplex/SnakeLemma.lean` for
 categories, but for definitional equality and universe issues we reprove them here for modules.
 
 ## Main results
-- `SnakeLemma.δ`: The connecting homomorphism guaranteed by the snake lemma.
-- `SnakeLemma.exact_δ_left`: The connecting homomorphism is exact on the right.
-- `SnakeLemma.exact_δ_right`: The connecting homomorphism is exact on the left.
+- `SnakeLemma.δ`: The connecting linear map guaranteed by the snake lemma.
+- `SnakeLemma.exact_δ_left`: The connecting linear map is exact on the right.
+- `SnakeLemma.exact_δ_right`: The connecting linear map is exact on the left.
 
 -/
 

Mathlib/LinearAlgebra/Prod.lean

@@ -1030,7 +1030,7 @@ lemma Submodule.exists_eq_graph {G : Submodule S (H × I)} (hf₁ : Bijective (P
 
 /-- **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 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
+$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,11 +103,11 @@ 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$
+* 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$. -/
@@ -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,7 +240,7 @@ 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
+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]
@@ -250,7 +250,7 @@ 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
+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$. -/
@@ -276,7 +276,7 @@ theorem exists_factorization_of_comp_eq_zero_of_free [Flat R M] {K N : Type u} [
   convert this ⊤ Finite.out
   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) :