Skip to content

Commit

Permalink
chore: golf some proofs introduced in #6360 (#6405)
Browse files Browse the repository at this point in the history 
Notably, getting rid of some injectivity restrictions makes some later proofs simpler.



Co-authored-by: dagurtomas <dagurtomas@gmail.com>
Co-authored-by: Dagur Tómas Ásgeirsson <dagurtomas@gmail.com>
  • Loading branch information
@ADedecker @dagurtomas
ADedecker and dagurtomas committed Aug 15, 2023
1 parent 17a54df commit 280a9f5
Show file tree
Hide file tree
Showing 2 changed files with 50 additions and 99 deletions.
115 changes: 44 additions & 71 deletions Mathlib/Algebra/Category/ModuleCat/Free.lean
View file
Expand Up @@ -37,29 +37,30 @@ namespace ModuleCat

variable {ι ι' R : Type*}[Ring R] {N P : ModuleCat R} {v : ι → N}

open CategoryTheory
open CategoryTheory Submodule Set

section LinearIndependent

variable (hv : LinearIndependent R v) {M : ModuleCat R}
{u : ι ⊕ ι' → M} {f : N ⟶ M} {g : M ⟶ P}
(hw : LinearIndependent R (g ∘ u ∘ Sum.inr)) (hu : Function.Injective u)
variable (hv : LinearIndependent R v) {M : ModuleCat R}
{u : ι ⊕ ι' → M} {f : N ⟶ M} {g : M ⟶ P}
(hw : LinearIndependent R (g ∘ u ∘ Sum.inr))
(hm : Mono f) (he : Exact f g) (huv : u ∘ Sum.inl = f ∘ v)

theorem disjoint_span_sum : Disjoint (Submodule.span R (Set.range (u ∘ Sum.inl)))
(Submodule.span R (Set.range (u ∘ Sum.inr))) := by
rw [huv]
refine' Disjoint.mono_left (Submodule.span_mono (Set.range_comp_subset_range _ _)) _
rw [← LinearMap.range_coe, (Submodule.span_eq (LinearMap.range f)), (exact_iff _ _).mp he]
exact Submodule.ker_range_disjoint (Function.Injective.comp hu Sum.inr_injective) hw
theorem disjoint_span_sum : Disjoint (span R (range (u ∘ Sum.inl)))
(span R (range (u ∘ Sum.inr))) := by
rw [huv, disjoint_comm]
refine' Disjoint.mono_right (span_mono (range_comp_subset_range _ _)) _
rw [← LinearMap.range_coe, (span_eq (LinearMap.range f)), (exact_iff _ _).mp he]
exact range_ker_disjoint hw

/-- In the commutative diagram
```
f g
0 --→ N --→ M --→ P
↑ ↑ ↑
v| u| w|
ι → ι ⊕ ι' ← ι'
```
where the top row is an exact sequence of modules and the maps on the bottom are `Sum.inl` and
`Sum.inr`. If `u` is injective and `v` and `w` are linearly independent, then `u` is linearly
independent. -/
Expand All @@ -68,46 +69,19 @@ theorem linearIndependent_leftExact : LinearIndependent R u :=
⟨(congr_arg (fun f ↦ LinearIndependent R f) huv).mpr
((LinearMap.linearIndependent_iff (f : N →ₗ[R] M)
(LinearMap.ker_eq_bot.mpr ((mono_iff_injective _).mp hm))).mpr hv),
LinearIndependent.of_comp g hw, disjoint_span_sum hw hu he huv⟩

/-- Given a short exact sequence of modules and injective families `v : ι → N` and `w : ι' → P`
f g
0 --→ N --→ M --→ P --→ 0
↑ ↑ ↑
v| | w|
ι ι ⊕ ι' ι'
such that `w` does not hit `0`, the family `Sum.elim (f ∘ v) (g.toFun.invFun ∘ w) : ι ⊕ ι' → M`
is injective. -/
theorem family_injective_shortExact {w : ι' → P} (hse : ShortExact f g)
(hv : v.Injective) (hw : w.Injective) (hw' : ∀ x, w x ≠ 0) :
Function.Injective (Sum.elim (f ∘ v) (g.toFun.invFun ∘ w)) :=
Function.Injective.sum_elim
(Function.Injective.comp ((mono_iff_injective _).mp hse.mono) hv)
(Function.Injective.comp (Function.rightInverse_invFun
((epi_iff_surjective _).mp hse.epi)).injective hw) (fun a b h ↦ by
apply_fun g at h
dsimp at h
rw [Function.rightInverse_invFun ((epi_iff_surjective _).mp hse.epi)] at h
change (f ≫ g) (v a) = _ at h
rw [hse.exact.w] at h
change 0 = _ at h
exact hw' _ h.symm )
LinearIndependent.of_comp g hw, disjoint_span_sum hw he huv⟩

/-- Given a short exact sequence `0 ⟶ N ⟶ M ⟶ P ⟶ 0` of `R`-modules and linearly independent
families `v : ι → N` and `w : ι' → P`, we get a linearly independent family `ι ⊕ ι' → M` -/
theorem linearIndependent_shortExact {w : ι' → P}
(hw : LinearIndependent R w) (hse : ShortExact f g) :
LinearIndependent R (Sum.elim (f ∘ v) (g.toFun.invFun ∘ w)) := by
cases subsingleton_or_nontrivial R
· exact linearIndependent_of_subsingleton
· refine' linearIndependent_leftExact hv _ (family_injective_shortExact hse hv.injective
hw.injective (fun x ↦ hw.ne_zero x)) hse.mono hse.exact _
· simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inr]
rwa [← Function.comp.assoc, Function.RightInverse.comp_eq_id (Function.rightInverse_invFun
((epi_iff_surjective _).mp hse.epi)),
Function.comp.left_id]
· simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inl]
refine' linearIndependent_leftExact hv _ hse.mono hse.exact _
· simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inr]
rwa [← Function.comp.assoc, Function.RightInverse.comp_eq_id (Function.rightInverse_invFun
((epi_iff_surjective _).mp hse.epi)),
Function.comp.left_id]
· simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inl]

end LinearIndependent

Expand All @@ -116,40 +90,41 @@ section Span
variable {M : ModuleCat R} {u : ι⊕ ι' → M} {f : N ⟶ M} {g : M ⟶ P}

/-- In the commutative diagram
```
f g
N --→ M --→ P
↑ ↑ ↑
v| u| w|
ι → ι ⊕ ι' ← ι'
```
where the top row is an exact sequence of modules and the maps on the bottom are `Sum.inl` and
`Sum.inr`. If `v` spans `N` and `w` spans `P`, then `u` spans `M`. -/
theorem span_exact (he : Exact f g) (huv : u ∘ Sum.inl = f ∘ v)
(hv : ⊤ ≤ Submodule.span R (Set.range v))
(hw : ⊤ ≤ Submodule.span R (Set.range (g ∘ u ∘ Sum.inr))) :
⊤ ≤ Submodule.span R (Set.range u) := by
(hv : ⊤ ≤ span R (range v))
(hw : ⊤ ≤ span R (range (g ∘ u ∘ Sum.inr))) :
⊤ ≤ span R (range u) := by
intro m _
have hgm : g m ∈ Submodule.span R (Set.range (g ∘ u ∘ Sum.inr)) := hw Submodule.mem_top
have hgm : g m ∈ span R (range (g ∘ u ∘ Sum.inr)) := hw mem_top
rw [Finsupp.mem_span_range_iff_exists_finsupp] at hgm
obtain ⟨cm, hm⟩ := hgm
let m' : M := Finsupp.sum cm fun j a ↦ a • (u (Sum.inr j))
have hsub : m - m' ∈ LinearMap.range f
· rw [(exact_iff _ _).mp he]
simp only [LinearMap.mem_ker, map_sub, sub_eq_zero]
rw [← hm, map_finsupp_sum]
simp only [Function.comp_apply, map_smul]
simp only [Function.comp_apply, SMulHomClass.map_smul]
obtain ⟨n, hnm⟩ := hsub
have hn : n ∈ Submodule.span R (Set.range v) := hv Submodule.mem_top
have hn : n ∈ span R (range v) := hv mem_top
rw [Finsupp.mem_span_range_iff_exists_finsupp] at hn
obtain ⟨cn, hn⟩ := hn
rw [← hn, map_finsupp_sum] at hnm
rw [← sub_add_cancel m m', ← hnm,]
simp only [map_smul]
simp only [SMulHomClass.map_smul]
have hn' : (Finsupp.sum cn fun a b ↦ b • f (v a)) =
(Finsupp.sum cn fun a b ↦ b • u (Sum.inl a)) :=
by congr; ext a b; change b • (f ∘ v) a = _; rw [← huv]; rfl
rw [hn']
apply Submodule.add_mem
apply add_mem
· rw [Finsupp.mem_span_range_iff_exists_finsupp]
use cn.mapDomain (Sum.inl)
rw [Finsupp.sum_mapDomain_index_inj Sum.inl_injective]
Expand All @@ -159,9 +134,9 @@ theorem span_exact (he : Exact f g) (huv : u ∘ Sum.inl = f ∘ v)

/-- Given an exact sequence `N ⟶ M ⟶ P ⟶ 0` of `R`-modules and spanning
families `v : ι → N` and `w : ι' → P`, we get a spanning family `ι ⊕ ι' → M` -/
theorem span_rightExact {w : ι' → P} (hv : ⊤ ≤ Submodule.span R (Set.range v))
(hw : ⊤ ≤ Submodule.span R (Set.range w)) (hE : Epi g) (he : Exact f g) :
⊤ ≤ Submodule.span R (Set.range (Sum.elim (f ∘ v) (g.toFun.invFun ∘ w))) := by
theorem span_rightExact {w : ι' → P} (hv : ⊤ ≤ span R (range v))
(hw : ⊤ ≤ span R (range w)) (hE : Epi g) (he : Exact f g) :
⊤ ≤ span R (range (Sum.elim (f ∘ v) (g.toFun.invFun ∘ w))) := by
refine' span_exact he _ hv _
· simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inl]
· convert hw
Expand All @@ -172,31 +147,29 @@ theorem span_rightExact {w : ι' → P} (hv : ⊤ ≤ Submodule.span R (Set.rang

end Span

/-- In a short exact sequence `0 ⟶ N ⟶ M ⟶ P ⟶ 0`, given bases for `N` and `P` indexed by `ι` and
`ι'` respectively, we get a basis for `M` indexed by `ι ⊕ ι'`. -/
noncomputable
def Basis.ofShortExact {M : ModuleCat R} {f : N ⟶ M} {g : M ⟶ P} (h : ShortExact f g)
(bN : Basis ι R N) (bP : Basis ι' R P) : Basis (ι ⊕ ι') R M :=
Basis.mk (linearIndependent_shortExact bN.linearIndependent bP.linearIndependent h)
(span_rightExact (le_of_eq (bN.span_eq.symm)) (le_of_eq (bP.span_eq.symm)) h.epi h.exact)

/-- In a short exact sequence `0 ⟶ N ⟶ M ⟶ P ⟶ 0`, if `N` and `P` are free, then `M` is free.-/
theorem free_shortExact {M : ModuleCat R} {f : N ⟶ M}
{g : M ⟶ P} (h : ShortExact f g) [Module.Free R N] [Module.Free R P] :
Module.Free R M :=
Module.Free.of_basis (Basis.mk
(linearIndependent_shortExact
(Module.Free.chooseBasis R N).linearIndependent
(Module.Free.chooseBasis R P).linearIndependent h)
(span_rightExact
(le_of_eq ((Module.Free.chooseBasis R N)).span_eq.symm)
(le_of_eq (Module.Free.chooseBasis R P).span_eq.symm) h.epi h.exact))
Module.Free.of_basis (Basis.ofShortExact h (Module.Free.chooseBasis R N)
(Module.Free.chooseBasis R P))

theorem free_shortExact_rank_add {M : ModuleCat R} {f : N ⟶ M}
{g : M ⟶ P} (h : ShortExact f g) [Module.Free R N] [Module.Free R P] [StrongRankCondition R] :
Module.rank R M = Module.rank R N + Module.rank R P := by
haveI := free_shortExact h
rw [Module.Free.rank_eq_card_chooseBasisIndex, Module.Free.rank_eq_card_chooseBasisIndex R N,
Module.Free.rank_eq_card_chooseBasisIndex R P, Cardinal.add_def, Cardinal.eq]
exact ⟨Basis.indexEquiv (Module.Free.chooseBasis R M) (Basis.mk
(linearIndependent_shortExact
(Module.Free.chooseBasis R N).linearIndependent
(Module.Free.chooseBasis R P).linearIndependent h)
(span_rightExact
(le_of_eq ((Module.Free.chooseBasis R N)).span_eq.symm)
(le_of_eq (Module.Free.chooseBasis R P).span_eq.symm) h.epi h.exact))⟩
exact ⟨Basis.indexEquiv (Module.Free.chooseBasis R M) (Basis.ofShortExact h
(Module.Free.chooseBasis R N) (Module.Free.chooseBasis R P))⟩

theorem free_shortExact_finrank_add {M : ModuleCat R} {f : N ⟶ M}
{g : M ⟶ P} (h : ShortExact f g) [Module.Free R N] [Module.Finite R N]
Expand Down
34 changes: 6 additions & 28 deletions Mathlib/LinearAlgebra/LinearIndependent.lean
View file
Expand Up @@ -222,35 +222,13 @@ theorem LinearIndependent.map (hv : LinearIndependent R v) {f : M →ₗ[R] M'}

/-- If `v` is an injective family of vectors such that `f ∘ v` is linearly independent, then `v`
spans a submodule disjoint from the kernel of `f` -/
theorem Submodule.ker_range_disjoint {f : M →ₗ[R] M'} (hi : v.Injective)
theorem Submodule.range_ker_disjoint {f : M →ₗ[R] M'}
(hv : LinearIndependent R (f ∘ v)) :
Disjoint (LinearMap.ker f) (Submodule.span R (Set.range v)) := by
rw [Submodule.disjoint_def]
intro m hm hmr
simp only [LinearMap.mem_ker] at hm
rw [mem_span_set] at hmr
obtain ⟨c, ⟨hc, hsum⟩⟩ := hmr
rw [← hsum, map_finsupp_sum] at hm
simp_rw [f.map_smul] at hm
dsimp [Finsupp.sum] at hm
rw [linearIndependent_iff'] at hv
specialize hv (Finset.preimage c.support v (Set.injOn_of_injective hi _))
rw [← Finset.sum_preimage v c.support (Set.injOn_of_injective hi _) _ _] at hm
· rw [← hsum]
apply Finset.sum_eq_zero
intro x hx
obtain ⟨y, hy⟩ := hc hx
rw [← hy]
have : c (v y) = 0
· apply hv (c ∘ v) hm y
simp only [Finset.mem_preimage, Function.comp_apply]
dsimp at hy
rwa [hy]
rw [this]
simp only [zero_smul]
· intro x hx hnx
exfalso
exact hnx (hc hx)
Disjoint (span R (range v)) (LinearMap.ker f) := by
rw [LinearIndependent, Finsupp.total_comp, Finsupp.lmapDomain_total R _ f (fun _ ↦ rfl),
LinearMap.ker_comp] at hv
rw [disjoint_iff_inf_le, ← Set.image_univ, Finsupp.span_image_eq_map_total,
map_inf_eq_map_inf_comap, hv, inf_bot_eq, map_bot]

/-- An injective linear map sends linearly independent families of vectors to linearly independent
families of vectors. See also `LinearIndependent.map` for a more general statement. -/
Expand Down

0 comments on commit 280a9f5

Please sign in to comment.