From 4c069fa39bcfbd70b35628b4b29c2b0a6eb2dcbd Mon Sep 17 00:00:00 2001 From: Mitchell Lee Date: Mon, 6 Jan 2025 21:02:31 +0000 Subject: [PATCH] doc: change "module homomorphism" to "linear map" (#20481) We change all occurrences of "module homomorphism" in docstrings to "linear map". See here: https://github.com/leanprover-community/mathlib4/pull/20452#issuecomment-2571343604 Co-authored-by: Mitchell Lee <130885647+trivial1711@users.noreply.github.com> --- Mathlib/Algebra/DirectSum/Algebra.lean | 2 +- Mathlib/LinearAlgebra/Prod.lean | 8 ++-- .../RingTheory/Flat/EquationalCriterion.lean | 40 +++++++++---------- Mathlib/RingTheory/Flat/FaithfullyFlat.lean | 2 +- Mathlib/Topology/Germ.lean | 2 +- 5 files changed, 27 insertions(+), 27 deletions(-) diff --git a/Mathlib/Algebra/DirectSum/Algebra.lean b/Mathlib/Algebra/DirectSum/Algebra.lean index 80c5c808cd07ed..5db0ecc0efa46a 100644 --- a/Mathlib/Algebra/DirectSum/Algebra.lean +++ b/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] diff --git a/Mathlib/LinearAlgebra/Prod.lean b/Mathlib/LinearAlgebra/Prod.lean index 328fdca858bd50..560e3f103c1d0b 100644 --- a/Mathlib/LinearAlgebra/Prod.lean +++ b/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,10 +1019,10 @@ 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 @@ -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 (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`. -/ diff --git a/Mathlib/RingTheory/Flat/EquationalCriterion.lean b/Mathlib/RingTheory/Flat/EquationalCriterion.lean index df38f6aa41c23f..ccb3ba16c850ce 100644 --- a/Mathlib/RingTheory/Flat/EquationalCriterion.lean +++ b/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) : diff --git a/Mathlib/RingTheory/Flat/FaithfullyFlat.lean b/Mathlib/RingTheory/Flat/FaithfullyFlat.lean index 39e1cd3c439b7a..600a25333f1bd7 100644 --- a/Mathlib/RingTheory/Flat/FaithfullyFlat.lean +++ b/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) ≠ ⊤ diff --git a/Mathlib/Topology/Germ.lean b/Mathlib/Topology/Germ.lean index 35d47bcfa9b8a6..acee6078395652 100644 --- a/Mathlib/Topology/Germ.lean +++ b/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