English
For a locally constant function f on C with integer values, if a certain linear combination vanishes, then f lies in the image of a constructed splitting map; i.e., there exists y with a prescribed equality.
Русский
Для локально постоянной функции f на C с целочисленными значениями, если определенный линейный компонент равен нулю, то существует y, удовлетворяющее равенству через заданный отображатель.
LaTeX
$$$ \\forall f:\\mathrm{LocallyConstant}\, C\\mathbb{Z},\\ (\\mathrm{Linear\\_CC'} C hsC ho\\, f = 0) \\Rightarrow \\exists y, \\ \\pi_s C o y = f $$$
Lean4
theorem CC_exact {f : LocallyConstant C ℤ} (hf : Linear_CC' C hsC ho f = 0) : ∃ y, πs C o y = f :=
by
dsimp [Linear_CC', Linear_CC'₀, Linear_CC'₁] at hf
simp only [sub_eq_zero, ← LocallyConstant.coe_inj] at hf
let C₀C : C0 C ho → C := fun x ↦ ⟨x.val, x.prop.1⟩
have h₀ : Continuous C₀C := Continuous.subtype_mk continuous_induced_dom _
let C₁C : π (C1 C ho) (ord I · < o) → C := fun x ↦ ⟨SwapTrue o x.val, (swapTrue_mem_C1 C hsC ho x).1⟩
have h₁ : Continuous C₁C := Continuous.subtype_mk ((continuous_swapTrue o).comp continuous_subtype_val) _
refine
⟨LocallyConstant.piecewise' ?_ (isClosed_C0 C hC ho) (isClosed_proj _ o (isClosed_C1 C hC ho)) (f.comap ⟨C₀C, h₀⟩)
(f.comap ⟨C₁C, h₁⟩) ?_,
?_⟩
· rintro _ ⟨y, hyC, rfl⟩
simp only [Set.mem_union]
rw [← union_C0C1_eq C ho] at hyC
refine hyC.imp (fun hyC ↦ ?_) (fun hyC ↦ ⟨y, hyC, rfl⟩)
rwa [C0_projOrd C hsC ho hyC]
· intro x hx
simpa only [h₀, h₁, LocallyConstant.coe_comap] using (congrFun hf ⟨x, hx⟩).symm
· ext ⟨x, hx⟩
rw [← union_C0C1_eq C ho] at hx
rcases hx with hx₀ | hx₁
· have hx₀' : ProjRestrict C (ord I · < o) ⟨x, hx⟩ = x := by
simpa only [ProjRestrict, Set.MapsTo.val_restrict_apply] using C0_projOrd C hsC ho hx₀
simp only [C₀C, πs_apply_apply, hx₀', hx₀, LocallyConstant.piecewise'_apply_left, LocallyConstant.coe_comap,
ContinuousMap.coe_mk, Function.comp_apply]
· have hx₁' : (ProjRestrict C (ord I · < o) ⟨x, hx⟩).val ∈ π (C1 C ho) (ord I · < o) := by
simpa only [ProjRestrict, Set.MapsTo.val_restrict_apply] using ⟨x, hx₁, rfl⟩
simp only [C₁C, πs_apply_apply, LocallyConstant.coe_comap, Function.comp_apply, hx₁',
LocallyConstant.piecewise'_apply_right]
congr
simp only [ContinuousMap.coe_mk, Subtype.mk.injEq]
exact C1_projOrd C hsC ho hx₁
