The low-degree homology of a k-linear G-representation #
Let k be a commutative ring and G a group. This file contains specialised API for
the cycles and group homology of a k-linear G-representation A in degrees 0, 1 and 2.
In Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean, we define the nth group
homology of A to be the homology of a complex inhomogeneousChains A, whose objects are
(Fin n →₀ G) → A; this is unnecessarily unwieldy in low degree.
Given an additive abelian group A with an appropriate scalar action of G, we provide support
for turning a finsupp f : G →₀ A satisfying the 1-cycle identity into an element of the
cycles₁ of the representation on A corresponding to the scalar action. We also do this for
0-boundaries, 1-boundaries, 2-cycles and 2-boundaries.
The file also contains an identification between the definitions in
Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean, groupHomology.cycles A n, and
the cyclesₙ in this file for n = 1, 2, as well as an isomorphism
groupHomology.cycles A 0 ≅ A.V.
Moreover, we provide API for the natural maps cyclesₙ A → Hn A for n = 1, 2.
We show that when the representation on A is trivial, H₁(G, A) ≃+ Gᵃᵇ ⊗[ℤ] A.
Main definitions #
groupHomology.H0Iso A: isomorphism betweenH₀(G, A)and the coinvariantsA_Gof theG-representation onA.groupHomology.H1π A: epimorphism from the 1-cycles (i.e.Z₁(G, A) := Ker(d₀ : (G →₀ A) → A) toH₁(G, A).groupHomology.H2π A: epimorphism from the 2-cycles (i.e.Z₂(G, A) := Ker(d₁ : (G² →₀ A) → (G →₀ A)) toH₂(G, A).groupHomology.H1AddEquivOfIsTrivial: an isomorphismH₁(G, A) ≃+ Gᵃᵇ ⊗[ℤ] Awhen the representation onAis trivial.
noncomputable def
groupHomology.chainsIso₀
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The 0th object in the complex of inhomogeneous chains of A : Rep k G is isomorphic
to A as a k-module.
Instances For
noncomputable def
groupHomology.chainsIso₁
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The 1st object in the complex of inhomogeneous chains of A : Rep k G is isomorphic
to G →₀ A as a k-module.
Instances For
noncomputable def
groupHomology.chainsIso₂
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The 2nd object in the complex of inhomogeneous chains of A : Rep k G is isomorphic
to G² →₀ A as a k-module.
Instances For
noncomputable def
groupHomology.chainsIso₃
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The 3rd object in the complex of inhomogeneous chains of A : Rep k G is isomorphic
to G³ → A as a k-module.
Instances For
The 0th differential in the complex of inhomogeneous chains of A : Rep k G, as a
k-linear map (G →₀ A) → A. It is defined by single g a ↦ ρ_A(g⁻¹)(a) - a.
Instances For
@[simp]
theorem
groupHomology.d₁₀_single
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(g : G)
(a : ↑A)
:
theorem
groupHomology.d₁₀_single_one
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(a : ↑A)
:
((CategoryTheory.ConcreteCategory.hom (d₁₀ A)) fun₀ | 1 => a) = 0
theorem
groupHomology.d₁₀_single_inv
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(g : G)
(a : ↑A)
:
theorem
groupHomology.range_d₁₀_eq_coinvariantsKer
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
@[simp]
theorem
groupHomology.d₁₀_comp_coinvariantsMk
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
CategoryTheory.CategoryStruct.comp (d₁₀ A) ((Rep.coinvariantsMk k G).app A) = 0
@[simp]
theorem
groupHomology.d₁₀_comp_coinvariantsMk_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : (Rep.coinvariantsFunctor k G).obj A ⟶ Z)
:
@[simp]
theorem
groupHomology.d₁₀_comp_coinvariantsMk_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : G →₀ ↑A)
:
(Representation.Coinvariants.mk A.ρ) ((CategoryTheory.ConcreteCategory.hom (d₁₀ A)) x) = 0 x
noncomputable def
groupHomology.chains₁ToCoinvariantsKer
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The 0th differential in the complex of inhomogeneous chains of a G-representation A as a
linear map into the k-submodule of A spanned by elements of the form
ρ(g)(x) - x, g ∈ G, x ∈ A.
Instances For
theorem
groupHomology.chains₁ToCoinvariantsKer_surjective
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (chains₁ToCoinvariantsKer A))
@[simp]
theorem
groupHomology.d₁₀_eq_zero_of_isTrivial
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
[A.IsTrivial]
:
d₁₀ A = 0
The 1st differential in the complex of inhomogeneous chains of A : Rep k G, as a
k-linear map (G² →₀ A) → (G →₀ A). It is defined by
a·(g₁, g₂) ↦ ρ_A(g₁⁻¹)(a)·g₂ - a·g₁g₂ + a·g₁.
Instances For
theorem
groupHomology.d₂₁_single_one_fst
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(g : G)
(a : ↑A)
:
theorem
groupHomology.d₂₁_single_one_snd
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(g : G)
(a : ↑A)
:
The 2nd differential in the complex of inhomogeneous chains of A : Rep k G, as a
k-linear map (G³ →₀ A) → (G² →₀ A). It is defined by
a·(g₁, g₂, g₃) ↦ ρ_A(g₁⁻¹)(a)·(g₂, g₃) - a·(g₁g₂, g₃) + a·(g₁, g₂g₃) - a·(g₁, g₂).
Instances For
@[simp]
theorem
groupHomology.d₃₂_single
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(g : G × G × G)
(a : ↑A)
:
theorem
groupHomology.comp_d₁₀_eq
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
CategoryTheory.CategoryStruct.comp (chainsIso₁ A).hom (d₁₀ A) = CategoryTheory.CategoryStruct.comp ((inhomogeneousChains A).d 1 0) (chainsIso₀ A).hom
Let C(G, A) denote the complex of inhomogeneous chains of A : Rep k G. This lemma
says d₁₀ gives a simpler expression for the 0th differential: that is, the following
square commutes:
C₁(G, A) --d 1 0--> C₀(G, A)
| |
| |
| |
v v
(G →₀ A) ----d₁₀----> A
where the vertical arrows are chainsIso₁ and chainsIso₀ respectively.
@[simp]
theorem
groupHomology.eq_d₁₀_comp_inv
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
CategoryTheory.CategoryStruct.comp (chainsIso₁ A).inv ((inhomogeneousChains A).d 1 0) = CategoryTheory.CategoryStruct.comp (d₁₀ A) (chainsIso₀ A).inv
@[simp]
theorem
groupHomology.eq_d₁₀_comp_inv_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : (inhomogeneousChains A).X 0 ⟶ Z)
:
@[simp]
theorem
groupHomology.eq_d₁₀_comp_inv_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : G →₀ ↑A)
:
(CategoryTheory.ConcreteCategory.hom ((inhomogeneousChains A).d 1 0))
((CategoryTheory.ConcreteCategory.hom (chainsIso₁ A).inv) x) = (CategoryTheory.ConcreteCategory.hom (chainsIso₀ A).inv) ((CategoryTheory.ConcreteCategory.hom (d₁₀ A)) x)
theorem
groupHomology.comp_d₂₁_eq
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
CategoryTheory.CategoryStruct.comp (chainsIso₂ A).hom (d₂₁ A) = CategoryTheory.CategoryStruct.comp ((inhomogeneousChains A).d 2 1) (chainsIso₁ A).hom
Let C(G, A) denote the complex of inhomogeneous chains of A : Rep k G. This lemma
says d₂₁ gives a simpler expression for the 1st differential: that is, the following
square commutes:
C₂(G, A) --d 2 1--> C₁(G, A)
| |
| |
| |
v v
(G² →₀ A) --d₂₁--> (G →₀ A)
where the vertical arrows are chainsIso₂ and chainsIso₁ respectively.
@[simp]
theorem
groupHomology.eq_d₂₁_comp_inv
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
CategoryTheory.CategoryStruct.comp (chainsIso₂ A).inv ((inhomogeneousChains A).d 2 1) = CategoryTheory.CategoryStruct.comp (d₂₁ A) (chainsIso₁ A).inv
@[simp]
theorem
groupHomology.eq_d₂₁_comp_inv_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : (inhomogeneousChains A).X 1 ⟶ Z)
:
@[simp]
theorem
groupHomology.eq_d₂₁_comp_inv_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : G × G →₀ ↑A)
:
(CategoryTheory.ConcreteCategory.hom ((inhomogeneousChains A).d 2 1))
((CategoryTheory.ConcreteCategory.hom (chainsIso₂ A).inv) x) = (CategoryTheory.ConcreteCategory.hom (chainsIso₁ A).inv) ((CategoryTheory.ConcreteCategory.hom (d₂₁ A)) x)
theorem
groupHomology.comp_d₃₂_eq
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
CategoryTheory.CategoryStruct.comp (chainsIso₃ A).hom (d₃₂ A) = CategoryTheory.CategoryStruct.comp ((inhomogeneousChains A).d 3 2) (chainsIso₂ A).hom
Let C(G, A) denote the complex of inhomogeneous chains of A : Rep k G. This lemma
says d₃₂ gives a simpler expression for the 2nd differential: that is, the following
square commutes:
C₃(G, A) --d 3 2--> C₂(G, A)
| |
| |
| |
v v
(G³ →₀ A) --d₃₂--> (G² →₀ A)
where the vertical arrows are chainsIso₃ and chainsIso₂ respectively.
@[simp]
theorem
groupHomology.eq_d₃₂_comp_inv
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
CategoryTheory.CategoryStruct.comp (chainsIso₃ A).inv ((inhomogeneousChains A).d 3 2) = CategoryTheory.CategoryStruct.comp (d₃₂ A) (chainsIso₂ A).inv
@[simp]
theorem
groupHomology.eq_d₃₂_comp_inv_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : (inhomogeneousChains A).X 2 ⟶ Z)
:
@[simp]
theorem
groupHomology.eq_d₃₂_comp_inv_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : G × G × G →₀ ↑A)
:
(CategoryTheory.ConcreteCategory.hom ((inhomogeneousChains A).d 3 2))
((CategoryTheory.ConcreteCategory.hom (chainsIso₃ A).inv) x) = (CategoryTheory.ConcreteCategory.hom (chainsIso₂ A).inv) ((CategoryTheory.ConcreteCategory.hom (d₃₂ A)) x)
@[simp]
theorem
groupHomology.d₂₁_comp_d₁₀
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
CategoryTheory.CategoryStruct.comp (d₂₁ A) (d₁₀ A) = 0
@[simp]
theorem
groupHomology.d₂₁_comp_d₁₀_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : ModuleCat.of k ↑A ⟶ Z)
:
@[simp]
theorem
groupHomology.d₂₁_comp_d₁₀_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : G × G →₀ ↑A)
:
(CategoryTheory.ConcreteCategory.hom (d₁₀ A)) ((CategoryTheory.ConcreteCategory.hom (d₂₁ A)) x) = 0
@[simp]
theorem
groupHomology.d₃₂_comp_d₂₁
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
CategoryTheory.CategoryStruct.comp (d₃₂ A) (d₂₁ A) = 0
@[simp]
theorem
groupHomology.d₃₂_comp_d₂₁_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : ModuleCat.of k (G →₀ ↑A) ⟶ Z)
:
@[simp]
theorem
groupHomology.d₃₂_comp_d₂₁_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : G × G × G →₀ ↑A)
:
(CategoryTheory.ConcreteCategory.hom (d₂₁ A)) ((CategoryTheory.ConcreteCategory.hom (d₃₂ A)) x) = 0
noncomputable def
groupHomology.shortComplexH0
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The (exact) short complex (G →₀ A) ⟶ A ⟶ A.ρ.coinvariants.
Instances For
theorem
groupHomology.shortComplexH0_g
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
(shortComplexH0 A).g = (Rep.coinvariantsMk k G).app A
theorem
groupHomology.shortComplexH0_f
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
(shortComplexH0 A).f = d₁₀ A
noncomputable def
groupHomology.shortComplexH1
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The short complex (G² →₀ A) --d₂₁--> (G →₀ A) --d₁₀--> A.
Instances For
theorem
groupHomology.shortComplexH1_g
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
(shortComplexH1 A).g = d₁₀ A
theorem
groupHomology.shortComplexH1_f
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
(shortComplexH1 A).f = d₂₁ A
noncomputable def
groupHomology.shortComplexH2
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The short complex (G³ →₀ A) --d₃₂--> (G² →₀ A) --d₂₁--> (G →₀ A).
Instances For
theorem
groupHomology.shortComplexH2_g
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
(shortComplexH2 A).g = d₂₁ A
theorem
groupHomology.shortComplexH2_f
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
(shortComplexH2 A).f = d₃₂ A
noncomputable def
groupHomology.cycles₁
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The 1-cycles Z₁(G, A) of A : Rep k G, defined as the kernel of the map
(G →₀ A) → A defined by single g a ↦ ρ_A(g⁻¹)(a) - a.
Instances For
noncomputable def
groupHomology.cycles₂
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The 2-cycles Z₂(G, A) of A : Rep k G, defined as the kernel of the map
(G² →₀ A) → (G →₀ A) defined by a·(g₁, g₂) ↦ ρ_A(g₁⁻¹)(a)·g₂ - a·g₁g₂ + a·g₁.
Instances For
theorem
groupHomology.single_mem_cycles₁_iff
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(g : G)
(a : ↑A)
:
theorem
groupHomology.single_mem_cycles₁_of_mem_invariants
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(g : G)
(a : ↑A)
(ha : a ∈ A.ρ.invariants)
:
theorem
groupHomology.d₂₁_apply_mem_cycles₁
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(x : G × G →₀ ↑A)
:
(CategoryTheory.ConcreteCategory.hom (d₂₁ A)) x ∈ cycles₁ A
theorem
groupHomology.cycles₁_eq_top_of_isTrivial
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
[A.IsTrivial]
:
noncomputable def
groupHomology.cycles₁IsoOfIsTrivial
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
[A.IsTrivial]
:
The natural inclusion Z₁(G, A) ⟶ C₁(G, A) is an isomorphism when the representation
on A is trivial.
Instances For
@[simp]
theorem
groupHomology.cycles₁IsoOfIsTrivial_hom_apply
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
[A.IsTrivial]
(x : ↥(cycles₁ A))
:
(CategoryTheory.ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).hom) x = ↑x
@[simp]
theorem
groupHomology.cycles₁IsoOfIsTrivial_inv_apply
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
[A.IsTrivial]
(x : G →₀ ↑A)
:
↑((CategoryTheory.ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) x) = x
theorem
groupHomology.d₃₂_apply_mem_cycles₂
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(x : G × G × G →₀ ↑A)
:
(CategoryTheory.ConcreteCategory.hom (d₃₂ A)) x ∈ cycles₂ A
noncomputable def
groupHomology.boundaries₁
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The 1-boundaries B₁(G, A) of A : Rep k G, defined as the image of the map
(G² →₀ A) → (G →₀ A) defined by a·(g₁, g₂) ↦ ρ_A(g₁⁻¹)(a)·g₂ - a·g₁g₂ + a·g₁.
Instances For
noncomputable def
groupHomology.boundaries₂
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The 2-boundaries B₂(G, A) of A : Rep k G, defined as the image of the map
(G³ →₀ A) → (G² →₀ A) defined by
a·(g₁, g₂, g₃) ↦ ρ_A(g₁⁻¹)(a)·(g₂, g₃) - a·(g₁g₂, g₃) + a·(g₁, g₂g₃) - a·(g₁, g₂).
Instances For
theorem
groupHomology.mem_cycles₁_of_mem_boundaries₁
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(f : G →₀ ↑A)
(h : f ∈ boundaries₁ A)
:
f ∈ cycles₁ A
theorem
groupHomology.boundaries₁_le_cycles₁
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
@[reducible, inline]
noncomputable abbrev
groupHomology.boundariesToCycles₁
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The natural inclusion B₁(G, A) →ₗ[k] Z₁(G, A).
Instances For
@[simp]
theorem
groupHomology.boundariesToCycles₁_apply
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(x : ↥(boundaries₁ A))
:
↑((boundariesToCycles₁ A) x) = ↑x
theorem
groupHomology.single_one_mem_boundaries₁
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(a : ↑A)
:
(fun₀ | 1 => a) ∈ boundaries₁ A
theorem
groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(g : G)
(a : ↑A)
:
theorem
groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(g : G)
(a : ↑A)
:
theorem
groupHomology.mem_cycles₂_of_mem_boundaries₂
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(x : G × G →₀ ↑A)
(h : x ∈ boundaries₂ A)
:
x ∈ cycles₂ A
theorem
groupHomology.boundaries₂_le_cycles₂
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
@[reducible, inline]
noncomputable abbrev
groupHomology.boundariesToCycles₂
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The natural inclusion B₂(G, A) →ₗ[k] Z₂(G, A).
Instances For
@[simp]
theorem
groupHomology.boundariesToCycles₂_apply
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(x : ↥(boundaries₂ A))
:
↑((boundariesToCycles₂ A) x) = ↑x
theorem
groupHomology.single_one_fst_sub_single_one_fst_mem_boundaries₂
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(g h : G)
(a : ↑A)
:
theorem
groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(g h : G)
(a : ↑A)
:
theorem
groupHomology.single_one_snd_sub_single_one_fst_mem_boundaries₂
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(g h : G)
(a : ↑A)
:
theorem
groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(g h : G)
(a : ↑A)
:
def
groupHomology.IsCycle₁
{G : Type u_1}
{A : Type u_2}
[Inv G]
[AddCommGroup A]
[SMul G A]
(x : G →₀ A)
:
A finsupp ∑ aᵢ·gᵢ : G →₀ A satisfies the 1-cycle condition if ∑ gᵢ⁻¹ • aᵢ = ∑ aᵢ.
Instances For
def
groupHomology.IsCycle₂
{G : Type u_1}
{A : Type u_2}
[Mul G]
[Inv G]
[AddCommGroup A]
[SMul G A]
(x : G × G →₀ A)
:
A finsupp ∑ aᵢ·(gᵢ, hᵢ) : G × G →₀ A satisfies the 2-cycle condition if
∑ (gᵢ⁻¹ • aᵢ)·hᵢ + aᵢ·gᵢ = ∑ aᵢ·gᵢhᵢ.
Instances For
@[simp]
theorem
groupHomology.single_isCycle₁_iff
{G : Type u_1}
{A : Type u_2}
[Group G]
[AddCommGroup A]
[DistribMulAction G A]
(g : G)
(a : A)
:
theorem
groupHomology.single_isCycle₁_of_mem_fixedPoints
{G : Type u_1}
{A : Type u_2}
[Group G]
[AddCommGroup A]
[DistribMulAction G A]
(g : G)
(a : A)
(ha : a ∈ MulAction.fixedPoints G A)
:
def
groupHomology.IsBoundary₀
(G : Type u_1)
{A : Type u_2}
[Inv G]
[AddCommGroup A]
[SMul G A]
(a : A)
:
A term x : A satisfies the 0-boundary condition if there exists a finsupp
∑ aᵢ·gᵢ : G →₀ A such that ∑ gᵢ⁻¹ • aᵢ - aᵢ = x.
Instances For
def
groupHomology.IsBoundary₁
{G : Type u_1}
{A : Type u_2}
[Mul G]
[Inv G]
[AddCommGroup A]
[SMul G A]
(x : G →₀ A)
:
A finsupp x : G →₀ A satisfies the 1-boundary condition if there's a finsupp
∑ aᵢ·(gᵢ, hᵢ) : G × G →₀ A such that ∑ (gᵢ⁻¹ • aᵢ)·hᵢ - aᵢ·gᵢhᵢ + aᵢ·gᵢ = x.
Instances For
def
groupHomology.IsBoundary₂
{G : Type u_1}
{A : Type u_2}
[Mul G]
[Inv G]
[AddCommGroup A]
[SMul G A]
(x : G × G →₀ A)
:
A finsupp x : G × G →₀ A satisfies the 2-boundary condition if there's a finsupp
∑ aᵢ·(gᵢ, hᵢ, jᵢ) : G × G × G →₀ A such that
∑ (gᵢ⁻¹ • aᵢ)·(hᵢ, jᵢ) - aᵢ·(gᵢhᵢ, jᵢ) + aᵢ·(gᵢ, hᵢjᵢ) - aᵢ·(gᵢ, hᵢ) = x.
Instances For
theorem
groupHomology.isBoundary₀_iff
(G : Type u_1)
{A : Type u_2}
[Group G]
[AddCommGroup A]
[DistribMulAction G A]
(a : A)
:
IsBoundary₀ G a ↔ ∃ (x : G →₀ A), (x.sum fun (g : G) (z : A) => g • z - z) = a
theorem
groupHomology.isBoundary₁_iff
{G : Type u_1}
{A : Type u_2}
[Group G]
[AddCommGroup A]
[DistribMulAction G A]
(x : G →₀ A)
:
theorem
groupHomology.isBoundary₂_iff
{G : Type u_1}
{A : Type u_2}
[Group G]
[AddCommGroup A]
[DistribMulAction G A]
(x : G × G →₀ A)
:
def
groupHomology.coinvariantsKerOfIsBoundary₀
{k G A : Type u}
[CommRing k]
[Group G]
[AddCommGroup A]
[Module k A]
[DistribMulAction G A]
[SMulCommClass G k A]
(x : A)
(hx : IsBoundary₀ G x)
:
Given a k-module A with a compatible DistribMulAction of G, and a term
x : A satisfying the 0-boundary condition, this produces an element of the kernel of the quotient
map A → A_G for the representation on A induced by the DistribMulAction.
Instances For
@[simp]
theorem
groupHomology.coinvariantsKerOfIsBoundary₀_coe
{k G A : Type u}
[CommRing k]
[Group G]
[AddCommGroup A]
[Module k A]
[DistribMulAction G A]
[SMulCommClass G k A]
(x : A)
(hx : IsBoundary₀ G x)
:
↑(coinvariantsKerOfIsBoundary₀ x hx) = x
theorem
groupHomology.isBoundary₀_of_mem_coinvariantsKer
{k G A : Type u}
[CommRing k]
[Group G]
[AddCommGroup A]
[Module k A]
[DistribMulAction G A]
[SMulCommClass G k A]
(x : A)
(hx : x ∈ Representation.Coinvariants.ker (Representation.ofDistribMulAction k G A))
:
IsBoundary₀ G x
def
groupHomology.cyclesOfIsCycle₁
{k G A : Type u}
[CommRing k]
[Group G]
[AddCommGroup A]
[Module k A]
[DistribMulAction G A]
[SMulCommClass G k A]
(x : G →₀ A)
(hx : IsCycle₁ x)
:
↥(cycles₁ (Rep.ofDistribMulAction k G A))
Given a k-module A with a compatible DistribMulAction of G, and a finsupp
x : G →₀ A satisfying the 1-cycle condition, produces a 1-cycle for the representation on
A induced by the DistribMulAction.
Instances For
@[simp]
theorem
groupHomology.cyclesOfIsCycle₁_coe
{k G A : Type u}
[CommRing k]
[Group G]
[AddCommGroup A]
[Module k A]
[DistribMulAction G A]
[SMulCommClass G k A]
(x : G →₀ A)
(hx : IsCycle₁ x)
:
↑(cyclesOfIsCycle₁ x hx) = x
theorem
groupHomology.isCycle₁_of_mem_cycles₁
{k G A : Type u}
[CommRing k]
[Group G]
[AddCommGroup A]
[Module k A]
[DistribMulAction G A]
[SMulCommClass G k A]
(x : G →₀ A)
(hx : x ∈ cycles₁ (Rep.ofDistribMulAction k G A))
:
IsCycle₁ x
def
groupHomology.boundariesOfIsBoundary₁
{k G A : Type u}
[CommRing k]
[Group G]
[AddCommGroup A]
[Module k A]
[DistribMulAction G A]
[SMulCommClass G k A]
(x : G →₀ A)
(hx : IsBoundary₁ x)
:
↥(boundaries₁ (Rep.ofDistribMulAction k G A))
Given a k-module A with a compatible DistribMulAction of G, and a finsupp
x : G →₀ A satisfying the 1-boundary condition, produces a 1-boundary for the representation
on A induced by the DistribMulAction.
Instances For
@[simp]
theorem
groupHomology.boundariesOfIsBoundary₁_coe
{k G A : Type u}
[CommRing k]
[Group G]
[AddCommGroup A]
[Module k A]
[DistribMulAction G A]
[SMulCommClass G k A]
(x : G →₀ A)
(hx : IsBoundary₁ x)
:
↑(boundariesOfIsBoundary₁ x hx) = x
theorem
groupHomology.isBoundary₁_of_mem_boundaries₁
{k G A : Type u}
[CommRing k]
[Group G]
[AddCommGroup A]
[Module k A]
[DistribMulAction G A]
[SMulCommClass G k A]
(x : G →₀ A)
(hx : x ∈ boundaries₁ (Rep.ofDistribMulAction k G A))
:
def
groupHomology.cyclesOfIsCycle₂
{k G A : Type u}
[CommRing k]
[Group G]
[AddCommGroup A]
[Module k A]
[DistribMulAction G A]
[SMulCommClass G k A]
(x : G × G →₀ A)
(hx : IsCycle₂ x)
:
↥(cycles₂ (Rep.ofDistribMulAction k G A))
Given a k-module A with a compatible DistribMulAction of G, and a finsupp
x : G × G →₀ A satisfying the 2-cycle condition, produces a 2-cycle for the representation on
A induced by the DistribMulAction.
Instances For
@[simp]
theorem
groupHomology.cyclesOfIsCycle₂_coe
{k G A : Type u}
[CommRing k]
[Group G]
[AddCommGroup A]
[Module k A]
[DistribMulAction G A]
[SMulCommClass G k A]
(x : G × G →₀ A)
(hx : IsCycle₂ x)
:
↑(cyclesOfIsCycle₂ x hx) = x
theorem
groupHomology.isCycle₂_of_mem_cycles₂
{k G A : Type u}
[CommRing k]
[Group G]
[AddCommGroup A]
[Module k A]
[DistribMulAction G A]
[SMulCommClass G k A]
(x : G × G →₀ A)
(hx : x ∈ cycles₂ (Rep.ofDistribMulAction k G A))
:
IsCycle₂ x
def
groupHomology.boundariesOfIsBoundary₂
{k G A : Type u}
[CommRing k]
[Group G]
[AddCommGroup A]
[Module k A]
[DistribMulAction G A]
[SMulCommClass G k A]
(x : G × G →₀ A)
(hx : IsBoundary₂ x)
:
↥(boundaries₂ (Rep.ofDistribMulAction k G A))
Given a k-module A with a compatible DistribMulAction of G, and a finsupp
x : G × G →₀ A satisfying the 2-boundary condition, produces a 2-boundary for the
representation on A induced by the DistribMulAction.
Instances For
@[simp]
theorem
groupHomology.boundariesOfIsBoundary₂_coe
{k G A : Type u}
[CommRing k]
[Group G]
[AddCommGroup A]
[Module k A]
[DistribMulAction G A]
[SMulCommClass G k A]
(x : G × G →₀ A)
(hx : IsBoundary₂ x)
:
↑(boundariesOfIsBoundary₂ x hx) = x
theorem
groupHomology.isBoundary₂_of_mem_boundaries₂
{k G A : Type u}
[CommRing k]
[Group G]
[AddCommGroup A]
[Module k A]
[DistribMulAction G A]
[SMulCommClass G k A]
(x : G × G →₀ A)
(hx : x ∈ boundaries₂ (Rep.ofDistribMulAction k G A))
:
instance
groupHomology.instEpiModuleCatGShortComplexH0
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
theorem
groupHomology.shortComplexH0_exact
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
(shortComplexH0 A).Exact
noncomputable def
groupHomology.cyclesIso₀
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The 0-cycles of the complex of inhomogeneous chains of A are isomorphic to A.
Instances For
@[simp]
theorem
groupHomology.cyclesIso₀_inv_comp_iCycles
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
CategoryTheory.CategoryStruct.comp (cyclesIso₀ A).inv (iCycles A 0) = (chainsIso₀ A).inv
@[simp]
theorem
groupHomology.cyclesIso₀_inv_comp_iCycles_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : (inhomogeneousChains A).X 0 ⟶ Z)
:
@[simp]
theorem
groupHomology.cyclesIso₀_inv_comp_iCycles_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↑A)
:
(CategoryTheory.ConcreteCategory.hom (iCycles A 0)) ((CategoryTheory.ConcreteCategory.hom (cyclesIso₀ A).inv) x) = (CategoryTheory.ConcreteCategory.hom (chainsIso₀ A).inv) x
noncomputable def
groupHomology.d₁₀ArrowIso
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The arrow (G →₀ A) --d₁₀--> A is isomorphic to the differential
(inhomogeneousChains A).d 1 0 of the complex of inhomogeneous chains of A.
Instances For
@[simp]
theorem
groupHomology.d₁₀ArrowIso_hom_right
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
(d₁₀ArrowIso A).hom.right = (chainsIso₀ A).hom
@[simp]
theorem
groupHomology.d₁₀ArrowIso_inv_left
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
(d₁₀ArrowIso A).inv.left = (chainsIso₁ A).inv
@[simp]
theorem
groupHomology.d₁₀ArrowIso_hom_left
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
(d₁₀ArrowIso A).hom.left = (chainsIso₁ A).hom
@[simp]
theorem
groupHomology.d₁₀ArrowIso_inv_right
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
(d₁₀ArrowIso A).inv.right = (chainsIso₀ A).inv
noncomputable def
groupHomology.opcyclesIso₀
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The 0-cycles of the complex of inhomogeneous chains of A are isomorphic to
A.ρ.coinvariants, which is a simpler type.
Instances For
@[simp]
theorem
groupHomology.pOpcycles_comp_opcyclesIso_hom
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
@[simp]
theorem
groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : (Rep.coinvariantsFunctor k G).obj A ⟶ Z)
:
@[simp]
theorem
groupHomology.pOpcycles_comp_opcyclesIso_hom_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↑((inhomogeneousChains A).X 0))
:
@[simp]
theorem
groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
@[simp]
theorem
groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : HomologicalComplex.opcycles (inhomogeneousChains A) 0 ⟶ Z)
:
@[simp]
theorem
groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↑((CategoryTheory.forget₂ (Rep.{u, u, u} k G) (ModuleCat k)).obj A))
:
theorem
groupHomology.cyclesMk₀_eq
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↑A)
:
cyclesMk 0 0 cyclesMk₀_eq._proof_1 ((CategoryTheory.ConcreteCategory.hom (chainsIso₀ A).inv) x) ⋯ = (CategoryTheory.ConcreteCategory.hom (cyclesIso₀ A).inv) x
noncomputable def
groupHomology.isoShortComplexH1
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The short complex (G² →₀ A) --d₂₁--> (G →₀ A) --d₁₀--> A is isomorphic to the 1st
short complex associated to the complex of inhomogeneous chains of A.
Instances For
@[simp]
theorem
groupHomology.isoShortComplexH1_inv
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
(isoShortComplexH1 A).inv = CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.homMk (chainsIso₂ A).inv (chainsIso₁ A).inv (chainsIso₀ A).inv ⋯ ⋯)
((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.down ℕ) 2 1 0 isoShortComplexH1._proof_1
isoShortComplexH1._proof_2).inv.app
(inhomogeneousChains A))
@[simp]
theorem
groupHomology.isoShortComplexH1_hom
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
(isoShortComplexH1 A).hom = CategoryTheory.CategoryStruct.comp
((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.down ℕ) 2 1 0 isoShortComplexH1._proof_1
isoShortComplexH1._proof_2).hom.app
(inhomogeneousChains A))
(CategoryTheory.ShortComplex.isoMk (chainsIso₂ A) (chainsIso₁ A) (chainsIso₀ A) ⋯ ⋯).hom
noncomputable def
groupHomology.isoCycles₁
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The 1-cycles of the complex of inhomogeneous chains of A are isomorphic to
cycles₁ A, which is a simpler type.
Instances For
@[simp]
theorem
groupHomology.isoCycles₁_hom_comp_i
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
@[simp]
theorem
groupHomology.isoCycles₁_hom_comp_i_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : (shortComplexH1 A).X₂ ⟶ Z)
:
@[simp]
theorem
groupHomology.isoCycles₁_hom_comp_i_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↑(cycles A 1))
:
(ModuleCat.Hom.hom (shortComplexH1 A).g).ker.subtype ((CategoryTheory.ConcreteCategory.hom (isoCycles₁ A).hom) x) = (CategoryTheory.ConcreteCategory.hom (chainsIso₁ A).hom) ((CategoryTheory.ConcreteCategory.hom (iCycles A 1)) x)
@[simp]
theorem
groupHomology.isoCycles₁_inv_comp_iCycles
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
@[simp]
theorem
groupHomology.isoCycles₁_inv_comp_iCycles_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : (inhomogeneousChains A).X 1 ⟶ Z)
:
@[simp]
theorem
groupHomology.isoCycles₁_inv_comp_iCycles_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↥(cycles₁ A))
:
@[simp]
theorem
groupHomology.toCycles_comp_isoCycles₁_hom
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
@[simp]
theorem
groupHomology.toCycles_comp_isoCycles₁_hom_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : ModuleCat.of k ↥(cycles₁ A) ⟶ Z)
:
@[simp]
theorem
groupHomology.toCycles_comp_isoCycles₁_hom_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↑((inhomogeneousChains A).X 2))
:
(CategoryTheory.ConcreteCategory.hom (isoCycles₁ A).hom) ((CategoryTheory.ConcreteCategory.hom (toCycles A 2 1)) x) = (shortComplexH1 A).moduleCatToCycles ((CategoryTheory.ConcreteCategory.hom (chainsIso₂ A).hom) x)
theorem
groupHomology.cyclesMk₁_eq
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↥(cycles₁ A))
:
cyclesMk 1 0 cyclesMk₁_eq._proof_1 ((CategoryTheory.ConcreteCategory.hom (chainsIso₁ A).inv) ↑x) ⋯ = (CategoryTheory.ConcreteCategory.hom (isoCycles₁ A).inv) x
noncomputable def
groupHomology.isoShortComplexH2
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The short complex (G³ →₀ A) --d₃₂--> (G² →₀ A) --d₂₁--> (G →₀ A) is isomorphic to the 2nd
short complex associated to the complex of inhomogeneous chains of A.
Instances For
@[simp]
theorem
groupHomology.isoShortComplexH2_inv
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
(isoShortComplexH2 A).inv = CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.homMk (chainsIso₃ A).inv (chainsIso₂ A).inv (chainsIso₁ A).inv ⋯ ⋯)
((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.down ℕ) 3 2 1 isoShortComplexH2._proof_1
isoShortComplexH2._proof_2).inv.app
(inhomogeneousChains A))
@[simp]
theorem
groupHomology.isoShortComplexH2_hom
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
(isoShortComplexH2 A).hom = CategoryTheory.CategoryStruct.comp
((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.down ℕ) 3 2 1 isoShortComplexH2._proof_1
isoShortComplexH2._proof_2).hom.app
(inhomogeneousChains A))
(CategoryTheory.ShortComplex.isoMk (chainsIso₃ A) (chainsIso₂ A) (chainsIso₁ A) ⋯ ⋯).hom
noncomputable def
groupHomology.isoCycles₂
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The 2-cycles of the complex of inhomogeneous chains of A are isomorphic to
cycles₂ A, which is a simpler type.
Instances For
@[simp]
theorem
groupHomology.isoCycles₂_hom_comp_i
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
@[simp]
theorem
groupHomology.isoCycles₂_hom_comp_i_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : (shortComplexH2 A).X₂ ⟶ Z)
:
@[simp]
theorem
groupHomology.isoCycles₂_hom_comp_i_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↑(cycles A 2))
:
(ModuleCat.Hom.hom (shortComplexH2 A).g).ker.subtype ((CategoryTheory.ConcreteCategory.hom (isoCycles₂ A).hom) x) = (CategoryTheory.ConcreteCategory.hom (chainsIso₂ A).hom) ((CategoryTheory.ConcreteCategory.hom (iCycles A 2)) x)
@[simp]
theorem
groupHomology.isoCycles₂_inv_comp_iCycles
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
@[simp]
theorem
groupHomology.isoCycles₂_inv_comp_iCycles_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : (inhomogeneousChains A).X 2 ⟶ Z)
:
@[simp]
theorem
groupHomology.isoCycles₂_inv_comp_iCycles_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↥(cycles₂ A))
:
@[simp]
theorem
groupHomology.toCycles_comp_isoCycles₂_hom
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
@[simp]
theorem
groupHomology.toCycles_comp_isoCycles₂_hom_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : ModuleCat.of k ↥(cycles₂ A) ⟶ Z)
:
@[simp]
theorem
groupHomology.toCycles_comp_isoCycles₂_hom_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↑((inhomogeneousChains A).X 3))
:
(CategoryTheory.ConcreteCategory.hom (isoCycles₂ A).hom) ((CategoryTheory.ConcreteCategory.hom (toCycles A 3 2)) x) = (shortComplexH2 A).moduleCatToCycles ((CategoryTheory.ConcreteCategory.hom (chainsIso₃ A).hom) x)
theorem
groupHomology.cyclesMk₂_eq
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↥(cycles₂ A))
:
cyclesMk 2 1 cyclesMk₂_eq._proof_1 ((CategoryTheory.ConcreteCategory.hom (chainsIso₂ A).inv) ↑x) ⋯ = (CategoryTheory.ConcreteCategory.hom (isoCycles₂ A).inv) x
@[reducible, inline]
noncomputable abbrev
groupHomology.H0
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
Shorthand for the 0th group homology of a k-linear G-representation A, H₀(G, A),
defined as the 0th homology of the complex of inhomogeneous chains of A.
Instances For
noncomputable def
groupHomology.H0Iso
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The 0th group homology of A, defined as the 0th homology of the complex of inhomogeneous
chains, is isomorphic to the invariants of the representation on A.
Instances For
The quotient map from A to H₀(G, A).
Instances For
instance
groupHomology.instEpiModuleCatH0π
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
@[simp]
theorem
groupHomology.π_comp_H0Iso_hom
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
CategoryTheory.CategoryStruct.comp (π A 0) (H0Iso A).hom = CategoryTheory.CategoryStruct.comp (cyclesIso₀ A).hom ((Rep.coinvariantsMk k G).app A)
@[simp]
theorem
groupHomology.π_comp_H0Iso_hom_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : (Rep.coinvariantsFunctor k G).obj A ⟶ Z)
:
@[simp]
theorem
groupHomology.π_comp_H0Iso_hom_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↑(cycles A 0))
:
(CategoryTheory.ConcreteCategory.hom (H0Iso A).hom) ((CategoryTheory.ConcreteCategory.hom (π A 0)) x) = (Representation.Coinvariants.mk A.ρ) ((CategoryTheory.ConcreteCategory.hom (cyclesIso₀ A).hom) x)
@[simp]
theorem
groupHomology.coinvariantsMk_comp_H0Iso_inv
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) (H0Iso A).inv = H0π A
@[simp]
theorem
groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : H0 A ⟶ Z)
:
@[simp]
theorem
groupHomology.coinvariantsMk_comp_H0Iso_inv_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↑((CategoryTheory.forget₂ (Rep.{u, u, u} k G) (ModuleCat k)).obj A))
:
(CategoryTheory.ConcreteCategory.hom (H0Iso A).inv)
((CategoryTheory.ConcreteCategory.hom ((Rep.coinvariantsMk k G).app A)) x) = (CategoryTheory.ConcreteCategory.hom (H0π A)) x
@[simp]
theorem
groupHomology.H0π_comp_H0Iso_hom
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
CategoryTheory.CategoryStruct.comp (H0π A) (H0Iso A).hom = (Rep.coinvariantsMk k G).app A
@[simp]
theorem
groupHomology.H0π_comp_H0Iso_hom_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : (Rep.coinvariantsFunctor k G).obj A ⟶ Z)
:
@[simp]
theorem
groupHomology.H0π_comp_H0Iso_hom_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↑A)
:
(CategoryTheory.ConcreteCategory.hom (H0Iso A).hom) ((CategoryTheory.ConcreteCategory.hom (H0π A)) x) = (CategoryTheory.ConcreteCategory.hom ((Rep.coinvariantsMk k G).app A)) x
@[simp]
theorem
groupHomology.cyclesIso₀_comp_H0π
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
CategoryTheory.CategoryStruct.comp (cyclesIso₀ A).hom (H0π A) = π A 0
@[simp]
theorem
groupHomology.cyclesIso₀_comp_H0π_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : H0 A ⟶ Z)
:
@[simp]
theorem
groupHomology.cyclesIso₀_comp_H0π_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↑(cycles A 0))
:
(CategoryTheory.ConcreteCategory.hom (H0π A)) ((CategoryTheory.ConcreteCategory.hom (cyclesIso₀ A).hom) x) = (CategoryTheory.ConcreteCategory.hom (π A 0)) x
theorem
groupHomology.H0_induction_on
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{C : ↑(H0 A) → Prop}
(x : ↑(H0 A))
(h : ∀ (x : ↑A), C ((CategoryTheory.ConcreteCategory.hom (H0π A)) x))
:
C x
noncomputable def
groupHomology.H0IsoOfIsTrivial
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
[A.IsTrivial]
:
When the representation on A is trivial, then H₀(G, A) is all of A.
Instances For
@[simp]
theorem
groupHomology.H0IsoOfIsTrivial_inv_eq_π
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
[A.IsTrivial]
:
(H0IsoOfIsTrivial A).inv = H0π A
@[simp]
theorem
groupHomology.π_comp_H0IsoOfIsTrivial_hom
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
[A.IsTrivial]
:
CategoryTheory.CategoryStruct.comp (π A 0) (H0IsoOfIsTrivial A).hom = (cyclesIso₀ A).hom
@[simp]
theorem
groupHomology.π_comp_H0IsoOfIsTrivial_hom_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
[A.IsTrivial]
{Z : ModuleCat k}
(h : ModuleCat.of k ↑A ⟶ Z)
:
@[simp]
theorem
groupHomology.π_comp_H0IsoOfIsTrivial_hom_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
[A.IsTrivial]
(x : ↑(cycles A 0))
:
(CategoryTheory.ConcreteCategory.hom (H0IsoOfIsTrivial A).hom) ((CategoryTheory.ConcreteCategory.hom (π A 0)) x) = (CategoryTheory.ConcreteCategory.hom (cyclesIso₀ A).hom) x
@[reducible, inline]
noncomputable abbrev
groupHomology.H1
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
Shorthand for the 1st group homology of a k-linear G-representation A, H₁(G, A),
defined as the 1st homology of the complex of inhomogeneous chains of A.
Instances For
The quotient map from the 1-cycles of A, as a submodule of G →₀ A, to H₁(G, A).
Instances For
instance
groupHomology.instEpiModuleCatH1π
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
theorem
groupHomology.H1π_eq_zero_iff
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(x : ↥(cycles₁ A))
:
(CategoryTheory.ConcreteCategory.hom (H1π A)) x = 0 ↔ ↑x ∈ boundaries₁ A
theorem
groupHomology.H1π_eq_iff
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(x y : ↥(cycles₁ A))
:
(CategoryTheory.ConcreteCategory.hom (H1π A)) x = (CategoryTheory.ConcreteCategory.hom (H1π A)) y ↔ ↑x - ↑y ∈ boundaries₁ A
theorem
groupHomology.H1_induction_on
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
{C : ↑(H1 A) → Prop}
(x : ↑(H1 A))
(h : ∀ (x : ↥(cycles₁ A)), C ((CategoryTheory.ConcreteCategory.hom (H1π A)) x))
:
C x
noncomputable def
groupHomology.H1Iso
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The 1st group homology of A, defined as the 1st homology of the complex of inhomogeneous
chains, is isomorphic to cycles₁ A ⧸ boundaries₁ A, which is a simpler type.
Instances For
@[simp]
theorem
groupHomology.π_comp_H1Iso_hom
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
@[simp]
theorem
groupHomology.π_comp_H1Iso_hom_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : (shortComplexH1 A).moduleCatLeftHomologyData.H ⟶ Z)
:
@[simp]
theorem
groupHomology.π_comp_H1Iso_hom_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↑(cycles A 1))
:
(CategoryTheory.ConcreteCategory.hom (H1Iso A).hom) ((CategoryTheory.ConcreteCategory.hom (π A 1)) x) = (shortComplexH1 A).moduleCatToCycles.range.mkQ ((CategoryTheory.ConcreteCategory.hom (isoCycles₁ A).hom) x)
@[simp]
theorem
groupHomology.π_comp_H1Iso_inv
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
@[simp]
theorem
groupHomology.π_comp_H1Iso_inv_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : H1 A ⟶ Z)
:
@[simp]
theorem
groupHomology.π_comp_H1Iso_inv_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↑(shortComplexH1 A).moduleCatLeftHomologyData.K)
:
(CategoryTheory.ConcreteCategory.hom (H1Iso A).inv) ((shortComplexH1 A).moduleCatToCycles.range.mkQ x) = (CategoryTheory.ConcreteCategory.hom (H1π A)) x
noncomputable def
groupHomology.mkH1OfIsTrivial
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
[A.IsTrivial]
:
If a G-representation on A is trivial, this is the natural map Gᵃᵇ → A → H₁(G, A)
sending ⟦g⟧, a to ⟦single g a⟧.
Instances For
@[simp]
theorem
groupHomology.mkH1OfIsTrivial_apply
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
[A.IsTrivial]
(g : G)
(a : ↑A)
:
((mkH1OfIsTrivial A) (Additive.ofMul (Abelianization.of g))) a = (CategoryTheory.ConcreteCategory.hom (H1π A))
((CategoryTheory.ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) fun₀ | g => a)
noncomputable def
groupHomology.H1ToTensorOfIsTrivial
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
[A.IsTrivial]
:
If a G-representation on A is trivial, this is the natural map H₁(G, A) → Gᵃᵇ ⊗[ℤ] A
sending ⟦single g a⟧ to ⟦g⟧ ⊗ₜ a.
Instances For
@[simp]
theorem
groupHomology.H1ToTensorOfIsTrivial_H1π_single
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
[A.IsTrivial]
(g : G)
(a : ↑A)
:
(H1ToTensorOfIsTrivial A)
((CategoryTheory.ConcreteCategory.hom (H1π A))
((CategoryTheory.ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) fun₀ | g => a)) = Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a
noncomputable def
groupHomology.H1AddEquivOfIsTrivial
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
[A.IsTrivial]
:
If a G-representation on A is trivial, this is the group isomorphism between
H₁(G, A) ≃+ Gᵃᵇ ⊗[ℤ] A defined by ⟦single g a⟧ ↦ ⟦g⟧ ⊗ a.
Instances For
theorem
groupHomology.H1AddEquivOfIsTrivial_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
[A.IsTrivial]
(a✝ : ↑(H1 A))
:
(H1AddEquivOfIsTrivial A) a✝ = (H1ToTensorOfIsTrivial A) a✝
theorem
groupHomology.H1AddEquivOfIsTrivial_symm_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
[A.IsTrivial]
(a✝ : TensorProduct ℤ (Additive (Abelianization G)) ↑A)
:
(H1AddEquivOfIsTrivial A).symm a✝ = (TensorProduct.lift (mkH1OfIsTrivial A)) a✝
@[simp]
theorem
groupHomology.H1AddEquivOfIsTrivial_single
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
[A.IsTrivial]
(g : G)
(a : ↑A)
:
(H1AddEquivOfIsTrivial A)
((CategoryTheory.ConcreteCategory.hom (H1π A))
((CategoryTheory.ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) fun₀ | g => a)) = Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a
@[simp]
theorem
groupHomology.H1AddEquivOfIsTrivial_symm_tmul
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
[A.IsTrivial]
(g : G)
(a : ↑A)
:
(H1AddEquivOfIsTrivial A).symm (Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a) = (CategoryTheory.ConcreteCategory.hom (H1π A))
((CategoryTheory.ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) fun₀ | g => a)
@[reducible, inline]
noncomputable abbrev
groupHomology.H2
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
Shorthand for the 2nd group homology of a k-linear G-representation A, H₂(G, A),
defined as the 2nd homology of the complex of inhomogeneous chains of A.
Instances For
The quotient map from the 2-cycles of A, as a submodule of G × G →₀ A, to H₂(G, A).
Instances For
instance
groupHomology.instEpiModuleCatH2π
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
theorem
groupHomology.H2π_eq_zero_iff
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(x : ↥(cycles₂ A))
:
(CategoryTheory.ConcreteCategory.hom (H2π A)) x = 0 ↔ ↑x ∈ boundaries₂ A
theorem
groupHomology.H2π_eq_iff
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
(x y : ↥(cycles₂ A))
:
(CategoryTheory.ConcreteCategory.hom (H2π A)) x = (CategoryTheory.ConcreteCategory.hom (H2π A)) y ↔ ↑x - ↑y ∈ boundaries₂ A
theorem
groupHomology.H2_induction_on
{k G : Type u}
[CommRing k]
[Group G]
{A : Rep.{u, u, u} k G}
{C : ↑(H2 A) → Prop}
(x : ↑(H2 A))
(h : ∀ (x : ↥(cycles₂ A)), C ((CategoryTheory.ConcreteCategory.hom (H2π A)) x))
:
C x
noncomputable def
groupHomology.H2Iso
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
The 2nd group homology of A, defined as the 2nd homology of the complex of inhomogeneous
chains, is isomorphic to cycles₂ A ⧸ boundaries₂ A, which is a simpler type.
Instances For
@[simp]
theorem
groupHomology.π_comp_H2Iso_hom
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
@[simp]
theorem
groupHomology.π_comp_H2Iso_hom_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : (shortComplexH2 A).moduleCatLeftHomologyData.H ⟶ Z)
:
@[simp]
theorem
groupHomology.π_comp_H2Iso_hom_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↑(cycles A 2))
:
(CategoryTheory.ConcreteCategory.hom (H2Iso A).hom) ((CategoryTheory.ConcreteCategory.hom (π A 2)) x) = (shortComplexH2 A).moduleCatToCycles.range.mkQ ((CategoryTheory.ConcreteCategory.hom (isoCycles₂ A).hom) x)
@[simp]
theorem
groupHomology.π_comp_H2Iso_inv
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
:
@[simp]
theorem
groupHomology.π_comp_H2Iso_inv_assoc
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
{Z : ModuleCat k}
(h : H2 A ⟶ Z)
:
@[simp]
theorem
groupHomology.π_comp_H2Iso_inv_apply
{k G : Type u}
[CommRing k]
[Group G]
(A : Rep.{u, u, u} k G)
(x : ↑(shortComplexH2 A).moduleCatLeftHomologyData.K)
:
(CategoryTheory.ConcreteCategory.hom (H2Iso A).inv) ((shortComplexH2 A).moduleCatToCycles.range.mkQ x) = (CategoryTheory.ConcreteCategory.hom (H2π A)) x