FiniteCyclicH2CoefficientNorm.lean

theorem finiteCyclicGroupH2_piEven_surjective
    {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
    (A : Rep R G) (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    Function.Surjective
      (Rep.FiniteCyclicGroup.groupCohomologyπEven A g hg 2 (by decide)) := by
  let S : ShortComplex (ModuleCat R) := Rep.FiniteCyclicGroup.normHomCompSub A g
  let e : groupCohomology A 2 ≅ S.homology :=
    Rep.FiniteCyclicGroup.groupCohomologyIsoEven A g hg 2 (by decide)
  have hπ : Function.Surjective S.homologyπ :=
    (ModuleCat.epi_iff_surjective S.homologyπ).mp inferInstance
  intro x
  obtain ⟨y, hy⟩ := hπ (e.hom x)
  refine ⟨S.moduleCatCyclesIso.hom y, ?_⟩
  change e.inv
    (S.homologyπ (S.moduleCatCyclesIso.inv (S.moduleCatCyclesIso.hom y))) = x
  have hCycles : S.moduleCatCyclesIso.inv (S.moduleCatCyclesIso.hom y) = y :=
    S.moduleCatCyclesIso.toLinearEquiv.symm_apply_apply y
  exact (congrArg (fun z : S.cycles ↦ e.inv (S.homologyπ z)) hCycles).trans
    ((congrArg (fun z : S.homology ↦ e.inv z) hy).trans
      (e.toLinearEquiv.symm_apply_apply x))

theorem finiteCyclicH2_coefficientMap_eq_zero_of_norm
    {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
    (A B : Rep R G) (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (φ : A ⟶ B)
    (hNorm : ∀ a : LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap,
      ∃ b : B, B.norm.hom b = φ.hom a.1) :
    groupCohomology.map (MonoidHom.id G) φ 2 = 0