From 3b07c2d2579bc1ce2f52ef8e6f16eee256b65381 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri, 2 Feb 2024 22:34:33 +0100 Subject: [PATCH 1/3] chore: Move a few lemmas to Mathlib.Algebra.Module.Submodule.Map --- Mathlib/Algebra/Module/Submodule/Map.lean | 84 ++++++++++++++++++++++- Mathlib/LinearAlgebra/Basic.lean | 76 -------------------- scripts/style-exceptions.txt | 1 - 3 files changed, 83 insertions(+), 78 deletions(-) diff --git a/Mathlib/Algebra/Module/Submodule/Map.lean b/Mathlib/Algebra/Module/Submodule/Map.lean index d789bdf14f14d..23ba66dba1bf1 100644 --- a/Mathlib/Algebra/Module/Submodule/Map.lean +++ b/Mathlib/Algebra/Module/Submodule/Map.lean @@ -26,7 +26,6 @@ submodule, subspace, linear map, pushforward, pullback open Function BigOperators Pointwise Set variable {R : Type*} {R₁ : Type*} {R₂ : Type*} {R₃ : Type*} -variable {S : Type*} variable {M : Type*} {M₁ : Type*} {M₂ : Type*} {M₃ : Type*} namespace Submodule @@ -434,6 +433,11 @@ theorem _root_.LinearMap.iInf_invariant {σ : R →+* R} [RingHomSurjective σ] exact le_iInf fun i => (Submodule.map_mono (iInf_le p i)).trans (this i) #align linear_map.infi_invariant LinearMap.iInf_invariant +theorem disjoint_iff_comap_eq_bot {p q : Submodule R M} : Disjoint p q ↔ comap p.subtype q = ⊥ := by + rw [← (map_injective_of_injective (show Injective p.subtype from Subtype.coe_injective)).eq_iff, + map_comap_subtype, map_bot, disjoint_iff] +#align submodule.disjoint_iff_comap_eq_bot Submodule.disjoint_iff_comap_eq_bot + end AddCommMonoid section AddCommGroup @@ -650,4 +654,82 @@ theorem submoduleMap_coe_apply (f : M →ₗ[R] M₁) {p : Submodule R M} (x : p theorem submoduleMap_surjective (f : M →ₗ[R] M₁) (p : Submodule R M) : Function.Surjective (f.submoduleMap p) := f.toAddMonoidHom.addSubmonoidMap_surjective _ +variable [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {σ₂₁ : R₂ →+* R} + +open Submodule + +theorem map_codRestrict [RingHomSurjective σ₂₁] (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (h p') : + Submodule.map (codRestrict p f h) p' = comap p.subtype (p'.map f) := + Submodule.ext fun ⟨x, hx⟩ => by simp [Subtype.ext_iff_val] +#align linear_map.map_cod_restrict LinearMap.map_codRestrict + +theorem comap_codRestrict (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (hf p') : + Submodule.comap (codRestrict p f hf) p' = Submodule.comap f (map p.subtype p') := + Submodule.ext fun x => ⟨fun h => ⟨⟨_, hf x⟩, h, rfl⟩, by rintro ⟨⟨_, _⟩, h, ⟨⟩⟩; exact h⟩ +#align linear_map.comap_cod_restrict LinearMap.comap_codRestrict + end LinearMap + +/-! ### Linear equivalences -/ + +namespace LinearEquiv + +section AddCommMonoid + +section + +variable [Semiring R] [Semiring R₂] +variable [AddCommMonoid M] [AddCommMonoid M₂] +variable {module_M : Module R M} {module_M₂ : Module R₂ M₂} +variable {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} +variable {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} +variable (e : M ≃ₛₗ[σ₁₂] M₂) + +theorem map_eq_comap {p : Submodule R M} : + (p.map (e : M →ₛₗ[σ₁₂] M₂) : Submodule R₂ M₂) = p.comap (e.symm : M₂ →ₛₗ[σ₂₁] M) := + SetLike.coe_injective <| by simp [e.image_eq_preimage] +#align linear_equiv.map_eq_comap LinearEquiv.map_eq_comap + +/-- A linear equivalence of two modules restricts to a linear equivalence from any submodule +`p` of the domain onto the image of that submodule. + +This is the linear version of `AddEquiv.submonoidMap` and `AddEquiv.subgroupMap`. + +This is `LinearEquiv.ofSubmodule'` but with `map` on the right instead of `comap` on the left. -/ +def submoduleMap (p : Submodule R M) : p ≃ₛₗ[σ₁₂] ↥(p.map (e : M →ₛₗ[σ₁₂] M₂) : Submodule R₂ M₂) := + { ((e : M →ₛₗ[σ₁₂] M₂).domRestrict p).codRestrict (p.map (e : M →ₛₗ[σ₁₂] M₂)) fun x => + ⟨x, by + simp only [LinearMap.domRestrict_apply, eq_self_iff_true, and_true_iff, SetLike.coe_mem, + SetLike.mem_coe]⟩ with + invFun := fun y => + ⟨(e.symm : M₂ →ₛₗ[σ₂₁] M) y, by + rcases y with ⟨y', hy⟩ + rw [Submodule.mem_map] at hy + rcases hy with ⟨x, hx, hxy⟩ + subst hxy + simp only [symm_apply_apply, Submodule.coe_mk, coe_coe, hx]⟩ + left_inv := fun x => by + simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.toFun_eq_coe, + LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, SetLike.eta] + right_inv := fun y => by + apply SetCoe.ext + simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.toFun_eq_coe, + LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply] } +#align linear_equiv.submodule_map LinearEquiv.submoduleMap + +@[simp] +theorem submoduleMap_apply (p : Submodule R M) (x : p) : ↑(e.submoduleMap p x) = e x := + rfl +#align linear_equiv.submodule_map_apply LinearEquiv.submoduleMap_apply + +@[simp] +theorem submoduleMap_symm_apply (p : Submodule R M) + (x : (p.map (e : M →ₛₗ[σ₁₂] M₂) : Submodule R₂ M₂)) : ↑((e.submoduleMap p).symm x) = e.symm x := + rfl +#align linear_equiv.submodule_map_symm_apply LinearEquiv.submoduleMap_symm_apply + +end + +end AddCommMonoid + +end LinearEquiv diff --git a/Mathlib/LinearAlgebra/Basic.lean b/Mathlib/LinearAlgebra/Basic.lean index a71f222da61c9..2f81e97142bd8 100644 --- a/Mathlib/LinearAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/Basic.lean @@ -124,16 +124,6 @@ variable {σ₂₁ : R₂ →+* R} {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ variable [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] -theorem map_codRestrict [RingHomSurjective σ₂₁] (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (h p') : - Submodule.map (codRestrict p f h) p' = comap p.subtype (p'.map f) := - Submodule.ext fun ⟨x, hx⟩ => by simp [Subtype.ext_iff_val] -#align linear_map.map_cod_restrict LinearMap.map_codRestrict - -theorem comap_codRestrict (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (hf p') : - Submodule.comap (codRestrict p f hf) p' = Submodule.comap f (map p.subtype p') := - Submodule.ext fun x => ⟨fun h => ⟨⟨_, hf x⟩, h, rfl⟩, by rintro ⟨⟨_, _⟩, h, ⟨⟩⟩; exact h⟩ -#align linear_map.comap_cod_restrict LinearMap.comap_codRestrict - section variable {F : Type*} [sc : SemilinearMapClass F τ₁₂ M M₂] @@ -664,11 +654,6 @@ theorem map_subtype_range_inclusion {p p' : Submodule R M} (h : p ≤ p') : map p'.subtype (range <| inclusion h) = p := by simp [range_inclusion, map_comap_eq, h] #align submodule.map_subtype_range_of_le Submodule.map_subtype_range_inclusion -theorem disjoint_iff_comap_eq_bot {p q : Submodule R M} : Disjoint p q ↔ comap p.subtype q = ⊥ := by - rw [← (map_injective_of_injective (show Injective p.subtype from Subtype.coe_injective)).eq_iff, - map_comap_subtype, map_bot, disjoint_iff] -#align submodule.disjoint_iff_comap_eq_bot Submodule.disjoint_iff_comap_eq_bot - /-- If `N ⊆ M` then submodules of `N` are the same as submodules of `M` contained in `N` -/ def MapSubtype.relIso : Submodule R p ≃o { p' : Submodule R M // p' ≤ p } where toFun p' := ⟨map p.subtype p', map_subtype_le p _⟩ @@ -846,69 +831,8 @@ instance uniqueOfSubsingleton [Subsingleton R] [Subsingleton R₂] : Unique (M end Subsingleton -section - -variable [Semiring R] [Semiring R₂] [Semiring R₃] [Semiring R₄] - -variable [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] - -variable {module_M : Module R M} {module_M₂ : Module R₂ M₂} - -variable {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} - -variable {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} - -variable (e e' : M ≃ₛₗ[σ₁₂] M₂) - #align linear_equiv.map_sum map_sumₓ -theorem map_eq_comap {p : Submodule R M} : - (p.map (e : M →ₛₗ[σ₁₂] M₂) : Submodule R₂ M₂) = p.comap (e.symm : M₂ →ₛₗ[σ₂₁] M) := - SetLike.coe_injective <| by simp [e.image_eq_preimage] -#align linear_equiv.map_eq_comap LinearEquiv.map_eq_comap - -/-- A linear equivalence of two modules restricts to a linear equivalence from any submodule -`p` of the domain onto the image of that submodule. - -This is the linear version of `AddEquiv.submonoidMap` and `AddEquiv.subgroupMap`. - -This is `LinearEquiv.ofSubmodule'` but with `map` on the right instead of `comap` on the left. -/ -def submoduleMap (p : Submodule R M) : p ≃ₛₗ[σ₁₂] ↥(p.map (e : M →ₛₗ[σ₁₂] M₂) : Submodule R₂ M₂) := - { ((e : M →ₛₗ[σ₁₂] M₂).domRestrict p).codRestrict (p.map (e : M →ₛₗ[σ₁₂] M₂)) fun x => - ⟨x, by - simp only [LinearMap.domRestrict_apply, eq_self_iff_true, and_true_iff, SetLike.coe_mem, - SetLike.mem_coe]⟩ with - invFun := fun y => - ⟨(e.symm : M₂ →ₛₗ[σ₂₁] M) y, by - rcases y with ⟨y', hy⟩ - rw [Submodule.mem_map] at hy - rcases hy with ⟨x, hx, hxy⟩ - subst hxy - simp only [symm_apply_apply, Submodule.coe_mk, coe_coe, hx]⟩ - left_inv := fun x => by - simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.toFun_eq_coe, - LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, SetLike.eta] - right_inv := fun y => by - apply SetCoe.ext - simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.toFun_eq_coe, - LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply] } -#align linear_equiv.submodule_map LinearEquiv.submoduleMap - - -@[simp] -theorem submoduleMap_apply (p : Submodule R M) (x : p) : ↑(e.submoduleMap p x) = e x := - rfl -#align linear_equiv.submodule_map_apply LinearEquiv.submoduleMap_apply - -@[simp] -theorem submoduleMap_symm_apply (p : Submodule R M) - (x : (p.map (e : M →ₛₗ[σ₁₂] M₂) : Submodule R₂ M₂)) : ↑((e.submoduleMap p).symm x) = e.symm x := - rfl -#align linear_equiv.submodule_map_symm_apply LinearEquiv.submoduleMap_symm_apply - - -end - section Uncurry variable [Semiring R] [Semiring R₂] [Semiring R₃] [Semiring R₄] diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt index a09d1d7383c62..0847b130c3ca1 100644 --- a/scripts/style-exceptions.txt +++ b/scripts/style-exceptions.txt @@ -82,7 +82,6 @@ Mathlib/Lean/Exception.lean : line 8 : ERR_MOD : Module docstring missing, or to Mathlib/Lean/Expr/ReplaceRec.lean : line 12 : ERR_MOD : Module docstring missing, or too late Mathlib/Lean/LocalContext.lean : line 8 : ERR_MOD : Module docstring missing, or too late Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean : line 1 : ERR_NUM_LIN : 2100 file contains 1900 lines, try to split it up -Mathlib/LinearAlgebra/Basic.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1522 lines, try to split it up Mathlib/LinearAlgebra/Basis.lean : line 1 : ERR_NUM_LIN : 1800 file contains 1646 lines, try to split it up Mathlib/LinearAlgebra/Dual.lean : line 1 : ERR_NUM_LIN : 2000 file contains 1847 lines, try to split it up Mathlib/LinearAlgebra/LinearIndependent.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1537 lines, try to split it up From f5cbc6210070abfd6e8a5e3a2ece937a486f1100 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri, 2 Feb 2024 22:51:22 +0100 Subject: [PATCH 2/3] chore: Move LinearMap.ker to a new file --- Mathlib.lean | 1 + Mathlib/Algebra/Algebra/Basic.lean | 4 +- .../Algebra/Algebra/NonUnitalSubalgebra.lean | 1 + Mathlib/Algebra/Algebra/Operations.lean | 9 +- Mathlib/Algebra/Algebra/Prod.lean | 1 + Mathlib/Algebra/Category/ModuleCat/Basic.lean | 1 + Mathlib/Algebra/Module/Submodule/Ker.lean | 354 ++++++++++++++++++ Mathlib/Analysis/LocallyConvex/Polar.lean | 1 + .../AffineSpace/AffineEquiv.lean | 1 + Mathlib/LinearAlgebra/Basic.lean | 201 +--------- Mathlib/LinearAlgebra/BilinearMap.lean | 2 +- Mathlib/LinearAlgebra/Dual.lean | 1 + Mathlib/LinearAlgebra/PiTensorProduct.lean | 1 + Mathlib/LinearAlgebra/Prod.lean | 3 +- Mathlib/LinearAlgebra/SesquilinearForm.lean | 4 +- Mathlib/LinearAlgebra/TensorProduct.lean | 3 +- .../LinearAlgebra/TensorProduct/Tower.lean | 3 +- 17 files changed, 379 insertions(+), 212 deletions(-) create mode 100644 Mathlib/Algebra/Module/Submodule/Ker.lean diff --git a/Mathlib.lean b/Mathlib.lean index 71d61dfedcae2..ff5ecf79b45b2 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -335,6 +335,7 @@ import Mathlib.Algebra.Module.Prod import Mathlib.Algebra.Module.Projective import Mathlib.Algebra.Module.Submodule.Basic import Mathlib.Algebra.Module.Submodule.Bilinear +import Mathlib.Algebra.Module.Submodule.Ker import Mathlib.Algebra.Module.Submodule.Lattice import Mathlib.Algebra.Module.Submodule.LinearMap import Mathlib.Algebra.Module.Submodule.Localization diff --git a/Mathlib/Algebra/Algebra/Basic.lean b/Mathlib/Algebra/Algebra/Basic.lean index 143e88e3c091f..e11bf33f2265b 100644 --- a/Mathlib/Algebra/Algebra/Basic.lean +++ b/Mathlib/Algebra/Algebra/Basic.lean @@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kenny Lau, Yury Kudryashov -/ import Mathlib.Algebra.CharZero.Lemmas +import Mathlib.Algebra.Module.Submodule.Ker +import Mathlib.Algebra.Module.Submodule.RestrictScalars import Mathlib.Algebra.Module.ULift -import Mathlib.LinearAlgebra.Basic import Mathlib.RingTheory.Subring.Basic -import Mathlib.Algebra.Module.Submodule.RestrictScalars #align_import algebra.algebra.basic from "leanprover-community/mathlib"@"36b8aa61ea7c05727161f96a0532897bd72aedab" diff --git a/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean b/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean index 2cd81fe6a75e4..08e24876d5800 100644 --- a/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean +++ b/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean @@ -5,6 +5,7 @@ Authors: Jireh Loreaux -/ import Mathlib.Algebra.Algebra.NonUnitalHom import Mathlib.Data.Set.UnionLift +import Mathlib.LinearAlgebra.Basic import Mathlib.LinearAlgebra.Span import Mathlib.RingTheory.NonUnitalSubring.Basic diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean index 16528e9752c06..1979c1270d8af 100644 --- a/Mathlib/Algebra/Algebra/Operations.lean +++ b/Mathlib/Algebra/Algebra/Operations.lean @@ -6,15 +6,16 @@ Authors: Kenny Lau import Mathlib.Algebra.Algebra.Bilinear import Mathlib.Algebra.Algebra.Equiv import Mathlib.Algebra.Algebra.Opposite -import Mathlib.Algebra.Module.Submodule.Pointwise -import Mathlib.Algebra.Module.Submodule.Bilinear +import Mathlib.Algebra.GroupWithZero.NonZeroDivisors import Mathlib.Algebra.Module.Opposites +import Mathlib.Algebra.Module.Submodule.Bilinear +import Mathlib.Algebra.Module.Submodule.Pointwise import Mathlib.Algebra.Order.Kleene import Mathlib.Data.Finset.Pointwise -import Mathlib.Data.Set.Semiring import Mathlib.Data.Set.Pointwise.BigOperators +import Mathlib.Data.Set.Semiring import Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise -import Mathlib.Algebra.GroupWithZero.NonZeroDivisors +import Mathlib.LinearAlgebra.Basic #align_import algebra.algebra.operations from "leanprover-community/mathlib"@"27b54c47c3137250a521aa64e9f1db90be5f6a26" diff --git a/Mathlib/Algebra/Algebra/Prod.lean b/Mathlib/Algebra/Algebra/Prod.lean index 3a4f44aee8065..faeda2cd27075 100644 --- a/Mathlib/Algebra/Algebra/Prod.lean +++ b/Mathlib/Algebra/Algebra/Prod.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kenny Lau, Yury Kudryashov -/ import Mathlib.Algebra.Algebra.Hom +import Mathlib.Algebra.Module.Prod #align_import algebra.algebra.prod from "leanprover-community/mathlib"@"28aa996fc6fb4317f0083c4e6daf79878d81be33" diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index d52cf13c01618..d571ed5bcd3f9 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -7,6 +7,7 @@ import Mathlib.Algebra.Category.GroupCat.Preadditive import Mathlib.CategoryTheory.Conj import Mathlib.CategoryTheory.Linear.Basic import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor +import Mathlib.LinearAlgebra.Basic #align_import algebra.category.Module.basic from "leanprover-community/mathlib"@"829895f162a1f29d0133f4b3538f4cd1fb5bffd3" diff --git a/Mathlib/Algebra/Module/Submodule/Ker.lean b/Mathlib/Algebra/Module/Submodule/Ker.lean new file mode 100644 index 0000000000000..54304d16840c3 --- /dev/null +++ b/Mathlib/Algebra/Module/Submodule/Ker.lean @@ -0,0 +1,354 @@ +/- +Copyright (c) 2017 Johannes Hölzl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov, Frédéric Dupuis, + Heather Macbeth +-/ +import Mathlib.Algebra.Module.Submodule.Map + +#align_import linear_algebra.basic from "leanprover-community/mathlib"@"9d684a893c52e1d6692a504a118bfccbae04feeb" + +/-! +# Kernel of a linear map + +This file defines the kernel of a linear map. + +## Main definitions + +* `LinearMap.ker`: the kernel of a linear map as a submodule of the domain + +## Notations + +* We continue to use the notations `M →ₛₗ[σ] M₂` and `M →ₗ[R] M₂` for the type of semilinear + (resp. linear) maps from `M` to `M₂` over the ring homomorphism `σ` (resp. over the ring `R`). + +## Tags +linear algebra, vector space, module + +-/ + +open Function + +open BigOperators Pointwise + +variable {R : Type*} {R₁ : Type*} {R₂ : Type*} {R₃ : Type*} +variable {K : Type*} +variable {M : Type*} {M₁ : Type*} {M₂ : Type*} {M₃ : Type*} +variable {V : Type*} {V₂ : Type*} + +/-! ### Properties of linear maps -/ + + +namespace LinearMap + +section AddCommMonoid + +variable [Semiring R] [Semiring R₂] [Semiring R₃] +variable [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] +variable {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} +variable [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] +variable [Module R M] [Module R₂ M₂] [Module R₃ M₃] + +open Submodule + +variable {σ₂₁ : R₂ →+* R} {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} + +variable [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] + +variable {F : Type*} [sc : SemilinearMapClass F τ₁₂ M M₂] + +/-- The kernel of a linear map `f : M → M₂` is defined to be `comap f ⊥`. This is equivalent to the +set of `x : M` such that `f x = 0`. The kernel is a submodule of `M`. -/ +def ker (f : F) : Submodule R M := + comap f ⊥ +#align linear_map.ker LinearMap.ker + +@[simp] +theorem mem_ker {f : F} {y} : y ∈ ker f ↔ f y = 0 := + mem_bot R₂ +#align linear_map.mem_ker LinearMap.mem_ker + +@[simp] +theorem ker_id : ker (LinearMap.id : M →ₗ[R] M) = ⊥ := + rfl +#align linear_map.ker_id LinearMap.ker_id + +@[simp] +theorem map_coe_ker (f : F) (x : ker f) : f x = 0 := + mem_ker.1 x.2 +#align linear_map.map_coe_ker LinearMap.map_coe_ker + +theorem ker_toAddSubmonoid (f : M →ₛₗ[τ₁₂] M₂) : f.ker.toAddSubmonoid = (AddMonoidHom.mker f) := + rfl +#align linear_map.ker_to_add_submonoid LinearMap.ker_toAddSubmonoid + +theorem comp_ker_subtype (f : M →ₛₗ[τ₁₂] M₂) : f.comp f.ker.subtype = 0 := + LinearMap.ext fun x => mem_ker.1 x.2 +#align linear_map.comp_ker_subtype LinearMap.comp_ker_subtype + +theorem ker_comp (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) : + ker (g.comp f : M →ₛₗ[τ₁₃] M₃) = comap f (ker g) := + rfl +#align linear_map.ker_comp LinearMap.ker_comp + +theorem ker_le_ker_comp (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) : + ker f ≤ ker (g.comp f : M →ₛₗ[τ₁₃] M₃) := by rw [ker_comp]; exact comap_mono bot_le +#align linear_map.ker_le_ker_comp LinearMap.ker_le_ker_comp + +theorem ker_sup_ker_le_ker_comp_of_commute {f g : M →ₗ[R] M} (h : Commute f g) : + ker f ⊔ ker g ≤ ker (f ∘ₗ g) := by + refine sup_le_iff.mpr ⟨?_, ker_le_ker_comp g f⟩ + rw [← mul_eq_comp, h.eq, mul_eq_comp] + exact ker_le_ker_comp f g + +@[simp] +theorem ker_le_comap {p : Submodule R₂ M₂} (f : M →ₛₗ[τ₁₂] M₂) : + ker f ≤ p.comap f := + fun x hx ↦ by simp [mem_ker.mp hx] + +theorem disjoint_ker {f : F} {p : Submodule R M} : + Disjoint p (ker f) ↔ ∀ x ∈ p, f x = 0 → x = 0 := by + simp [disjoint_def] +#align linear_map.disjoint_ker LinearMap.disjoint_ker + +theorem ker_eq_bot' {f : F} : ker f = ⊥ ↔ ∀ m, f m = 0 → m = 0 := by + simpa [disjoint_iff_inf_le] using disjoint_ker (f := f) (p := ⊤) +#align linear_map.ker_eq_bot' LinearMap.ker_eq_bot' + +theorem ker_eq_bot_of_inverse {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] {f : M →ₛₗ[τ₁₂] M₂} + {g : M₂ →ₛₗ[τ₂₁] M} (h : (g.comp f : M →ₗ[R] M) = id) : ker f = ⊥ := + ker_eq_bot'.2 fun m hm => by rw [← id_apply (R := R) m, ← h, comp_apply, hm, g.map_zero] +#align linear_map.ker_eq_bot_of_inverse LinearMap.ker_eq_bot_of_inverse + +theorem le_ker_iff_map [RingHomSurjective τ₁₂] {f : F} {p : Submodule R M} : + p ≤ ker f ↔ map f p = ⊥ := by rw [ker, eq_bot_iff, map_le_iff_le_comap] +#align linear_map.le_ker_iff_map LinearMap.le_ker_iff_map + +theorem ker_codRestrict {τ₂₁ : R₂ →+* R} (p : Submodule R M) (f : M₂ →ₛₗ[τ₂₁] M) (hf) : + ker (codRestrict p f hf) = ker f := by rw [ker, comap_codRestrict, Submodule.map_bot]; rfl +#align linear_map.ker_cod_restrict LinearMap.ker_codRestrict + +theorem ker_restrict [AddCommMonoid M₁] [Module R M₁] {p : Submodule R M} {q : Submodule R M₁} + {f : M →ₗ[R] M₁} (hf : ∀ x : M, x ∈ p → f x ∈ q) : + ker (f.restrict hf) = LinearMap.ker (f.domRestrict p) := by + rw [restrict_eq_codRestrict_domRestrict, ker_codRestrict] +#align linear_map.ker_restrict LinearMap.ker_restrict + +@[simp] +theorem ker_zero : ker (0 : M →ₛₗ[τ₁₂] M₂) = ⊤ := + eq_top_iff'.2 fun x => by simp +#align linear_map.ker_zero LinearMap.ker_zero + +theorem ker_eq_top {f : M →ₛₗ[τ₁₂] M₂} : ker f = ⊤ ↔ f = 0 := + ⟨fun h => ext fun _ => mem_ker.1 <| h.symm ▸ trivial, fun h => h.symm ▸ ker_zero⟩ +#align linear_map.ker_eq_top LinearMap.ker_eq_top + +@[simp] +theorem _root_.AddMonoidHom.coe_toIntLinearMap_ker {M M₂ : Type*} [AddCommGroup M] [AddCommGroup M₂] + (f : M →+ M₂) : LinearMap.ker f.toIntLinearMap = AddSubgroup.toIntSubmodule f.ker := rfl + +theorem ker_eq_bot_of_injective {f : F} (hf : Injective f) : ker f = ⊥ := by + have : Disjoint ⊤ (ker f) := by + -- Porting note: `← map_zero f` should work here, but it needs to be directly applied to H. + rw [disjoint_ker] + intros _ _ H + rw [← map_zero f] at H + exact hf H + simpa [disjoint_iff_inf_le] +#align linear_map.ker_eq_bot_of_injective LinearMap.ker_eq_bot_of_injective + +/-- The increasing sequence of submodules consisting of the kernels of the iterates of a linear map. +-/ +@[simps] +def iterateKer (f : M →ₗ[R] M) : ℕ →o Submodule R M where + toFun n := ker (f ^ n) + monotone' n m w x h := by + obtain ⟨c, rfl⟩ := le_iff_exists_add.mp w + rw [LinearMap.mem_ker] at h + rw [LinearMap.mem_ker, add_comm, pow_add, LinearMap.mul_apply, h, LinearMap.map_zero] +#align linear_map.iterate_ker LinearMap.iterateKer + +end AddCommMonoid + +section Ring + +variable [Ring R] [Ring R₂] [Ring R₃] +variable [AddCommGroup M] [AddCommGroup M₂] [AddCommGroup M₃] +variable [Module R M] [Module R₂ M₂] [Module R₃ M₃] +variable {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} +variable [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] +variable {F : Type*} [sc : SemilinearMapClass F τ₁₂ M M₂] +variable {f : F} + +open Submodule + +theorem ker_toAddSubgroup (f : M →ₛₗ[τ₁₂] M₂) : (ker f).toAddSubgroup = f.toAddMonoidHom.ker := + rfl +#align linear_map.ker_to_add_subgroup LinearMap.ker_toAddSubgroup + +theorem sub_mem_ker_iff {x y} : x - y ∈ ker f ↔ f x = f y := by rw [mem_ker, map_sub, sub_eq_zero] +#align linear_map.sub_mem_ker_iff LinearMap.sub_mem_ker_iff + +theorem disjoint_ker' {p : Submodule R M} : + Disjoint p (ker f) ↔ ∀ x ∈ p, ∀ y ∈ p, f x = f y → x = y := + disjoint_ker.trans + ⟨fun H x hx y hy h => eq_of_sub_eq_zero <| H _ (sub_mem hx hy) (by simp [h]), + fun H x h₁ h₂ => H x h₁ 0 (zero_mem _) (by simpa using h₂)⟩ +#align linear_map.disjoint_ker' LinearMap.disjoint_ker' + +theorem injOn_of_disjoint_ker {p : Submodule R M} {s : Set M} (h : s ⊆ p) + (hd : Disjoint p (ker f)) : Set.InjOn f s := fun _ hx _ hy => + disjoint_ker'.1 hd _ (h hx) _ (h hy) +#align linear_map.inj_on_of_disjoint_ker LinearMap.injOn_of_disjoint_ker + +variable (F) + +theorem _root_.LinearMapClass.ker_eq_bot : ker f = ⊥ ↔ Injective f := by + simpa [disjoint_iff_inf_le] using disjoint_ker' (f := f) (p := ⊤) +#align linear_map_class.ker_eq_bot LinearMapClass.ker_eq_bot + +variable {F} + +theorem ker_eq_bot {f : M →ₛₗ[τ₁₂] M₂} : ker f = ⊥ ↔ Injective f := + LinearMapClass.ker_eq_bot _ +#align linear_map.ker_eq_bot LinearMap.ker_eq_bot + +@[simp] lemma injective_domRestrict_iff {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} : + Injective (f.domRestrict S) ↔ S ⊓ LinearMap.ker f = ⊥ := by + rw [← LinearMap.ker_eq_bot] + refine ⟨fun h ↦ le_bot_iff.1 ?_, fun h ↦ le_bot_iff.1 ?_⟩ + · intro x ⟨hx, h'x⟩ + have : ⟨x, hx⟩ ∈ LinearMap.ker (LinearMap.domRestrict f S) := by simpa using h'x + rw [h] at this + simpa using this + · rintro ⟨x, hx⟩ h'x + have : x ∈ S ⊓ LinearMap.ker f := ⟨hx, h'x⟩ + rw [h] at this + simpa using this + +@[simp] theorem injective_restrict_iff_disjoint {p : Submodule R M} {f : M →ₗ[R] M} + (hf : ∀ x ∈ p, f x ∈ p) : + Injective (f.restrict hf) ↔ Disjoint p (ker f) := by + rw [← ker_eq_bot, ker_restrict hf, ker_eq_bot, injective_domRestrict_iff, disjoint_iff] + +end Ring + +section Semifield + +variable [Semifield K] +variable [AddCommMonoid V] [Module K V] +variable [AddCommMonoid V₂] [Module K V₂] + +theorem ker_smul (f : V →ₗ[K] V₂) (a : K) (h : a ≠ 0) : ker (a • f) = ker f := + Submodule.comap_smul f _ a h +#align linear_map.ker_smul LinearMap.ker_smul + +theorem ker_smul' (f : V →ₗ[K] V₂) (a : K) : ker (a • f) = ⨅ _ : a ≠ 0, ker f := + Submodule.comap_smul' f _ a +#align linear_map.ker_smul' LinearMap.ker_smul' + +end Semifield + +end LinearMap + +namespace Submodule + +section AddCommMonoid + +variable [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] + +variable [Module R M] [Module R₂ M₂] + +variable (p p' : Submodule R M) (q : Submodule R₂ M₂) + +variable {τ₁₂ : R →+* R₂} + +variable {F : Type*} [sc : SemilinearMapClass F τ₁₂ M M₂] + +open LinearMap + +@[simp] +theorem comap_bot (f : F) : comap f ⊥ = ker f := + rfl +#align submodule.comap_bot Submodule.comap_bot + +@[simp] +theorem ker_subtype : ker p.subtype = ⊥ := + ker_eq_bot_of_injective fun _ _ => Subtype.ext_val +#align submodule.ker_subtype Submodule.ker_subtype + +@[simp] +theorem ker_inclusion (p p' : Submodule R M) (h : p ≤ p') : ker (inclusion h) = ⊥ := by + rw [inclusion, ker_codRestrict, ker_subtype] +#align submodule.ker_of_le Submodule.ker_inclusion + +end AddCommMonoid + +end Submodule + +namespace LinearMap + +section Semiring + +variable [Semiring R] [Semiring R₂] [Semiring R₃] + +variable [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] + +variable [Module R M] [Module R₂ M₂] [Module R₃ M₃] + +variable {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} + +variable [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] + +theorem ker_comp_of_ker_eq_bot (f : M →ₛₗ[τ₁₂] M₂) {g : M₂ →ₛₗ[τ₂₃] M₃} (hg : ker g = ⊥) : + ker (g.comp f : M →ₛₗ[τ₁₃] M₃) = ker f := by rw [ker_comp, hg, Submodule.comap_bot] +#align linear_map.ker_comp_of_ker_eq_bot LinearMap.ker_comp_of_ker_eq_bot + +end Semiring + +end LinearMap + +/-! ### Linear equivalences -/ + + +namespace LinearEquiv + +section AddCommMonoid + +section + +variable [Semiring R] [Semiring R₂] [Semiring R₃] + +variable [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] + +variable {module_M : Module R M} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} + +variable {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} + +variable {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] + +variable {σ₃₂ : R₃ →+* R₂} + +variable {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} + +variable {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} + +variable (e : M ≃ₛₗ[σ₁₂] M₂) (e'' : M₂ ≃ₛₗ[σ₂₃] M₃) + +@[simp] +protected theorem ker : LinearMap.ker (e : M →ₛₗ[σ₁₂] M₂) = ⊥ := + LinearMap.ker_eq_bot_of_injective e.toEquiv.injective +#align linear_equiv.ker LinearEquiv.ker + +@[simp] +theorem ker_comp (l : M →ₛₗ[σ₁₂] M₂) : + LinearMap.ker (((e'' : M₂ →ₛₗ[σ₂₃] M₃).comp l : M →ₛₗ[σ₁₃] M₃) : M →ₛₗ[σ₁₃] M₃) = + LinearMap.ker l := + LinearMap.ker_comp_of_ker_eq_bot _ e''.ker +#align linear_equiv.ker_comp LinearEquiv.ker_comp + +end + +end AddCommMonoid + +end LinearEquiv diff --git a/Mathlib/Analysis/LocallyConvex/Polar.lean b/Mathlib/Analysis/LocallyConvex/Polar.lean index 30d81e5d2b425..ddd96a4e6a220 100644 --- a/Mathlib/Analysis/LocallyConvex/Polar.lean +++ b/Mathlib/Analysis/LocallyConvex/Polar.lean @@ -3,6 +3,7 @@ Copyright (c) 2022 Moritz Doll. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Doll, Kalle Kytölä -/ +import Mathlib.Algebra.EuclideanDomain.Instances import Mathlib.Analysis.Normed.Field.Basic import Mathlib.LinearAlgebra.SesquilinearForm import Mathlib.Topology.Algebra.Module.WeakDual diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean index 00953128451cb..532e5ce361555 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury G. Kudryashov -/ import Mathlib.LinearAlgebra.AffineSpace.AffineMap +import Mathlib.LinearAlgebra.Basic import Mathlib.LinearAlgebra.GeneralLinearGroup #align_import linear_algebra.affine_space.affine_equiv from "leanprover-community/mathlib"@"bd1fc183335ea95a9519a1630bcf901fe9326d83" diff --git a/Mathlib/LinearAlgebra/Basic.lean b/Mathlib/LinearAlgebra/Basic.lean index 2f81e97142bd8..88d196704baa7 100644 --- a/Mathlib/LinearAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/Basic.lean @@ -6,7 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov, Fréd -/ import Mathlib.Algebra.Module.Hom import Mathlib.Algebra.Module.Prod -import Mathlib.Algebra.Module.Submodule.Map +import Mathlib.Algebra.Module.Submodule.Ker import Mathlib.Data.Set.Finite import Mathlib.Order.ConditionallyCompleteLattice.Basic @@ -277,89 +277,12 @@ instance fintypeRange [Fintype M] [DecidableEq M₂] [RingHomSurjective τ₁₂ variable {F : Type*} [sc : SemilinearMapClass F τ₁₂ M M₂] -/-- The kernel of a linear map `f : M → M₂` is defined to be `comap f ⊥`. This is equivalent to the -set of `x : M` such that `f x = 0`. The kernel is a submodule of `M`. -/ -def ker (f : F) : Submodule R M := - comap f ⊥ -#align linear_map.ker LinearMap.ker - -@[simp] -theorem mem_ker {f : F} {y} : y ∈ ker f ↔ f y = 0 := - mem_bot R₂ -#align linear_map.mem_ker LinearMap.mem_ker - -@[simp] -theorem ker_id : ker (LinearMap.id : M →ₗ[R] M) = ⊥ := - rfl -#align linear_map.ker_id LinearMap.ker_id - -@[simp] -theorem map_coe_ker (f : F) (x : ker f) : f x = 0 := - mem_ker.1 x.2 -#align linear_map.map_coe_ker LinearMap.map_coe_ker - -theorem ker_toAddSubmonoid (f : M →ₛₗ[τ₁₂] M₂) : f.ker.toAddSubmonoid = (AddMonoidHom.mker f) := - rfl -#align linear_map.ker_to_add_submonoid LinearMap.ker_toAddSubmonoid - -theorem comp_ker_subtype (f : M →ₛₗ[τ₁₂] M₂) : f.comp f.ker.subtype = 0 := - LinearMap.ext fun x => mem_ker.1 x.2 -#align linear_map.comp_ker_subtype LinearMap.comp_ker_subtype - -theorem ker_comp (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) : - ker (g.comp f : M →ₛₗ[τ₁₃] M₃) = comap f (ker g) := - rfl -#align linear_map.ker_comp LinearMap.ker_comp - -theorem ker_le_ker_comp (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) : - ker f ≤ ker (g.comp f : M →ₛₗ[τ₁₃] M₃) := by rw [ker_comp]; exact comap_mono bot_le -#align linear_map.ker_le_ker_comp LinearMap.ker_le_ker_comp - -theorem ker_sup_ker_le_ker_comp_of_commute {f g : M →ₗ[R] M} (h : Commute f g) : - ker f ⊔ ker g ≤ ker (f ∘ₗ g) := by - refine sup_le_iff.mpr ⟨?_, ker_le_ker_comp g f⟩ - rw [← mul_eq_comp, h.eq, mul_eq_comp] - exact ker_le_ker_comp f g - -@[simp] -theorem ker_le_comap {p : Submodule R₂ M₂} (f : M →ₛₗ[τ₁₂] M₂) : - ker f ≤ p.comap f := - fun x hx ↦ by simp [mem_ker.mp hx] - -theorem disjoint_ker {f : F} {p : Submodule R M} : - Disjoint p (ker f) ↔ ∀ x ∈ p, f x = 0 → x = 0 := by - simp [disjoint_def] -#align linear_map.disjoint_ker LinearMap.disjoint_ker - -theorem ker_eq_bot' {f : F} : ker f = ⊥ ↔ ∀ m, f m = 0 → m = 0 := by - simpa [disjoint_iff_inf_le] using disjoint_ker (f := f) (p := ⊤) -#align linear_map.ker_eq_bot' LinearMap.ker_eq_bot' - -theorem ker_eq_bot_of_inverse {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] {f : M →ₛₗ[τ₁₂] M₂} - {g : M₂ →ₛₗ[τ₂₁] M} (h : (g.comp f : M →ₗ[R] M) = id) : ker f = ⊥ := - ker_eq_bot'.2 fun m hm => by rw [← id_apply (R := R) m, ← h, comp_apply, hm, g.map_zero] -#align linear_map.ker_eq_bot_of_inverse LinearMap.ker_eq_bot_of_inverse - -theorem le_ker_iff_map [RingHomSurjective τ₁₂] {f : F} {p : Submodule R M} : - p ≤ ker f ↔ map f p = ⊥ := by rw [ker, eq_bot_iff, map_le_iff_le_comap] -#align linear_map.le_ker_iff_map LinearMap.le_ker_iff_map - -theorem ker_codRestrict {τ₂₁ : R₂ →+* R} (p : Submodule R M) (f : M₂ →ₛₗ[τ₂₁] M) (hf) : - ker (codRestrict p f hf) = ker f := by rw [ker, comap_codRestrict, Submodule.map_bot]; rfl -#align linear_map.ker_cod_restrict LinearMap.ker_codRestrict - theorem range_codRestrict {τ₂₁ : R₂ →+* R} [RingHomSurjective τ₂₁] (p : Submodule R M) (f : M₂ →ₛₗ[τ₂₁] M) (hf) : range (codRestrict p f hf) = comap p.subtype (LinearMap.range f) := by simpa only [range_eq_map] using map_codRestrict _ _ _ _ #align linear_map.range_cod_restrict LinearMap.range_codRestrict -theorem ker_restrict [AddCommMonoid M₁] [Module R M₁] {p : Submodule R M} {q : Submodule R M₁} - {f : M →ₗ[R] M₁} (hf : ∀ x : M, x ∈ p → f x ∈ q) : - ker (f.restrict hf) = LinearMap.ker (f.domRestrict p) := by - rw [restrict_eq_codRestrict_domRestrict, ker_codRestrict] -#align linear_map.ker_restrict LinearMap.ker_restrict - theorem _root_.Submodule.map_comap_eq [RingHomSurjective τ₁₂] (f : F) (q : Submodule R₂ M₂) : map f (comap f q) = range f ⊓ q := le_antisymm (le_inf map_le_range (map_comap_le _ _)) <| by @@ -370,24 +293,11 @@ theorem _root_.Submodule.map_comap_eq_self [RingHomSurjective τ₁₂] {f : F} (h : q ≤ range f) : map f (comap f q) = q := by rwa [Submodule.map_comap_eq, inf_eq_right] #align submodule.map_comap_eq_self Submodule.map_comap_eq_self -@[simp] -theorem ker_zero : ker (0 : M →ₛₗ[τ₁₂] M₂) = ⊤ := - eq_top_iff'.2 fun x => by simp -#align linear_map.ker_zero LinearMap.ker_zero - @[simp] theorem range_zero [RingHomSurjective τ₁₂] : range (0 : M →ₛₗ[τ₁₂] M₂) = ⊥ := by simpa only [range_eq_map] using Submodule.map_zero _ #align linear_map.range_zero LinearMap.range_zero -theorem ker_eq_top {f : M →ₛₗ[τ₁₂] M₂} : ker f = ⊤ ↔ f = 0 := - ⟨fun h => ext fun _ => mem_ker.1 <| h.symm ▸ trivial, fun h => h.symm ▸ ker_zero⟩ -#align linear_map.ker_eq_top LinearMap.ker_eq_top - -@[simp] -theorem _root_.AddMonoidHom.coe_toIntLinearMap_ker {M M₂ : Type*} [AddCommGroup M] [AddCommGroup M₂] - (f : M →+ M₂) : LinearMap.ker f.toIntLinearMap = AddSubgroup.toIntSubmodule f.ker := rfl - section variable [RingHomSurjective τ₁₂] @@ -416,27 +326,6 @@ theorem comap_injective {f : F} (hf : range f = ⊤) : Injective (comap f) := fu end -theorem ker_eq_bot_of_injective {f : F} (hf : Injective f) : ker f = ⊥ := by - have : Disjoint ⊤ (ker f) := by - -- Porting note: `← map_zero f` should work here, but it needs to be directly applied to H. - rw [disjoint_ker] - intros _ _ H - rw [← map_zero f] at H - exact hf H - simpa [disjoint_iff_inf_le] -#align linear_map.ker_eq_bot_of_injective LinearMap.ker_eq_bot_of_injective - -/-- The increasing sequence of submodules consisting of the kernels of the iterates of a linear map. --/ -@[simps] -def iterateKer (f : M →ₗ[R] M) : ℕ →o Submodule R M where - toFun n := ker (f ^ n) - monotone' n m w x h := by - obtain ⟨c, rfl⟩ := le_iff_exists_add.mp w - rw [LinearMap.mem_ker] at h - rw [LinearMap.mem_ker, add_comm, pow_add, LinearMap.mul_apply, h, LinearMap.map_zero] -#align linear_map.iterate_ker LinearMap.iterateKer - end AddCommMonoid section Ring @@ -456,41 +345,10 @@ theorem range_toAddSubgroup [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁ rfl #align linear_map.range_to_add_subgroup LinearMap.range_toAddSubgroup -theorem ker_toAddSubgroup (f : M →ₛₗ[τ₁₂] M₂) : (ker f).toAddSubgroup = f.toAddMonoidHom.ker := - rfl -#align linear_map.ker_to_add_subgroup LinearMap.ker_toAddSubgroup - theorem eqLocus_eq_ker_sub (f g : M →ₛₗ[τ₁₂] M₂) : eqLocus f g = ker (f - g) := SetLike.ext fun _ => sub_eq_zero.symm #align linear_map.eq_locus_eq_ker_sub LinearMap.eqLocus_eq_ker_sub -theorem sub_mem_ker_iff {x y} : x - y ∈ ker f ↔ f x = f y := by rw [mem_ker, map_sub, sub_eq_zero] -#align linear_map.sub_mem_ker_iff LinearMap.sub_mem_ker_iff - -theorem disjoint_ker' {p : Submodule R M} : - Disjoint p (ker f) ↔ ∀ x ∈ p, ∀ y ∈ p, f x = f y → x = y := - disjoint_ker.trans - ⟨fun H x hx y hy h => eq_of_sub_eq_zero <| H _ (sub_mem hx hy) (by simp [h]), - fun H x h₁ h₂ => H x h₁ 0 (zero_mem _) (by simpa using h₂)⟩ -#align linear_map.disjoint_ker' LinearMap.disjoint_ker' - -theorem injOn_of_disjoint_ker {p : Submodule R M} {s : Set M} (h : s ⊆ p) - (hd : Disjoint p (ker f)) : Set.InjOn f s := fun _ hx _ hy => - disjoint_ker'.1 hd _ (h hx) _ (h hy) -#align linear_map.inj_on_of_disjoint_ker LinearMap.injOn_of_disjoint_ker - -variable (F) - -theorem _root_.LinearMapClass.ker_eq_bot : ker f = ⊥ ↔ Injective f := by - simpa [disjoint_iff_inf_le] using disjoint_ker' (f := f) (p := ⊤) -#align linear_map_class.ker_eq_bot LinearMapClass.ker_eq_bot - -variable {F} - -theorem ker_eq_bot {f : M →ₛₗ[τ₁₂] M₂} : ker f = ⊥ ↔ Injective f := - LinearMapClass.ker_eq_bot _ -#align linear_map.ker_eq_bot LinearMap.ker_eq_bot - theorem ker_le_iff [RingHomSurjective τ₁₂] {p : Submodule R M} : ker f ≤ p ↔ ∃ y ∈ range f, f ⁻¹' {y} ⊆ p := by constructor @@ -512,24 +370,6 @@ theorem ker_le_iff [RingHomSurjective τ₁₂] {p : Submodule R M} : exact p.sub_mem hxz hx' #align linear_map.ker_le_iff LinearMap.ker_le_iff -@[simp] lemma injective_domRestrict_iff {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} : - Injective (f.domRestrict S) ↔ S ⊓ LinearMap.ker f = ⊥ := by - rw [← LinearMap.ker_eq_bot] - refine ⟨fun h ↦ le_bot_iff.1 ?_, fun h ↦ le_bot_iff.1 ?_⟩ - · intro x ⟨hx, h'x⟩ - have : ⟨x, hx⟩ ∈ LinearMap.ker (LinearMap.domRestrict f S) := by simpa using h'x - rw [h] at this - simpa using this - · rintro ⟨x, hx⟩ h'x - have : x ∈ S ⊓ LinearMap.ker f := ⟨hx, h'x⟩ - rw [h] at this - simpa using this - -@[simp] theorem injective_restrict_iff_disjoint {p : Submodule R M} {f : M →ₗ[R] M} - (hf : ∀ x ∈ p, f x ∈ p) : - Injective (f.restrict hf) ↔ Disjoint p (ker f) := by - rw [← ker_eq_bot, ker_restrict hf, ker_eq_bot, injective_domRestrict_iff, disjoint_iff] - end Ring section Semifield @@ -538,14 +378,6 @@ variable [Semifield K] [Semifield K₂] variable [AddCommMonoid V] [Module K V] variable [AddCommMonoid V₂] [Module K V₂] -theorem ker_smul (f : V →ₗ[K] V₂) (a : K) (h : a ≠ 0) : ker (a • f) = ker f := - Submodule.comap_smul f _ a h -#align linear_map.ker_smul LinearMap.ker_smul - -theorem ker_smul' (f : V →ₗ[K] V₂) (a : K) : ker (a • f) = ⨅ _ : a ≠ 0, ker f := - Submodule.comap_smul' f _ a -#align linear_map.ker_smul' LinearMap.ker_smul' - theorem range_smul (f : V →ₗ[K] V₂) (a : K) (h : a ≠ 0) : range (a • f) = range f := by simpa only [range_eq_map] using Submodule.map_smul f _ a h #align linear_map.range_smul LinearMap.range_smul @@ -605,16 +437,6 @@ theorem map_top [RingHomSurjective τ₁₂] (f : F) : map f ⊤ = range f := (range_eq_map f).symm #align submodule.map_top Submodule.map_top -@[simp] -theorem comap_bot (f : F) : comap f ⊥ = ker f := - rfl -#align submodule.comap_bot Submodule.comap_bot - -@[simp] -theorem ker_subtype : ker p.subtype = ⊥ := - ker_eq_bot_of_injective fun _ _ => Subtype.ext_val -#align submodule.ker_subtype Submodule.ker_subtype - @[simp] theorem range_subtype : range p.subtype = p := by simpa using map_comap_subtype p ⊤ #align submodule.range_subtype Submodule.range_subtype @@ -639,11 +461,6 @@ theorem comap_subtype_self : comap p.subtype p = ⊤ := comap_subtype_eq_top.2 le_rfl #align submodule.comap_subtype_self Submodule.comap_subtype_self -@[simp] -theorem ker_inclusion (p p' : Submodule R M) (h : p ≤ p') : ker (inclusion h) = ⊥ := by - rw [inclusion, ker_codRestrict, ker_subtype] -#align submodule.ker_of_le Submodule.ker_inclusion - theorem range_inclusion (p q : Submodule R M) (h : p ≤ q) : range (inclusion h) = comap q.subtype p := by rw [← map_top, inclusion, LinearMap.map_codRestrict, map_top, range_subtype] @@ -711,10 +528,6 @@ theorem range_comp_of_range_eq_top [RingHomSurjective τ₁₂] [RingHomSurjecti range (g.comp f : M →ₛₗ[τ₁₃] M₃) = range g := by rw [range_comp, hf, Submodule.map_top] #align linear_map.range_comp_of_range_eq_top LinearMap.range_comp_of_range_eq_top -theorem ker_comp_of_ker_eq_bot (f : M →ₛₗ[τ₁₂] M₂) {g : M₂ →ₛₗ[τ₂₃] M₃} (hg : ker g = ⊥) : - ker (g.comp f : M →ₛₗ[τ₁₃] M₃) = ker f := by rw [ker_comp, hg, Submodule.comap_bot] -#align linear_map.ker_comp_of_ker_eq_bot LinearMap.ker_comp_of_ker_eq_bot - section Image /-- If `O` is a submodule of `M`, and `Φ : O →ₗ M'` is a linear map, @@ -1018,11 +831,6 @@ theorem eq_bot_of_equiv [Module R₂ M₂] (e : p ≃ₛₗ[σ₁₂] (⊥ : Sub apply Submodule.eq_zero_of_bot_submodule #align linear_equiv.eq_bot_of_equiv LinearEquiv.eq_bot_of_equiv -@[simp] -protected theorem ker : LinearMap.ker (e : M →ₛₗ[σ₁₂] M₂) = ⊥ := - LinearMap.ker_eq_bot_of_injective e.toEquiv.injective -#align linear_equiv.ker LinearEquiv.ker - -- Porting note: `RingHomSurjective σ₁₂` is an unused argument. @[simp] theorem range_comp [RingHomSurjective σ₂₃] [RingHomSurjective σ₁₃] : @@ -1030,13 +838,6 @@ theorem range_comp [RingHomSurjective σ₂₃] [RingHomSurjective σ₁₃] : LinearMap.range_comp_of_range_eq_top _ e.range #align linear_equiv.range_comp LinearEquiv.range_comp -@[simp] -theorem ker_comp (l : M →ₛₗ[σ₁₂] M₂) : - LinearMap.ker (((e'' : M₂ →ₛₗ[σ₂₃] M₃).comp l : M →ₛₗ[σ₁₃] M₃) : M →ₛₗ[σ₁₃] M₃) = - LinearMap.ker l := - LinearMap.ker_comp_of_ker_eq_bot _ e''.ker -#align linear_equiv.ker_comp LinearEquiv.ker_comp - variable {f g} /-- A linear map `f : M →ₗ[R] M₂` with a left-inverse `g : M₂ →ₗ[R] M` defines a linear diff --git a/Mathlib/LinearAlgebra/BilinearMap.lean b/Mathlib/LinearAlgebra/BilinearMap.lean index 3e093669ba797..5b4d41d6e6c3c 100644 --- a/Mathlib/LinearAlgebra/BilinearMap.lean +++ b/Mathlib/LinearAlgebra/BilinearMap.lean @@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kenny Lau, Mario Carneiro -/ -import Mathlib.LinearAlgebra.Basic +import Mathlib.Algebra.Module.Submodule.Ker #align_import linear_algebra.bilinear_map from "leanprover-community/mathlib"@"87c54600fe3cdc7d32ff5b50873ac724d86aef8d" diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index 64e9f8b42f429..4f468267f1fa8 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -3,6 +3,7 @@ Copyright (c) 2019 Johan Commelin. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johan Commelin, Fabian Glöckle, Kyle Miller -/ +import Mathlib.Algebra.EuclideanDomain.Instances import Mathlib.LinearAlgebra.FiniteDimensional import Mathlib.LinearAlgebra.FreeModule.Finite.Basic import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 532555aaea288..0dec17c686450 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Frédéric Dupuis, Eric Wieser -/ import Mathlib.GroupTheory.Congruence +import Mathlib.LinearAlgebra.Basic import Mathlib.LinearAlgebra.Multilinear.TensorProduct import Mathlib.Tactic.LibrarySearch diff --git a/Mathlib/LinearAlgebra/Prod.lean b/Mathlib/LinearAlgebra/Prod.lean index 755767fb22164..dfe20d9794c1e 100644 --- a/Mathlib/LinearAlgebra/Prod.lean +++ b/Mathlib/LinearAlgebra/Prod.lean @@ -3,9 +3,10 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov, Eric Wieser -/ +import Mathlib.Algebra.Algebra.Prod +import Mathlib.LinearAlgebra.Basic import Mathlib.LinearAlgebra.Span import Mathlib.Order.PartialSups -import Mathlib.Algebra.Algebra.Prod #align_import linear_algebra.prod from "leanprover-community/mathlib"@"cd391184c85986113f8c00844cfe6dda1d34be3d" diff --git a/Mathlib/LinearAlgebra/SesquilinearForm.lean b/Mathlib/LinearAlgebra/SesquilinearForm.lean index 10bb7b1cc876d..6970c41099f8d 100644 --- a/Mathlib/LinearAlgebra/SesquilinearForm.lean +++ b/Mathlib/LinearAlgebra/SesquilinearForm.lean @@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Andreas Swerdlow -/ import Mathlib.Algebra.Module.LinearMap.Basic -import Mathlib.LinearAlgebra.BilinearMap -import Mathlib.Algebra.EuclideanDomain.Instances +import Mathlib.LinearAlgebra.Basic import Mathlib.LinearAlgebra.Basis +import Mathlib.LinearAlgebra.BilinearMap #align_import linear_algebra.sesquilinear_form from "leanprover-community/mathlib"@"87c54600fe3cdc7d32ff5b50873ac724d86aef8d" diff --git a/Mathlib/LinearAlgebra/TensorProduct.lean b/Mathlib/LinearAlgebra/TensorProduct.lean index 43a1fe66f230f..92501b49cf719 100644 --- a/Mathlib/LinearAlgebra/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/TensorProduct.lean @@ -3,8 +3,9 @@ Copyright (c) 2018 Kenny Lau. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kenny Lau, Mario Carneiro -/ -import Mathlib.GroupTheory.Congruence import Mathlib.Algebra.Module.Submodule.Bilinear +import Mathlib.GroupTheory.Congruence +import Mathlib.LinearAlgebra.Basic import Mathlib.Tactic.SuppressCompilation #align_import linear_algebra.tensor_product from "leanprover-community/mathlib"@"88fcdc3da43943f5b01925deddaa5bf0c0e85e4e" diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean index ae9f00a43179d..ab582c4ca3214 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean @@ -3,8 +3,9 @@ Copyright (c) 2020 Scott Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison, Johan Commelin, Eric Wieser -/ -import Mathlib.LinearAlgebra.TensorProduct import Mathlib.Algebra.Algebra.Tower +import Mathlib.LinearAlgebra.Basic +import Mathlib.LinearAlgebra.TensorProduct #align_import ring_theory.tensor_product from "leanprover-community/mathlib"@"88fcdc3da43943f5b01925deddaa5bf0c0e85e4e" From 5ea1547f42c0d89c40343d97e01fcfd4190fa255 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue, 13 Feb 2024 16:49:51 +0100 Subject: [PATCH 3/3] fix --- Mathlib/Algebra/Module/Submodule/Ker.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Module/Submodule/Ker.lean b/Mathlib/Algebra/Module/Submodule/Ker.lean index 54304d16840c3..c09c2bef696d1 100644 --- a/Mathlib/Algebra/Module/Submodule/Ker.lean +++ b/Mathlib/Algebra/Module/Submodule/Ker.lean @@ -55,7 +55,7 @@ variable {σ₂₁ : R₂ →+* R} {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ variable [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] -variable {F : Type*} [sc : SemilinearMapClass F τ₁₂ M M₂] +variable {F : Type*} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] /-- The kernel of a linear map `f : M → M₂` is defined to be `comap f ⊥`. This is equivalent to the set of `x : M` such that `f x = 0`. The kernel is a submodule of `M`. -/ @@ -177,7 +177,7 @@ variable [AddCommGroup M] [AddCommGroup M₂] [AddCommGroup M₃] variable [Module R M] [Module R₂ M₂] [Module R₃ M₃] variable {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} variable [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] -variable {F : Type*} [sc : SemilinearMapClass F τ₁₂ M M₂] +variable {F : Type*} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] variable {f : F} open Submodule @@ -263,7 +263,7 @@ variable (p p' : Submodule R M) (q : Submodule R₂ M₂) variable {τ₁₂ : R →+* R₂} -variable {F : Type*} [sc : SemilinearMapClass F τ₁₂ M M₂] +variable {F : Type*} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] open LinearMap