@[reducible, inline]

abbrev GroupCohomology.GModule (k : Type u) [CommRing k] (G : Type u) [Group G] : Type (max u (u_1 + 1))

@[reducible, inline]

noncomputable abbrev GroupCohomology.GInvariants {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep.{u_1, u, u} k G) : Submodule k ↑A

@[reducible, inline]

noncomputable abbrev GroupCohomology.nCochains {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep.{u, u, u} k G) (n : ℕ) : ModuleCat k

@[reducible, inline]

noncomputable abbrev GroupCohomology.coboundaryMap {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep.{u, u, u} k G) (n : ℕ) : nCochains A n ⟶ nCochains A (n + 1)

theorem GroupCohomology.coboundaryMap_comp_coboundaryMap {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep.{u, u, u} k G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (coboundaryMap A n) (coboundaryMap A (n + 1)) = 0

@[reducible, inline]

noncomputable abbrev GroupCohomology.cochainComplex {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep.{u, u, u} k G) : CochainComplex (ModuleCat k) ℕ

@[reducible, inline]

noncomputable abbrev GroupCohomology.nCocycles {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep.{u, u, u} k G) (n : ℕ) : ModuleCat k

@[reducible, inline]

noncomputable abbrev GroupCohomology.CohomologyGroup {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep.{u, u, u} k G) (n : ℕ) : ModuleCat k

noncomputable def GroupCohomology.cochainComplexMap {k : Type u} [CommRing k] {G : Type u} [Group G] {A B : Rep.{u, u, u} k G} (φ : A ⟶ B) : cochainComplex A ⟶ cochainComplex B

noncomputable def GroupCohomology.cohomology_map {k : Type u} [CommRing k] {G : Type u} [Group G] {A B : Rep.{u, u, u} k G} (φ : A ⟶ B) (n : ℕ) : CohomologyGroup A n ⟶ CohomologyGroup B n

theorem GroupCohomology.ses_cochains_exact {k : Type u} [CommRing k] {G : Type u} [Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hX : X.ShortExact) : (X.map (groupCohomology.cochainsFunctor k G)).ShortExact

theorem GroupCohomology.long_exact_sequence_exact₂ {k : Type u} [CommRing k] {G : Type u} [Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hX : X.ShortExact) (n : ℕ) : (groupCohomology.mapShortComplex₂ X n).Exact

theorem GroupCohomology.long_exact_sequence_exact₁ {k : Type u} [CommRing k] {G : Type u} [Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hX : X.ShortExact) {i j : ℕ} (hij : i + 1 = j) : (groupCohomology.mapShortComplex₁ hX hij).Exact

structure DeltaFunctor.CohomologicalDeltaFunctor (𝒜 : Type w₁) [CategoryTheory.Category.{w₂, w₁} 𝒜] [CategoryTheory.Abelian 𝒜] (ℬ : Type w₁) [CategoryTheory.Category.{w₂, w₁} ℬ] [CategoryTheory.Abelian ℬ] : Type (max w₁ w₂)

• F : ℕ → CategoryTheory.Functor 𝒜 ℬ
• additive (n : ℕ) : (self.F n).Additive
• δ (S : CategoryTheory.ShortComplex 𝒜) : S.ShortExact → (n : ℕ) → (self.F n).obj S.X₃ ⟶ (self.F (n + 1)).obj S.X₁
• map_g_comp_δ (S : CategoryTheory.ShortComplex 𝒜) (hS : S.ShortExact) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((self.F n).map S.g) (self.δ S hS n) = 0
• δ_comp_map_f (S : CategoryTheory.ShortComplex 𝒜) (hS : S.ShortExact) (n : ℕ) : CategoryTheory.CategoryStruct.comp (self.δ S hS n) ((self.F (n + 1)).map S.f) = 0
• exact₂ (S : CategoryTheory.ShortComplex 𝒜) : S.ShortExact → ∀ (n : ℕ), { X₁ := (self.F n).obj S.X₁, X₂ := (self.F n).obj S.X₂, X₃ := (self.F n).obj S.X₃, f := (self.F n).map S.f, g := (self.F n).map S.g, zero := ⋯ }.Exact
• exact₃ (S : CategoryTheory.ShortComplex 𝒜) (hS : S.ShortExact) (n : ℕ) : { X₁ := (self.F n).obj S.X₂, X₂ := (self.F n).obj S.X₃, X₃ := (self.F (n + 1)).obj S.X₁, f := (self.F n).map S.g, g := self.δ S hS n, zero := ⋯ }.Exact
• exact₁ (S : CategoryTheory.ShortComplex 𝒜) (hS : S.ShortExact) (n : ℕ) : { X₁ := (self.F n).obj S.X₃, X₂ := (self.F (n + 1)).obj S.X₁, X₃ := (self.F (n + 1)).obj S.X₂, f := self.δ S hS n, g := (self.F (n + 1)).map S.f, zero := ⋯ }.Exact
• δ_natural {S T : CategoryTheory.ShortComplex 𝒜} (hS : S.ShortExact) (hT : T.ShortExact) (φ : S ⟶ T) (n : ℕ) : CategoryTheory.CategoryStruct.comp (self.δ S hS n) ((self.F (n + 1)).map φ.τ₁) = CategoryTheory.CategoryStruct.comp ((self.F n).map φ.τ₃) (self.δ T hT n)

structure DeltaFunctor.HomologicalDeltaFunctor (𝒜 : Type w₁) [CategoryTheory.Category.{w₂, w₁} 𝒜] [CategoryTheory.Abelian 𝒜] (ℬ : Type w₁) [CategoryTheory.Category.{w₂, w₁} ℬ] [CategoryTheory.Abelian ℬ] : Type (max w₁ w₂)

• F : ℕ → CategoryTheory.Functor 𝒜 ℬ
• additive (n : ℕ) : (self.F n).Additive
• δ (S : CategoryTheory.ShortComplex 𝒜) : S.ShortExact → (n : ℕ) → (self.F (n + 1)).obj S.X₃ ⟶ (self.F n).obj S.X₁
• map_g_comp_δ (S : CategoryTheory.ShortComplex 𝒜) (hS : S.ShortExact) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((self.F (n + 1)).map S.g) (self.δ S hS n) = 0
• δ_comp_map_f (S : CategoryTheory.ShortComplex 𝒜) (hS : S.ShortExact) (n : ℕ) : CategoryTheory.CategoryStruct.comp (self.δ S hS n) ((self.F n).map S.f) = 0
• exact₂ (S : CategoryTheory.ShortComplex 𝒜) : S.ShortExact → ∀ (n : ℕ), { X₁ := (self.F n).obj S.X₁, X₂ := (self.F n).obj S.X₂, X₃ := (self.F n).obj S.X₃, f := (self.F n).map S.f, g := (self.F n).map S.g, zero := ⋯ }.Exact
• exact₁ (S : CategoryTheory.ShortComplex 𝒜) (hS : S.ShortExact) (n : ℕ) : { X₁ := (self.F (n + 1)).obj S.X₃, X₂ := (self.F n).obj S.X₁, X₃ := (self.F n).obj S.X₂, f := self.δ S hS n, g := (self.F n).map S.f, zero := ⋯ }.Exact
• exact₃ (S : CategoryTheory.ShortComplex 𝒜) (hS : S.ShortExact) (n : ℕ) : { X₁ := (self.F (n + 1)).obj S.X₂, X₂ := (self.F (n + 1)).obj S.X₃, X₃ := (self.F n).obj S.X₁, f := (self.F (n + 1)).map S.g, g := self.δ S hS n, zero := ⋯ }.Exact
• δ_natural {S T : CategoryTheory.ShortComplex 𝒜} (hS : S.ShortExact) (hT : T.ShortExact) (φ : S ⟶ T) (n : ℕ) : CategoryTheory.CategoryStruct.comp (self.δ S hS n) ((self.F n).map φ.τ₁) = CategoryTheory.CategoryStruct.comp ((self.F (n + 1)).map φ.τ₃) (self.δ T hT n)

noncomputable def GroupCohomology.standardResolution (k G : Type u) [CommRing k] [Group G] : CategoryTheory.ProjectiveResolution (Rep.trivial k G k)

structure GroupCohomology.FreeResolution (R : Type u) [Ring R] (M : ModuleCat R) extends CategoryTheory.ProjectiveResolution M : Type (u + 1)

• complex : ChainComplex (ModuleCat R) ℕ
• projective (n : ℕ) : Projective (self.complex.X n)
• hasHomology (i : ℕ) : HomologicalComplex.HasHomology self.complex i
• π : self.complex ⟶ (ChainComplex.single₀ (ModuleCat R)).obj M
• quasiIso : QuasiIso self.π
• free (n : ℕ) : Module.Free R ↑(self.complex.X n)

noncomputable def GroupCohomology.barComplex_iso_standardComplex (k G : Type u) [CommRing k] [Group G] : Rep.barComplex k G ≅ Rep.standardComplex k G

noncomputable def GroupCohomology.cohomology_iso_ext {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep.{u, u, u} k G) (n : ℕ) : CohomologyGroup A n ≅ ((Ext k (Rep.{u, u, u} k G) n).obj (Opposite.op (Rep.trivial k G k))).obj A

class GroupCohomology.IsAdditiveCategory (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] extends CategoryTheory.Preadditive C : Type (max u_1 u_2)

• homGroup (P Q : C) : AddCommGroup (P ⟶ Q)
• add_comp (P Q R : C) (f f' : P ⟶ Q) (g : Q ⟶ R) : CategoryStruct.comp (f + f') g = CategoryStruct.comp f g + CategoryStruct.comp f' g
• comp_add (P Q R : C) (f : P ⟶ Q) (g g' : Q ⟶ R) : CategoryStruct.comp f (g + g') = CategoryStruct.comp f g + CategoryStruct.comp f g'
• hasFiniteBiproducts : CategoryTheory.Limits.HasFiniteBiproducts C

@[instance 100]

instance GroupCohomology.IsAdditiveCategory.toHasFiniteCoproducts (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [IsAdditiveCategory C] : CategoryTheory.Limits.HasFiniteCoproducts C

@[instance 100]

instance GroupCohomology.IsAdditiveCategory.toHasFiniteProducts (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [IsAdditiveCategory C] : CategoryTheory.Limits.HasFiniteProducts C

@[instance 100]

instance GroupCohomology.IsAdditiveCategory.toHasZeroObject (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [IsAdditiveCategory C] : CategoryTheory.Limits.HasZeroObject C

class GroupCohomology.IsAdditiveFunctor {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) extends F.Additive : Prop

• map_add {X Y : C} {f g : X ⟶ Y} : F.map (f + g) = F.map f + F.map g

instance GroupCohomology.cochainsFunctor_additive (k G : Type u) [CommRing k] [Group G] : (groupCohomology.cochainsFunctor k G).Additive

noncomputable def GroupCohomology.cohomology_biprod_iso (k G : Type u) [CommRing k] [Group G] (A B : Rep.{u, u, u} k G) (n : ℕ) : groupCohomology (A ⊞ B) n ≅ groupCohomology A n ⊞ groupCohomology B n

noncomputable def GroupCohomology.coinduced_def (k G : Type u) [CommRing k] [Group G] : CategoryTheory.Functor (Rep.{u_1, u, u} k ↥⊥) (Rep.{max u u_1, u, u} k G)

theorem GroupCohomology.cohomology_coinduced_vanishing {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep.{u, u, u} k ↥⊥) (n : ℕ) : CategoryTheory.Limits.IsZero (groupCohomology (Rep.coind.{u, u, u, u} ⊥.subtype A) (n + 1))

noncomputable def GroupCohomology.cohomology_coinduced_H0_iso {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep.{u, u, u} k ↥⊥) : groupCohomology (Rep.coind.{u, u, u, u} ⊥.subtype A) 0 ≅ groupCohomology A 0

@[reducible, inline]

noncomputable abbrev GroupCohomology.HomologyGroup {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep.{u, u, u} k G) (n : ℕ) : ModuleCat k

noncomputable def GroupCohomology.homology_map {k : Type u} [CommRing k] {G : Type u} [Group G] {A B : Rep.{u, u, u} k G} (φ : A ⟶ B) (n : ℕ) : HomologyGroup A n ⟶ HomologyGroup B n

theorem GroupCohomology.homology_map_id {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep.{u, u, u} k G) (n : ℕ) : homology_map (CategoryTheory.CategoryStruct.id A) n = CategoryTheory.CategoryStruct.id (HomologyGroup A n)

theorem GroupCohomology.homology_map_comp {k : Type u} [CommRing k] {G : Type u} [Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ) : homology_map (CategoryTheory.CategoryStruct.comp φ ψ) n = CategoryTheory.CategoryStruct.comp (homology_map φ n) (homology_map ψ n)

noncomputable def GroupCohomology.homologyFunctor (k : Type u) [CommRing k] (G : Type u) [Group G] (n : ℕ) : CategoryTheory.Functor (Rep.{u, u, u} k G) (ModuleCat k)

noncomputable def GroupCohomology.induced_def (k G : Type u) [CommRing k] [Group G] : CategoryTheory.Functor (Rep.{u_1, u, u} k ↥⊥) (Rep.{max u u_1, u, u} k G)

structure GroupCohomology.IsLeftExact {C' : Type u_1} [CategoryTheory.Category.{u_2, u_1} C'] [CategoryTheory.Limits.HasZeroMorphisms C'] (S : CategoryTheory.ShortComplex C') : Prop

• mono_f : CategoryTheory.Mono S.f
• exact : S.Exact

structure GroupCohomology.IsRightExact {C' : Type u_1} [CategoryTheory.Category.{u_2, u_1} C'] [CategoryTheory.Limits.HasZeroMorphisms C'] (S : CategoryTheory.ShortComplex C') : Prop

• exact : S.Exact
• epi_g : CategoryTheory.Epi S.g

@[reducible, inline]

abbrev GroupCohomology.IsLeftExactFunctor {C' : Type u_2} {D' : Type u_3} [CategoryTheory.Category.{u_4, u_2} C'] [CategoryTheory.Category.{u_5, u_3} D'] (F : CategoryTheory.Functor C' D') : Prop

@[reducible, inline]

abbrev GroupCohomology.IsRightExactFunctor {C' : Type u_2} {D' : Type u_3} [CategoryTheory.Category.{u_4, u_2} C'] [CategoryTheory.Category.{u_5, u_3} D'] (F : CategoryTheory.Functor C' D') : Prop

@[reducible, inline]

abbrev GroupCohomology.LeftExact (C' : Type u_2) (D' : Type u_3) [CategoryTheory.Category.{u_4, u_2} C'] [CategoryTheory.Category.{u_5, u_3} D'] : Type (max (max (max u_2 u_3) u_4) u_5)

@[reducible, inline]

abbrev GroupCohomology.RightExact (C' : Type u_2) (D' : Type u_3) [CategoryTheory.Category.{u_4, u_2} C'] [CategoryTheory.Category.{u_5, u_3} D'] : Type (max (max (max u_2 u_3) u_4) u_5)

@[reducible, inline]

abbrev ChainComplexDef.ChainComplexRMod (R : Type v) [Ring R] : Type (v + 1)

@[reducible, inline]

abbrev ChainComplexDef.chainObject {R : Type v} [Ring R] (C : ChainComplexRMod R) (n : ℕ) : ModuleCat R

@[reducible, inline]

abbrev ChainComplexDef.boundaryMap {R : Type v} [Ring R] (C : ChainComplexRMod R) (n : ℕ) : chainObject C (n + 1) ⟶ chainObject C n

@[reducible, inline]

noncomputable abbrev ChainComplexDef.chainHomology {R : Type v} [Ring R] (C : ChainComplexRMod R) (n : ℕ) : ModuleCat R

noncomputable def ChainComplexDef.chainHomologyFunctor (R : Type v) [Ring R] (n : ℕ) : CategoryTheory.Functor (ChainComplexRMod R) (ModuleCat R)

@[reducible, inline]

abbrev ChainHomotopy.ChainHomotopy {R : Type v} [Ring R] {C D : ChainComplexDef.ChainComplexRMod R} (f g : C ⟶ D) : Type v

def ChainHomotopy.HomotopicChainMaps {R : Type v} [Ring R] {C D : ChainComplexDef.ChainComplexRMod R} (f g : C ⟶ D) : Prop

theorem ChainHomotopy.homotopicChainMaps_refl {R : Type v} [Ring R] {C D : ChainComplexDef.ChainComplexRMod R} (f : C ⟶ D) : HomotopicChainMaps f f

theorem ChainHomotopy.homotopicChainMaps_symm {R : Type v} [Ring R] {C D : ChainComplexDef.ChainComplexRMod R} {f g : C ⟶ D} (h : HomotopicChainMaps f g) : HomotopicChainMaps g f

theorem ChainHomotopy.homotopicChainMaps_trans {R : Type v} [Ring R] {C D : ChainComplexDef.ChainComplexRMod R} {f₁ f₂ f₃ : C ⟶ D} (h₁ : HomotopicChainMaps f₁ f₂) (h₂ : HomotopicChainMaps f₂ f₃) : HomotopicChainMaps f₁ f₃

theorem HomotopyHomology.homotopic_chain_maps_induce_equal_homology {R : Type v} [Ring R] {C D : ChainComplexDef.ChainComplexRMod R} {f g : C ⟶ D} (h : Homotopy f g) (n : ℕ) : (ChainComplexDef.chainHomologyFunctor R n).map f = (ChainComplexDef.chainHomologyFunctor R n).map g

@[reducible, inline]

abbrev DerivedFunctor.CochainComplexRMod (R : Type v) [Ring R] : Type (v + 1)

@[reducible, inline]

abbrev DerivedFunctor.cochainObject {R : Type v} [Ring R] (C : CochainComplexRMod R) (n : ℕ) : ModuleCat R

@[reducible, inline]

abbrev DerivedFunctor.coboundaryMap {R : Type v} [Ring R] (C : CochainComplexRMod R) (n : ℕ) : cochainObject C n ⟶ cochainObject C (n + 1)

theorem DerivedFunctor.coboundaryMap_comp_coboundaryMap {R : Type v} [Ring R] (C : CochainComplexRMod R) (n : ℕ) : CategoryTheory.CategoryStruct.comp (coboundaryMap C n) (coboundaryMap C (n + 1)) = 0

@[reducible, inline]

noncomputable abbrev DerivedFunctor.cochainCohomology {R : Type v} [Ring R] (C : CochainComplexRMod R) (n : ℕ) : ModuleCat R

noncomputable def DerivedFunctor.cochainCohomologyFunctor (R : Type v) [Ring R] (n : ℕ) : CategoryTheory.Functor (CochainComplexRMod R) (ModuleCat R)

noncomputable def LongExactDerived.cochainConnectingHomomorphism {R : Type v} [Ring R] {S : CategoryTheory.ShortComplex (DerivedFunctor.CochainComplexRMod R)} (hS : S.ShortExact) (n : ℕ) : DerivedFunctor.cochainCohomology S.X₃ n ⟶ DerivedFunctor.cochainCohomology S.X₁ (n + 1)

theorem LongExactDerived.cochainLES_exact {R : Type v} [Ring R] {S : CategoryTheory.ShortComplex (DerivedFunctor.CochainComplexRMod R)} (hS : S.ShortExact) (n : ℕ) : (HomologicalComplex.HomologySequence.composableArrows₅ hS n (n + 1) ⋯).Exact

theorem CochainHomotopyCohomology.homotopic_cochain_maps_cohomology_eq {R : Type v} [Ring R] {C D : DerivedFunctor.CochainComplexRMod R} {f g : C ⟶ D} (h : Homotopy f g) (n : ℕ) : HomologicalComplex.homologyMap f n = HomologicalComplex.homologyMap g n

@[reducible, inline]

abbrev Resolution.ProjectiveResolutionRMod {R : Type v} [Ring R] (M : ModuleCat R) : Type (v + 1)

@[reducible, inline]

abbrev Resolution.ProjectiveResolutionRMod.complex' {R : Type v} [Ring R] {M : ModuleCat R} (P : ProjectiveResolutionRMod M) : ChainComplex (ModuleCat R) ℕ

@[reducible, inline]

abbrev Resolution.InjectiveResolutionRMod {R : Type v} [Ring R] (M : ModuleCat R) : Type (v + 1)

theorem Resolution.ProjectiveResolutionRMod.exactAt_succ {R : Type v} [Ring R] {M : ModuleCat R} (P : ProjectiveResolutionRMod M) (n : ℕ) : HomologicalComplex.ExactAt P.complex (n + 1)

theorem Resolution.InjectiveResolutionRMod.exactAt_succ {R : Type v} [Ring R] {M : ModuleCat R} (I : InjectiveResolutionRMod M) (n : ℕ) : HomologicalComplex.ExactAt I.cocomplex (n + 1)

def HomFunctorHomotopy.homotopyOp {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} (h : Homotopy f g) : Homotopy ((HomologicalComplex.opFunctor V c).map f.op) ((HomologicalComplex.opFunctor V c).map g.op)

noncomputable def HomFunctorHomotopy.homStarFunctor {R : Type v} [Ring R] (A : ModuleCat R) : CategoryTheory.Functor (ChainComplexDef.ChainComplexRMod R)ᵒᵖ (HomologicalComplex AddCommGrpCat (ComplexShape.down ℕ).symm)

theorem HomFunctorHomotopy.hom_functor_preserves_homotopy {R : Type v} [Ring R] (A : ModuleCat R) {C D : ChainComplexDef.ChainComplexRMod R} {f g : C ⟶ D} (hfg : Nonempty (Homotopy f g)) : Nonempty (Homotopy ((homStarFunctor A).map f.op) ((homStarFunctor A).map g.op))