English
The continuousCohomology complex is the functor from the homogeneous cochains to invariants, via the homology functor.
Русский
Комплекс когомологий непрерывной группы задаётся как функтор из однородных когомологий к инвариантам через гомологический функтор.
LaTeX
$$$\\text{continuousCohomology } R G = \\text{homogeneousCochains } R G \\ ⋙ \\text{HomologicalComplex.homologyFunctor } _ _$$$
Lean4
/-- The `0`-homogeneous cochains are isomorphic to `Xᴳ`. -/
def kerHomogeneousCochainsZeroEquiv (X : Action (TopModuleCat R) G) (n : ℕ) (hn : n = 1) :
LinearMap.ker (((homogeneousCochains R G).obj X).d 0 n).hom ≃L[R] (invariants R G).obj X
where
toFun
x :=
{ val := DFunLike.coe (F := C(G, _)) x.1.1 1
property
g := by
subst hn
obtain ⟨⟨x : C(G, _), hx⟩, hx'⟩ := x
have : (X.ρ g).hom (x (g⁻¹ * 1)) = x 1 := congr(DFunLike.coe (F := C(G, _)) $(hx g) 1)
have hx' : x (g⁻¹ * 1) - x 1 = 0 :=
congr(DFunLike.coe (F := C(G, _)) (DFunLike.coe (F := C(G, _)) ($hx').1 1) (g⁻¹ * 1))
rw [sub_eq_zero] at hx'
exact congr((X.ρ g).hom $hx').symm.trans this }
map_add' _ _ := rfl
map_smul' _ _ := rfl
invFun
x :=
by
refine ⟨⟨ContinuousLinearMap.const R _ x.1, fun g ↦ ContinuousMap.ext fun a ↦ by subst hn; exact x.2 g⟩, ?_⟩
subst hn
exact Subtype.ext (ContinuousMap.ext fun a ↦ ContinuousMap.ext fun b ↦ show x.1 - x.1 = (0 : X.V) by simp)
left_inv
x := by
subst hn
obtain ⟨⟨x : C(G, _), hx⟩, hx'⟩ := x
refine Subtype.ext (Subtype.ext <| ContinuousMap.ext fun a ↦ ?_)
have hx' : x 1 - x a = 0 := congr(DFunLike.coe (F := C(G, _)) (DFunLike.coe (F := C(G, _)) ($hx').1 a) 1)
rwa [sub_eq_zero] at hx'
right_inv _ := rfl
continuous_toFun :=
continuous_induced_rng.mpr
((continuous_eval_const (F := C(G, _)) 1).comp (continuous_subtype_val.comp continuous_subtype_val))
continuous_invFun :=
continuous_induced_rng.mpr
(continuous_induced_rng.mpr ((ContinuousLinearMap.const R G).cont.comp continuous_subtype_val))
