CrowellExactSequence/FiniteFamilyExactness.lean
1import FoxDifferential.Common.FiniteFamilyLinearMap
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CrowellExactSequence/FiniteFamilyExactness.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Finite-family coordinate exactness
15coordinate maps, together with the four-term exact-sequence predicate and transport lemmas
16used by the discrete and profinite Crowell sequences.
17-/
19namespace CrowellExactSequence
21noncomputable section
23open scoped BigOperators
24open FoxDifferential
26section BlanchfieldLyndonFiniteFamilyMap
28variable {R : Type*} [Semiring R]
29variable {M : Type*} [AddCommMonoid M] [Module R M]
30variable {X : Type*} [Fintype X] [DecidableEq X]
32/-- The Blanchfield--Lyndon finite-family map associated to a chosen boundary-generating family. -/
33abbrev blanchfieldLyndonFiniteFamilyMap (generators : X → M) :
34 (X → R) →ₗ[R] M :=
35 finiteFamilyLinearMap (R := R) generators
37omit [DecidableEq X] in
38/-- Evaluate a Blanchfield--Lyndon finite-family map as its defining finite sum. -/
39theorem blanchfieldLyndonFiniteFamilyMap_apply (generators : X → M) (x : X → R) :
40 blanchfieldLyndonFiniteFamilyMap (R := R) generators x = ∑ i, x i • generators i := rfl
42/-- A Blanchfield--Lyndon finite-family map sends a coordinate basis vector to its generator. -/
43@[simp]
44theorem blanchfieldLyndonFiniteFamilyMap_single (generators : X → M) (i : X) :
45 blanchfieldLyndonFiniteFamilyMap (R := R) generators (Pi.single i 1) = generators i :=
46 finiteFamilyLinearMap_single (R := R) generators i
48/-- The image of the Blanchfield--Lyndon finite-family map is the span of its
49boundary-generating family. -/
50theorem blanchfieldLyndonFiniteFamilyMap_range_eq_span (generators : X → M) :
51 LinearMap.range (blanchfieldLyndonFiniteFamilyMap (R := R) generators) =
52 Submodule.span R (Set.range generators) :=
53 finiteFamilyLinearMap_range_eq_span (R := R) generators
55/-- The Blanchfield--Lyndon finite-family map is surjective when its target family spans the
56codomain. -/
58 (generators : X → M)
59 (hspan : Submodule.span R (Set.range generators) = ⊤) :
60 Function.Surjective (blanchfieldLyndonFiniteFamilyMap (R := R) generators) :=
61 finiteFamilyLinearMap_surjective_of_span_eq_top (R := R) generators hspan
63/-- The Blanchfield--Lyndon finite-family map is onto exactly when its boundary generators span. -/
65 (generators : X → M) :
66 Function.Surjective (blanchfieldLyndonFiniteFamilyMap (R := R) generators) ↔
67 Submodule.span R (Set.range generators) = ⊤ :=
68 finiteFamilyLinearMap_surjective_iff_span_eq_top (R := R) generators
70end BlanchfieldLyndonFiniteFamilyMap
72/-- A four-term exact sequence, stated at the function level. This packages the assertions
73`f` injective, exactness at the two middle terms, and surjectivity of the final map. -/
74def IsFourTermExactSequence {A B C D : Type*} [Zero C] [Zero D]
75 (f : A → B) (g : B → C) (h : C → D) : Prop :=
76 Function.Injective f ∧ Function.Exact f g ∧ Function.Exact g h ∧ Function.Surjective h
78/-- Blanchfield--Lyndon coordinate exactness is the same four-term predicate, with a
79paper-facing name for the coordinate form. -/
80abbrev IsBlanchfieldLyndonExactSequence {A B C D : Type*} [Zero C] [Zero D]
81 (f : A → B) (g : B → C) (h : C → D) : Prop :=
82 IsFourTermExactSequence f g h
84namespace IsFourTermExactSequence
86variable {A B C D : Type*} [Zero C] [Zero D]
87variable {f : A → B} {g : B → C} {h : C → D}
89/-- Extract injectivity of the first map from a four-term exact sequence. -/
90theorem injective (hexact : IsFourTermExactSequence f g h) :
91 Function.Injective f :=
92 hexact.1
94/-- Extract exactness at the middle-left map from a four-term exact sequence. -/
95theorem exact_head_tail (hexact : IsFourTermExactSequence f g h) :
96 Function.Exact f g :=
97 hexact.2.1
99/-- Extract exactness at the augmentation-side map from a four-term exact sequence. -/
100theorem exact_tail_augmentation (hexact : IsFourTermExactSequence f g h) :
101 Function.Exact g h :=
102 hexact.2.2.1
104/-- Extract final surjectivity from a four-term exact sequence. -/
105theorem tail_surjective (hexact : IsFourTermExactSequence f g h) :
106 Function.Surjective h :=
107 hexact.2.2.2
111namespace IsBlanchfieldLyndonExactSequence
113variable {A B C D : Type*} [Zero C] [Zero D]
114variable {f : A → B} {g : B → C} {h : C → D}
116/-- Extract injectivity of the first map from a BL exact sequence. -/
117theorem injective (hexact : IsBlanchfieldLyndonExactSequence f g h) :
118 Function.Injective f :=
119 hexact.1
121/-- Extract exactness at the middle-left map from a BL exact sequence. -/
122theorem exact_head_tail (hexact : IsBlanchfieldLyndonExactSequence f g h) :
123 Function.Exact f g :=
124 hexact.2.1
126/-- Extract exactness at the augmentation-side map from a BL exact sequence. -/
127theorem exact_tail_augmentation (hexact : IsBlanchfieldLyndonExactSequence f g h) :
128 Function.Exact g h :=
129 hexact.2.2.1
131/-- Extract augmentation surjectivity from a BL exact sequence. -/
132theorem augmentation_surjective (hexact : IsBlanchfieldLyndonExactSequence f g h) :
133 Function.Surjective h :=
134 hexact.2.2.2
138section LinearEquivTransport
140variable {R : Type*} [Semiring R]
141variable {A B B' C D : Type*}
142variable [AddCommMonoid B] [Module R B]
143variable [AddCommMonoid B'] [Module R B']
144variable [Zero C] [Zero D]
146/-- Transport function exactness across a linear equivalence on the middle type. -/
148 (e : B ≃ₗ[R] B') {f : A → B'} {g : B' → C}
149 (hexact : Function.Exact f g) :
150 Function.Exact (fun x : A => e.symm (f x)) (fun y : B => g (e y)) := by
151 intro y
152 constructor
153 · intro hy
154 rcases (hexact (e y)).1 hy with ⟨x, hx⟩
155 exact ⟨x, by simp only [hx, LinearEquiv.symm_apply_apply]⟩
156 · rintro ⟨x, hx⟩
157 have hxy : f x = e y := by
158 have hcongr := congrArg e hx
159 simpa using hcongr
160 exact (hexact (e y)).2 ⟨x, hxy⟩
162/-- Transporting exactness across a linear equivalence is an equivalence of exactness statements. -/
164 (e : B ≃ₗ[R] B') {f : A → B'} {g : B' → C} :
165 Function.Exact (fun x : A => e.symm (f x)) (fun y : B => g (e y)) ↔
166 Function.Exact f g := by
167 constructor
168 · intro hexact
169 simpa using
171 (e := e.symm)
172 (f := fun x : A => e.symm (f x))
173 (g := fun y : B => g (e y))
174 hexact)
175 · exact Function.Exact.linearEquiv_symm_comp_comp e
177omit [Zero C] in
178/-- Compose the tail map of an exact pair with a linear equivalence on the middle type. -/
180 (e : B ≃ₗ[R] B') {g : B' → C} {h : C → D}
181 (hexact : Function.Exact g h) :
182 Function.Exact (fun y : B => g (e y)) h := by
183 intro z
184 constructor
185 · intro hz
186 rcases (hexact z).1 hz with ⟨y', hy'⟩
187 rcases e.surjective y' with ⟨y, rfl⟩
188 exact ⟨y, hy'⟩
189 · rintro ⟨y, hy⟩
190 exact (hexact z).2 ⟨e y, hy⟩
192/-- Transport a full BL exact sequence across a linear equivalence on the coordinate middle term. -/
194 (e : B ≃ₗ[R] B') {f : A → B'} {g : B' → C} {h : C → D}
195 (hexact : IsBlanchfieldLyndonExactSequence f g h) :
197 (fun x : A => e.symm (f x)) (fun y : B => g (e y)) h := by
198 refine ⟨?_, ?_, ?_, hexact.2.2.2⟩
199 · intro x y hxy
200 apply hexact.1
201 have hcongr := congrArg e hxy
202 simpa using hcongr
203 · exact Function.Exact.linearEquiv_symm_comp_comp e hexact.2.1
204 · exact Function.Exact.comp_linearEquiv e hexact.2.2.1
206end LinearEquivTransport
208end
210end CrowellExactSequence