ExactSequences.lean

1 import KomorebiVerification.SeedRankOperations
2 
3 /-!
4 # Generator bounds for actual exact sequences
5 
6 The upper bound uses an arbitrary ring and unrestricted modules. Exactness is
7 the literal equality of the image of the first map with the kernel of the
8 second. No splitting, finite-dimensionality, or supplied generating family
9 for the middle module is assumed.
10 -/
11 
12 set_option autoImplicit false
13 set_option linter.unnecessarySimpa false
14 
15 namespace Komorebi.PaperIRelease
16 
17 open Cardinal Set
18 open Komorebi.SeedRankBasics Komorebi.SeedRankOperations
19 
20 universe u
21 
22 variable {A L M N : Type u} [Ring A]
23 variable [AddCommGroup L] [Module A L]
24 variable [AddCommGroup M] [Module A M]
25 variable [AddCommGroup N] [Module A N]
26 
27 /-- Lift generators of the quotient and adjoin images of generators of the
28 kernel. This proves the generator bound for every right exact sequence. -/
29 theorem seedRank_le_add_of_exact
30     (f : L →ₗ[A] M) (g : M →ₗ[A] N)
31     (hexact : LinearMap.range f = LinearMap.ker g)
32     (hg : Function.Surjective g) :
33     seedRank A M ≤ seedRank A L + seedRank A N := by
34   classical
35   obtain ⟨s, hs, hsCard⟩ := exists_generating_set_card_eq_seedRank A L
36   obtain ⟨t, ht, htCard⟩ := exists_generating_set_card_eq_seedRank A N
37   let lift : t → M := fun j ↦ Classical.choose (hg (j : N))
38   have hlift (j : t) : g (lift j) = (j : N) := Classical.choose_spec (hg (j : N))
39   let v : s ⊕ t → M := Sum.elim (fun i ↦ f (i : L)) lift
40   let p : Submodule A M := Submodule.span A (Set.range v)
41   have hfmem (x : L) : f x ∈ p := by
42     have hx : x ∈ Submodule.span A s := by rw [hs]; trivial
43     refine Submodule.span_induction
44       (p := fun x _ ↦ f x ∈ p) ?_ ?_ ?_ ?_ hx
45     · intro x hxs
46       exact Submodule.subset_span ⟨Sum.inl ⟨x, hxs⟩, rfl⟩
47     · simpa using p.zero_mem
48     · intro x y _ _ hx hy
49       simpa using p.add_mem hx hy
50     · intro a x _ hx
51       simpa using p.smul_mem a hx
52   have hmap : p.map g = ⊤ := by
53     apply top_unique
54     rw [← ht]
55     apply Submodule.span_le.mpr
56     intro y hy
57     exact ⟨lift ⟨y, hy⟩,
58       Submodule.subset_span ⟨Sum.inr ⟨y, hy⟩, rfl⟩, hlift ⟨y, hy⟩⟩
59   have hgen : FamilyGenerates A M v := by
60     change p = ⊤
61     apply top_unique
62     intro x _
63     have hx : g x ∈ p.map g := by rw [hmap]; trivial
64     obtain ⟨y, hy, hgy⟩ := hx
65     have hdiff : x - y ∈ LinearMap.range f := by
66       rw [hexact]
67       change g (x - y) = 0
68       rw [map_sub, hgy, sub_self]
69     obtain ⟨z, hz⟩ := hdiff
70     have hdmem : x - y ∈ p := by rw [← hz]; exact hfmem z
71     simpa using p.add_mem hdmem hy
72   have hbound := seedRank_le_mk_of_familyGenerates A M hgen
73   simpa [Cardinal.mk_sum, hsCard, htCard] using hbound
74 
75 /-- Paper I's two cardinal bounds for an actual short exact sequence. The
76 upper bound in fact needs only exactness in the middle and surjectivity. -/
77 theorem shortExact_seedRank_bounds
78     (f : L →ₗ[A] M) (g : M →ₗ[A] N)
79     (_hf : Function.Injective f)
80     (hexact : LinearMap.range f = LinearMap.ker g)
81     (hg : Function.Surjective g) :
82     seedRank A N ≤ seedRank A M ∧
83       seedRank A M ≤ seedRank A L + seedRank A N :=
84   ⟨seedRank_le_of_surjective_semilinear g hg,
85     seedRank_le_add_of_exact f g hexact hg⟩
86 
87 /-- The canonical submodule/quotient exact sequence, without any finiteness
88 restriction on the ring, submodule, or ambient module. -/
89 theorem submodule_quotient_seedRank_bounds (K : Submodule A M) :
90     seedRank A (M ⧸ K) ≤ seedRank A M ∧
91       seedRank A M ≤ seedRank A K + seedRank A (M ⧸ K) :=
92   shortExact_seedRank_bounds K.subtype K.mkQ K.subtype_injective
93     (by rw [K.range_subtype, K.ker_mkQ]) K.mkQ_surjective
94 
95 end Komorebi.PaperIRelease
96 
97 #print axioms Komorebi.PaperIRelease.seedRank_le_add_of_exact
98 #print axioms Komorebi.PaperIRelease.shortExact_seedRank_bounds
99 #print axioms Komorebi.PaperIRelease.submodule_quotient_seedRank_bounds

Back to source controls