FiniteCyclicBarPeriodicH2Comparison.lean

def resolutionLinearYonedaMap
    {X X' : Rep R G} {f : X ⟶ X'}
    (P : ProjectiveResolution X) (P' : ProjectiveResolution X')
    (phi : ProjectiveResolution.Hom P P' f) (A : Rep R G) :
    P'.complex.linearYonedaObj R A ⟶ P.complex.linearYonedaObj R A

theorem resolutionLinearYonedaMap_f
    {X X' : Rep R G} {f : X ⟶ X'}
    (P : ProjectiveResolution X) (P' : ProjectiveResolution X')
    (phi : ProjectiveResolution.Hom P P' f) (A : Rep R G) (n : ℕ) :
    (resolutionLinearYonedaMap P P' phi A).f n =
      ModuleCat.ofHom (Linear.leftComp R A (phi.hom.f n))

theorem resolution_isoExt_hom_naturality
    {X X' : Rep R G} {f : X ⟶ X'}
    (P : ProjectiveResolution X) (P' : ProjectiveResolution X')
    (phi : ProjectiveResolution.Hom P P' f) (A : Rep R G) (i : ℕ) :
    (((_root_.Ext R (Rep R G) i).map f.op).app A) ≫ (P.isoExt i A).hom =
      (P'.isoExt i A).hom ≫
        HomologicalComplex.homologyMap
          (resolutionLinearYonedaMap P P' phi A) i

theorem groupCohomologyIso_hom_naturality
    (P P' : ProjectiveResolution (Rep.trivial R G R))
    (phi : ProjectiveResolution.Hom P P' (𝟙 _))
    (A : Rep R G) (i : ℕ) :
    (groupCohomologyIso A i P).hom =
      (groupCohomologyIso A i P').hom ≫
        HomologicalComplex.homologyMap
          (resolutionLinearYonedaMap P P' phi A) i

def cyclicPeriodicH2HomologyOwnerIso
    (A : Rep R G) (g : G) :
    (Rep.FiniteCyclicGroup.moduleCatCochainComplex A g).homology 2 ≅
      ((Rep.FiniteCyclicGroup.moduleCatCochainComplex A g).sc 2).homology

theorem cyclicPeriodicH2HomologyOwnerIso_hom
    (A : Rep R G) (g : G) :
    (cyclicPeriodicH2HomologyOwnerIso A g).hom =
      𝟙 ((Rep.FiniteCyclicGroup.moduleCatCochainComplex A g).homology 2)

theorem cyclicPeriodicH2HomologyOwnerIso_eq_refl
    (A : Rep R G) (g : G) :
    cyclicPeriodicH2HomologyOwnerIso A g =
      Iso.refl
        ((Rep.FiniteCyclicGroup.moduleCatCochainComplex A g).homology 2)

def cyclicPeriodicH2ScIso (A : Rep R G) (g : G) :
    (Rep.FiniteCyclicGroup.moduleCatCochainComplex A g).sc 2 ≅
      Rep.FiniteCyclicGroup.normHomCompSub A g

def cyclicPeriodicH2Iso
    (A : Rep R G) (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    ((Rep.FiniteCyclicGroup.resolution R g hg).complex.linearYonedaObj R A).homology 2 ≅
      (Rep.FiniteCyclicGroup.normHomCompSub A g).homology

theorem cyclicPeriodicH2ScIso_inv_τ₂ (A : Rep R G) (g : G) :
    (cyclicPeriodicH2ScIso A g).inv.τ₂ = 𝟙 _

theorem cyclicPeriodicH2Iso_eq
    (A : Rep R G) (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    cyclicPeriodicH2Iso A g hg =
      HomologicalComplex.homologyMapIso
          (Rep.FiniteCyclicGroup.homResolutionIso A g hg) 2 ≪≫
        ShortComplex.homologyMapIso (cyclicPeriodicH2ScIso A g)

def cyclicPeriodicH2KernelIso
    (A : Rep R G) (g : G) :
    ModuleCat.of R
        (LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap) ≅
      (Rep.FiniteCyclicGroup.normHomCompSub A g).moduleCatLeftHomologyData.K

theorem cyclicPeriodicH2KernelIso_hom
    (A : Rep R G) (g : G) :
    (cyclicPeriodicH2KernelIso A g).hom =
      𝟙 (ModuleCat.of R
        (LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap))

def cyclicPeriodicH2CyclesOwnerIso
    (A : Rep R G) (g : G) :
    ((Rep.FiniteCyclicGroup.moduleCatCochainComplex A g).sc 2).cycles ≅
      (Rep.FiniteCyclicGroup.moduleCatCochainComplex A g).cycles 2

theorem cyclicPeriodicH2CyclesOwnerIso_hom
    (A : Rep R G) (g : G) :
    (cyclicPeriodicH2CyclesOwnerIso A g).hom =
      𝟙 ((Rep.FiniteCyclicGroup.moduleCatCochainComplex A g).cycles 2)

def cyclicPeriodicH2DegreeOwnerIso
    (A : Rep R G) (g : G) :
    ((Rep.FiniteCyclicGroup.moduleCatCochainComplex A g).sc 2).X₂ ≅
      (Rep.FiniteCyclicGroup.moduleCatCochainComplex A g).X 2

theorem cyclicPeriodicH2DegreeOwnerIso_hom
    (A : Rep R G) (g : G) :
    (cyclicPeriodicH2DegreeOwnerIso A g).hom =
      𝟙 ((Rep.FiniteCyclicGroup.moduleCatCochainComplex A g).X 2)

theorem cyclicPeriodicH2CyclesOwnerIso_hom_iCycles
    (A : Rep R G) (g : G) :
    (cyclicPeriodicH2CyclesOwnerIso A g).hom ≫
        (Rep.FiniteCyclicGroup.moduleCatCochainComplex A g).iCycles 2 =
      ((Rep.FiniteCyclicGroup.moduleCatCochainComplex A g).sc 2).iCycles ≫
        (cyclicPeriodicH2DegreeOwnerIso A g).hom

theorem cyclicPeriodicH2DegreeOwners_comp_homResolutionIso_inv
    (A : Rep R G) (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    (cyclicPeriodicH2ScIso A g).inv.τ₂ ≫
        (cyclicPeriodicH2DegreeOwnerIso A g).hom ≫
        (Rep.FiniteCyclicGroup.homResolutionIso A g hg).inv.f 2 =
      (Rep.FiniteCyclicGroup.homResolutionIso A g hg).inv.f 2

theorem cyclicPeriodicH2OwnerIso_homologyπ
    (A : Rep R G) (g : G) :
    (cyclicPeriodicH2CyclesOwnerIso A g).hom ≫
        (Rep.FiniteCyclicGroup.moduleCatCochainComplex A g).homologyπ 2 ≫
        (cyclicPeriodicH2HomologyOwnerIso A g).hom =
      ((Rep.FiniteCyclicGroup.moduleCatCochainComplex A g).sc 2).homologyπ

theorem cyclicPeriodicH2Iso_hom_owner
    (A : Rep R G) (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    (cyclicPeriodicH2Iso A g hg).hom =
      (HomologicalComplex.homologyMapIso
        (Rep.FiniteCyclicGroup.homResolutionIso A g hg) 2).hom ≫
      (cyclicPeriodicH2HomologyOwnerIso A g).hom ≫
      (ShortComplex.homologyMapIso (cyclicPeriodicH2ScIso A g)).hom

def cyclicPeriodicH2CyclesMap
    (A : Rep R G) (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    ModuleCat.of R
        (LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap) ⟶
      ((Rep.FiniteCyclicGroup.resolution R g hg).complex.linearYonedaObj R A).cycles 2

theorem cyclicPeriodicH2CyclesMap_iCycles
    (A : Rep R G) (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    cyclicPeriodicH2CyclesMap A g hg ≫
        ((Rep.FiniteCyclicGroup.resolution R g hg).complex.linearYonedaObj R A).iCycles 2 =
      (Rep.FiniteCyclicGroup.normHomCompSub A g).moduleCatLeftHomologyData.i ≫
        (Rep.FiniteCyclicGroup.homResolutionIso A g hg).inv.f 2

theorem cyclicPeriodicH2CyclesMap_iCycles_apply
    (A : Rep R G) (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g)
    (a : LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap) :
    (((Rep.FiniteCyclicGroup.resolution R g hg).complex.linearYonedaObj R A).iCycles 2).hom
        ((cyclicPeriodicH2CyclesMap A g hg).hom a) =
      ((Rep.FiniteCyclicGroup.homResolutionIso A g hg).inv.f 2).hom a.1

theorem cyclicPeriodicH2CyclesMap_homologyπ
    (A : Rep R G) (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    cyclicPeriodicH2CyclesMap A g hg ≫
        ((Rep.FiniteCyclicGroup.resolution R g hg).complex.linearYonedaObj R A).homologyπ 2 ≫
        (cyclicPeriodicH2Iso A g hg).hom =
      (ShortComplex.moduleCatCyclesIso
        (Rep.FiniteCyclicGroup.normHomCompSub A g)).inv ≫
        ShortComplex.homologyπ
          (Rep.FiniteCyclicGroup.normHomCompSub A g)

theorem cyclicPeriodicH2CyclesMap_groupCohomologyIso_inv
    (A : Rep R G) (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    cyclicPeriodicH2CyclesMap A g hg ≫
        ((Rep.FiniteCyclicGroup.resolution R g hg).complex.linearYonedaObj R A).homologyπ 2 ≫
        (groupCohomologyIso A 2
          (Rep.FiniteCyclicGroup.resolution R g hg)).inv =
      Rep.FiniteCyclicGroup.groupCohomologyπEven A g hg 2 (by simp) := by
  change
    cyclicPeriodicH2CyclesMap A g hg ≫
        ((Rep.FiniteCyclicGroup.resolution R g hg).complex.linearYonedaObj R A).homologyπ 2 ≫
      (groupCohomologyIso A 2
          (Rep.FiniteCyclicGroup.resolution R g hg)).inv =
      (ShortComplex.moduleCatCyclesIso
        (Rep.FiniteCyclicGroup.normHomCompSub A g)).inv ≫
        ShortComplex.homologyπ
          (Rep.FiniteCyclicGroup.normHomCompSub A g) ≫
        (Rep.FiniteCyclicGroup.groupCohomologyIsoEven
          A g hg 2 (by simp)).inv
  rw [show Rep.FiniteCyclicGroup.groupCohomologyIsoEven A g hg 2 (by simp) =
    groupCohomologyIso A 2
        (Rep.FiniteCyclicGroup.resolution R g hg) ≪≫
      cyclicPeriodicH2Iso A g hg by
        rw [cyclicPeriodicH2Iso_eq]
        rfl]
  simp only [Iso.trans_inv]
  let f :
      ModuleCat.of R
          (LinearMap.ker
            (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap) ⟶
        ((Rep.FiniteCyclicGroup.resolution R g hg).complex.linearYonedaObj
          R A).homology 2 :=
    cyclicPeriodicH2CyclesMap A g hg ≫
      ((Rep.FiniteCyclicGroup.resolution R g hg).complex.linearYonedaObj
        R A).homologyπ 2
  let n :
      ModuleCat.of R
          (LinearMap.ker
            (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap) ⟶
        (Rep.FiniteCyclicGroup.normHomCompSub A g).homology :=
    (cyclicPeriodicH2KernelIso A g).hom ≫
      (Rep.FiniteCyclicGroup.normHomCompSub A g).moduleCatCyclesIso.inv ≫
      (Rep.FiniteCyclicGroup.normHomCompSub A g).homologyπ
  let e := cyclicPeriodicH2Iso A g hg
  let j := (groupCohomologyIso A 2
    (Rep.FiniteCyclicGroup.resolution R g hg)).inv
  have hfe : f ≫ e.hom = n := by
    exact Eq.mp (by rfl)
      (cyclicPeriodicH2CyclesMap_homologyπ A g hg)
  have hRaw : f ≫ j = (n ≫ e.inv) ≫ j := by
    calc
      f ≫ j = f ≫ (e.hom ≫ e.inv ≫ j) :=
        congrArg (fun k ↦ f ≫ k) (Iso.hom_inv_id_assoc e j).symm
      _ = (f ≫ e.hom) ≫ (e.inv ≫ j) :=
        (Category.assoc f e.hom (e.inv ≫ j)).symm
      _ = n ≫ (e.inv ≫ j) :=
        congrArg (fun k ↦ k ≫ (e.inv ≫ j)) hfe
      _ = (n ≫ e.inv) ≫ j :=
        (Category.assoc n e.inv j).symm
  exact Eq.mp (by rfl) hRaw

theorem cyclicPeriodicH2CyclesMap_groupCohomologyIso_inv_apply
    (A : Rep R G) (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g)
    (a : LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap) :
    (groupCohomologyIso A 2
      (Rep.FiniteCyclicGroup.resolution R g hg)).inv.hom
        ((((Rep.FiniteCyclicGroup.resolution R g hg).complex.linearYonedaObj R A).homologyπ 2).hom
          ((cyclicPeriodicH2CyclesMap A g hg).hom a)) =
      (Rep.FiniteCyclicGroup.groupCohomologyπEven
        A g hg 2 (by simp)).hom a := by
  exact congrArg (fun f ↦ f.hom a)
    (cyclicPeriodicH2CyclesMap_groupCohomologyIso_inv A g hg)

def finiteCyclicBarToPeriodicLinearYonedaMap
    (A : Rep R G) (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    (Rep.FiniteCyclicGroup.resolution R g hg).complex.linearYonedaObj R A ⟶
      (Rep.barResolution R G).complex.linearYonedaObj R A

theorem finiteCyclicBarToPeriodicLinearYonedaMap_f
    (A : Rep R G) (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) (n : ℕ) :
    (finiteCyclicBarToPeriodicLinearYonedaMap A g hg).f n =
      ModuleCat.ofHom (Linear.leftComp R A
        ((finiteCyclicBarToPeriodicComparison (R := R) g hg).f n))

theorem finiteCyclicBarToPeriodic_groupCohomologyIso_hom
    (A : Rep R G) (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) (i : ℕ) :
    (groupCohomologyIso A i (Rep.barResolution R G)).hom =
      (groupCohomologyIso A i
          (Rep.FiniteCyclicGroup.resolution R g hg)).hom ≫
        HomologicalComplex.homologyMap
          (finiteCyclicBarToPeriodicLinearYonedaMap A g hg) i

def chainLinearYonedaMap
    {B P : ChainComplex (Rep R G) ℕ} (phi : B ⟶ P) (A : Rep R G) :
    P.linearYonedaObj R A ⟶ B.linearYonedaObj R A

def finiteCyclicBarPeriodicCochainMap
    (A : Rep R G) (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    ((Rep.FiniteCyclicGroup.resolution R g hg).complex.linearYonedaObj R A) ⟶
      ((Rep.barComplex R G).linearYonedaObj R A)

theorem finiteCyclicBarPeriodicCochainMap_two_carry
    (A : Rep R G) (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap) :
    Rep.freeLiftLEquiv R G (Fin 2 → G) A
        (((finiteCyclicBarPeriodicCochainMap A g hg).f 2).hom
          (((Rep.FiniteCyclicGroup.homResolutionIso A g hg).inv.f 2).hom
            a.1)) =
      (groupCohomology.cochainsIso₂ A).inv
        (finiteCyclicCarryTwoCocycle A g hg a)

def finiteCyclicBarCarryCycle
    (A : Rep R G) (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap) :
    ((Rep.barComplex R G).linearYonedaObj R A).cycles 2

theorem finiteCyclicBarCarryCycle_i
    (A : Rep R G) (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap) :
    Rep.freeLiftLEquiv R G (Fin 2 → G) A
        (((Rep.barComplex R G).linearYonedaObj R A).iCycles 2
          (finiteCyclicBarCarryCycle A g hg a)) =
      (groupCohomology.cochainsIso₂ A).inv
        (finiteCyclicCarryTwoCocycle A g hg a)

theorem finiteCyclicBarPeriodic_cyclesMap_eq
    (A : Rep R G) (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap) :
    HomologicalComplex.cyclesMap
        (finiteCyclicBarPeriodicCochainMap A g hg) 2
        ((cyclicPeriodicH2CyclesMap A g hg).hom a) =
      finiteCyclicBarCarryCycle A g hg a

theorem groupCohomologyIso_bar_hom_eq_homologyMap
    (A : Rep R G) :
    (groupCohomologyIso A 2 (Rep.barResolution R G)).hom =
      HomologicalComplex.homologyMap
        (groupCohomology.inhomogeneousCochainsIso A).hom 2

theorem groupCohomologyIso_bar_H2π_carry
    (A : Rep R G) (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap) :
    (groupCohomologyIso A 2 (Rep.barResolution R G)).hom
        (groupCohomology.H2π A (finiteCyclicCarryTwoCocycle A g hg a)) =
      ((Rep.barComplex R G).linearYonedaObj R A).homologyπ 2
        (finiteCyclicBarCarryCycle A g hg a)

theorem finiteCyclicBarPeriodic_homologyMap_carry
    (A : Rep R G) (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap) :
    HomologicalComplex.homologyMap
        (finiteCyclicBarPeriodicCochainMap A g hg) 2
        ((((Rep.FiniteCyclicGroup.resolution R g hg).complex.linearYonedaObj
          R A).homologyπ 2)
            ((cyclicPeriodicH2CyclesMap A g hg).hom a)) =
      (groupCohomologyIso A 2 (Rep.barResolution R G)).hom
        (groupCohomology.H2π A
          (finiteCyclicCarryTwoCocycle A g hg a))

theorem finiteCyclicBarPeriodicCochainMap_eq
    (A : Rep R G) (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    finiteCyclicBarPeriodicCochainMap A g hg =
      finiteCyclicBarToPeriodicLinearYonedaMap A g hg

theorem H2π_finiteCyclicCarryTwoCocycle
    (A : Rep R G) (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap) :
    groupCohomology.H2π A (finiteCyclicCarryTwoCocycle A g hg a) =
      Rep.FiniteCyclicGroup.groupCohomologyπEven
        A g hg 2 (by simp) a := by
  apply (ModuleCat.mono_iff_injective
    ((groupCohomologyIso A 2 (Rep.barResolution R G)).hom)).1
      inferInstance
  rw [← finiteCyclicBarPeriodic_homologyMap_carry]
  rw [finiteCyclicBarPeriodicCochainMap_eq]
  rw [finiteCyclicBarToPeriodic_groupCohomologyIso_hom A g hg 2]
  rw [ConcreteCategory.comp_apply]
  rw [← cyclicPeriodicH2CyclesMap_groupCohomologyIso_inv_apply
    A g hg a]
  rw [Iso.inv_hom_id_apply]
  rfl