noncomputable def GroupCohomology.corollary_23_28_homology_ind_H0_iso {k : Type u} [CommRing k] {G : Type u} [Group G] [DecidableEq G] [Fintype G] (A : Rep.{u, u, u} k ↥⊥) : groupHomology (Rep.ind ⊥.subtype A) 0 ≅ groupHomology A 0

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

theorem GroupCohomology.corollary_23_28_homology_ind_vanishing {k : Type u} [CommRing k] {G : Type u} [Group G] [DecidableEq G] [Fintype G] (A : Rep.{u, u, u} k ↥⊥) (n : ℕ) : CategoryTheory.Limits.IsZero (groupHomology (Rep.ind ⊥.subtype A) (n + 1))

theorem GroupCohomology.corollary_23_28_cohomology_coind_vanishing {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype 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.corollary_23_28_cohomology_ind_H0_iso {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k ↥⊥) : groupCohomology (Rep.ind ⊥.subtype A) 0 ≅ groupCohomology A 0

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

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

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

theorem GroupCohomology.induced_coinduced_cohomology_vanishing {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k ↥⊥) : Nonempty (groupHomology (Rep.ind ⊥.subtype A) 0 ≅ groupHomology A 0) ∧ Nonempty (groupCohomology (Rep.ind ⊥.subtype A) 0 ≅ groupCohomology A 0) ∧ Nonempty (groupHomology (Rep.coind.{u, u, u, u} ⊥.subtype A) 0 ≅ groupHomology A 0) ∧ Nonempty (groupCohomology (Rep.coind.{u, u, u, u} ⊥.subtype A) 0 ≅ groupCohomology A 0) ∧ (∀ (n : ℕ), CategoryTheory.Limits.IsZero (groupHomology (Rep.ind ⊥.subtype A) (n + 1))) ∧ (∀ (n : ℕ), CategoryTheory.Limits.IsZero (groupCohomology (Rep.ind ⊥.subtype A) (n + 1))) ∧ (∀ (n : ℕ), CategoryTheory.Limits.IsZero (groupHomology (Rep.coind.{u, u, u, u} ⊥.subtype A) (n + 1))) ∧ ∀ (n : ℕ), CategoryTheory.Limits.IsZero (groupCohomology (Rep.coind.{u, u, u, u} ⊥.subtype A) (n + 1))