The low-degree cohomology of a k-linear G-representation #
Let k be a commutative ring and G a group. This file contains specialised API for
the cocycles and group cohomology of a k-linear G-representation A in degrees 0, 1 and 2.
In RepresentationTheory/Homological/GroupCohomology/Basic.lean, we define the nth group
cohomology of A to be the cohomology of a complex inhomogeneousCochains A, whose objects are
(Fin n → G) → A; this is unnecessarily unwieldy in low degree. Here, meanwhile, we define the one
and two cocycles and coboundaries as submodules of Fun(G, A) and Fun(G × G, A), and provide
maps to H1 and H2.
We also show that when the representation on A is trivial, H¹(G, A) ≃ Hom(G, A).
Given an additive or multiplicative abelian group A with an appropriate scalar action of G,
we provide support for turning a function f : G → A satisfying the 1-cocycle identity into an
element of the cocycles₁ of the representation on A (or Additive A) corresponding to the
scalar action. We also do this for 1-coboundaries, 2-cocycles and 2-coboundaries. The
multiplicative case, starting with the section IsMulCocycle, just mirrors the additive case;
unfortunately @[to_additive] can't deal with scalar actions.
The file also contains an identification between the definitions in
RepresentationTheory/Homological/GroupCohomology/Basic.lean, groupCohomology.cocycles A n, and
the cocyclesₙ in this file, for n = 0, 1, 2.
Main definitions #
groupCohomology.H0Iso A: isomorphism betweenH⁰(G, A)and the invariantsAᴳof theG-representation onA.groupCohomology.H1π A: epimorphism from the 1-cocycles (i.e.Z¹(G, A) := Ker(d¹ : Fun(G, A) → Fun(G², A)) toH¹(G, A).groupCohomology.H2π A: epimorphism from the 2-cocycles (i.e.Z²(G, A) := Ker(d² : Fun(G², A) → Fun(G³, A)) toH²(G, A).groupCohomology.H1IsoOfIsTrivial: the isomorphismH¹(G, A) ≅ Hom(G, A)when the representation onAis trivial.
TODO #
- The relationship between
H2and group extensions - Nonabelian group cohomology
The 0th object in the complex of inhomogeneous cochains of A : Rep k G is isomorphic
to A as a k-module.
Equations
- groupCohomology.cochainsIso₀ A = (LinearEquiv.funUnique (Fin 0 → G) k ↑A.V).toModuleIso
Instances For
Alias of groupCohomology.cochainsIso₀.
The 0th object in the complex of inhomogeneous cochains of A : Rep k G is isomorphic
to A as a k-module.
Instances For
Alias of groupCohomology.cochainsIso₀.
Alias of groupCohomology.cochainsIso₀.
The 0th object in the complex of inhomogeneous cochains of A : Rep k G is isomorphic
to A as a k-module.
Instances For
The 1st object in the complex of inhomogeneous cochains of A : Rep k G is isomorphic
to Fun(G, A) as a k-module.
Equations
- groupCohomology.cochainsIso₁ A = (LinearEquiv.funCongrLeft k (↑A.V) (Equiv.funUnique (Fin 1) G)).toModuleIso.symm
Instances For
Alias of groupCohomology.cochainsIso₁.
The 1st object in the complex of inhomogeneous cochains of A : Rep k G is isomorphic
to Fun(G, A) as a k-module.
Instances For
Alias of groupCohomology.cochainsIso₁.
Alias of groupCohomology.cochainsIso₁.
The 1st object in the complex of inhomogeneous cochains of A : Rep k G is isomorphic
to Fun(G, A) as a k-module.
Instances For
The 2nd object in the complex of inhomogeneous cochains of A : Rep k G is isomorphic
to Fun(G², A) as a k-module.
Equations
- groupCohomology.cochainsIso₂ A = (LinearEquiv.funCongrLeft k (↑A.V) (piFinTwoEquiv fun (x : Fin 2) => G)).toModuleIso.symm
Instances For
Alias of groupCohomology.cochainsIso₂.
The 2nd object in the complex of inhomogeneous cochains of A : Rep k G is isomorphic
to Fun(G², A) as a k-module.
Instances For
Alias of groupCohomology.cochainsIso₂.
Alias of groupCohomology.cochainsIso₂.
The 2nd object in the complex of inhomogeneous cochains of A : Rep k G is isomorphic
to Fun(G², A) as a k-module.
Instances For
Alias of groupCohomology.cochainsIso₃.
The 3rd object in the complex of inhomogeneous cochains of A : Rep k G is isomorphic
to Fun(G³, A) as a k-module.
Instances For
Alias of groupCohomology.cochainsIso₃.
Alias of groupCohomology.cochainsIso₃.
The 3rd object in the complex of inhomogeneous cochains of A : Rep k G is isomorphic
to Fun(G³, A) as a k-module.
Instances For
The 0th differential in the complex of inhomogeneous cochains of A : Rep k G, as a
k-linear map A → Fun(G, A). It sends (a, g) ↦ ρ_A(g)(a) - a.
Equations
- groupCohomology.d₀₁ A = ModuleCat.ofHom { toFun := fun (m : ↑A.1) (g : G) => (A.ρ g) m - m, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Alias of groupCohomology.d₀₁.
The 0th differential in the complex of inhomogeneous cochains of A : Rep k G, as a
k-linear map A → Fun(G, A). It sends (a, g) ↦ ρ_A(g)(a) - a.
Equations
Instances For
Alias of groupCohomology.d₀₁_ker_eq_invariants.
Alias of groupCohomology.d₀₁_eq_zero.
Alias of groupCohomology.subtype_comp_d₀₁.
Alias of groupCohomology.d₁₂.
The 1st differential in the complex of inhomogeneous cochains of A : Rep k G, as a
k-linear map Fun(G, A) → Fun(G × G, A). It sends
(f, (g₁, g₂)) ↦ ρ_A(g₁)(f(g₂)) - f(g₁g₂) + f(g₁).
Equations
Instances For
The 2nd differential in the complex of inhomogeneous cochains of A : Rep k G, as a
k-linear map Fun(G × G, A) → Fun(G × G × G, A). It sends
(f, (g₁, g₂, g₃)) ↦ ρ_A(g₁)(f(g₂, g₃)) - f(g₁g₂, g₃) + f(g₁, g₂g₃) - f(g₁, g₂).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of groupCohomology.d₂₃.
The 2nd differential in the complex of inhomogeneous cochains of A : Rep k G, as a
k-linear map Fun(G × G, A) → Fun(G × G × G, A). It sends
(f, (g₁, g₂, g₃)) ↦ ρ_A(g₁)(f(g₂, g₃)) - f(g₁g₂, g₃) + f(g₁, g₂g₃) - f(g₁, g₂).
Equations
Instances For
Let C(G, A) denote the complex of inhomogeneous cochains 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 0 1--> C¹(G, A)
| |
| |
| |
v v
A ------d₀₁-----> Fun(G, A)
where the vertical arrows are cochainsIso₀ and cochainsIso₁ respectively.
Alias of groupCohomology.comp_d₀₁_eq.
Let C(G, A) denote the complex of inhomogeneous cochains 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 0 1--> C¹(G, A)
| |
| |
| |
v v
A ------d₀₁-----> Fun(G, A)
where the vertical arrows are cochainsIso₀ and cochainsIso₁ respectively.
Alias of groupCohomology.comp_d₀₁_eq.
Alias of groupCohomology.comp_d₀₁_eq.
Let C(G, A) denote the complex of inhomogeneous cochains 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 0 1--> C¹(G, A)
| |
| |
| |
v v
A ------d₀₁-----> Fun(G, A)
where the vertical arrows are cochainsIso₀ and cochainsIso₁ respectively.
Alias of groupCohomology.eq_d₀₁_comp_inv.
Let C(G, A) denote the complex of inhomogeneous cochains 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 1 2---> C²(G, A)
| |
| |
| |
v v
Fun(G, A) --d₁₂--> Fun(G × G, A)
where the vertical arrows are cochainsIso₁ and cochainsIso₂ respectively.
Alias of groupCohomology.comp_d₁₂_eq.
Let C(G, A) denote the complex of inhomogeneous cochains 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 1 2---> C²(G, A)
| |
| |
| |
v v
Fun(G, A) --d₁₂--> Fun(G × G, A)
where the vertical arrows are cochainsIso₁ and cochainsIso₂ respectively.
Alias of groupCohomology.comp_d₁₂_eq.
Alias of groupCohomology.comp_d₁₂_eq.
Let C(G, A) denote the complex of inhomogeneous cochains 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 1 2---> C²(G, A)
| |
| |
| |
v v
Fun(G, A) --d₁₂--> Fun(G × G, A)
where the vertical arrows are cochainsIso₁ and cochainsIso₂ respectively.
Alias of groupCohomology.eq_d₁₂_comp_inv.
Let C(G, A) denote the complex of inhomogeneous cochains 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 2 3----> C³(G, A)
| |
| |
| |
v v
Fun(G × G, A) --d₂₃--> Fun(G × G × G, A)
where the vertical arrows are cochainsIso₂ and cochainsIso₃ respectively.
Alias of groupCohomology.comp_d₂₃_eq.
Let C(G, A) denote the complex of inhomogeneous cochains 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 2 3----> C³(G, A)
| |
| |
| |
v v
Fun(G × G, A) --d₂₃--> Fun(G × G × G, A)
where the vertical arrows are cochainsIso₂ and cochainsIso₃ respectively.
Alias of groupCohomology.comp_d₂₃_eq.
Alias of groupCohomology.comp_d₂₃_eq.
Let C(G, A) denote the complex of inhomogeneous cochains 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 2 3----> C³(G, A)
| |
| |
| |
v v
Fun(G × G, A) --d₂₃--> Fun(G × G × G, A)
where the vertical arrows are cochainsIso₂ and cochainsIso₃ respectively.
Alias of groupCohomology.eq_d₂₃_comp_inv.
Alias of groupCohomology.d₀₁_comp_d₁₂.
Alias of groupCohomology.d₀₁_comp_d₁₂.
Alias of groupCohomology.d₀₁_comp_d₁₂.
Alias of groupCohomology.d₁₂_comp_d₂₃.
Alias of groupCohomology.d₁₂_comp_d₂₃.
Alias of groupCohomology.d₁₂_comp_d₂₃.
The (exact) short complex A.ρ.invariants ⟶ A ⟶ (G → A).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The short complex A --d₀₁--> Fun(G, A) --d₁₂--> Fun(G × G, A).
Equations
- groupCohomology.shortComplexH1 A = { X₁ := A.V, X₂ := ModuleCat.of k (G → ↑A.V), X₃ := ModuleCat.of k (G × G → ↑A.V), f := groupCohomology.d₀₁ A, g := groupCohomology.d₁₂ A, zero := ⋯ }
Instances For
The short complex Fun(G, A) --d₁₂--> Fun(G × G, A) --d₂₃--> Fun(G × G × G, A).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of groupCohomology.cocycles₁.
The 1-cocycles Z¹(G, A) of A : Rep k G, defined as the kernel of the map
Fun(G, A) → Fun(G × G, A) sending (f, (g₁, g₂)) ↦ ρ_A(g₁)(f(g₂)) - f(g₁g₂) + f(g₁).
Instances For
Alias of groupCohomology.cocycles₂.
The 2-cocycles Z²(G, A) of A : Rep k G, defined as the kernel of the map
Fun(G × G, A) → Fun(G × G × G, A) sending
(f, (g₁, g₂, g₃)) ↦ ρ_A(g₁)(f(g₂, g₃)) - f(g₁g₂, g₃) + f(g₁, g₂g₃) - f(g₁, g₂).
Instances For
Equations
- groupCohomology.instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁ = { coe := Subtype.val, coe_injective' := ⋯ }
Alias of groupCohomology.cocycles₁.val_eq_coe.
Alias of groupCohomology.cocycles₁_ext.
Alias of groupCohomology.cocycles₁_map_one.
Alias of groupCohomology.d₀₁_apply_mem_cocycles₁.
Alias of groupCohomology.cocycles₁.d₁₂_apply.
Alias of groupCohomology.cocycles₁IsoOfIsTrivial.
When A : Rep k G is a trivial representation of G, Z¹(G, A) is isomorphic to the
group homs G → A.
Instances For
Alias of groupCohomology.cocycles₁IsoOfIsTrivial.
Alias of groupCohomology.cocycles₁IsoOfIsTrivial.
When A : Rep k G is a trivial representation of G, Z¹(G, A) is isomorphic to the
group homs G → A.
Instances For
Equations
- groupCohomology.instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂ = { coe := Subtype.val, coe_injective' := ⋯ }
Alias of groupCohomology.cocycles₂.val_eq_coe.
Alias of groupCohomology.mem_cocycles₂_def.
Alias of groupCohomology.mem_cocycles₂_iff.
Alias of groupCohomology.d₁₂_apply_mem_cocycles₂.
Alias of groupCohomology.cocycles₂.d₂₃_apply.
Alias of groupCohomology.coboundaries₁.
The 1-coboundaries B¹(G, A) of A : Rep k G, defined as the image of the map
A → Fun(G, A) sending (a, g) ↦ ρ_A(g)(a) - a.
Instances For
Alias of groupCohomology.coboundaries₂.
The 2-coboundaries B²(G, A) of A : Rep k G, defined as the image of the map
Fun(G, A) → Fun(G × G, A) sending (f, (g₁, g₂)) ↦ ρ_A(g₁)(f(g₂)) - f(g₁g₂) + f(g₁).
Instances For
Equations
- groupCohomology.instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCoboundaries₁ = { coe := Subtype.val, coe_injective' := ⋯ }
Alias of groupCohomology.coboundaries₁.coe_mk.
Alias of groupCohomology.coboundaries₁.val_eq_coe.
Alias of groupCohomology.coboundaries₁_ext.
Natural inclusion B¹(G, A) →ₗ[k] Z¹(G, A).
Equations
Instances For
Alias of groupCohomology.coboundariesToCocycles₁.
Natural inclusion B¹(G, A) →ₗ[k] Z¹(G, A).
Instances For
Equations
- groupCohomology.instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCoboundaries₂ = { coe := Subtype.val, coe_injective' := ⋯ }
Alias of groupCohomology.coboundaries₂.coe_mk.
Alias of groupCohomology.coboundaries₂.val_eq_coe.
Natural inclusion B²(G, A) →ₗ[k] Z²(G, A).
Equations
Instances For
Alias of groupCohomology.coboundariesToCocycles₂.
Natural inclusion B²(G, A) →ₗ[k] Z²(G, A).
Instances For
A function f : G → A satisfies the 1-cocycle condition if
f(gh) = g • f(h) + f(g) for all g, h : G.
Instances For
Alias of groupCohomology.IsCocycle₁.
A function f : G → A satisfies the 1-cocycle condition if
f(gh) = g • f(h) + f(g) for all g, h : G.
Instances For
A function f : G × G → A satisfies the 2-cocycle condition if
f(gh, j) + f(g, h) = g • f(h, j) + f(g, hj) for all g, h : G.
Equations
Instances For
Alias of groupCohomology.IsCocycle₂.
A function f : G × G → A satisfies the 2-cocycle condition if
f(gh, j) + f(g, h) = g • f(h, j) + f(g, hj) for all g, h : G.
Instances For
Alias of groupCohomology.map_one_of_isCocycle₁.
Alias of groupCohomology.map_inv_of_isCocycle₁.
Alias of groupCohomology.smul_map_inv_sub_map_inv_of_isCocycle₂.
A function f : G → A satisfies the 1-coboundary condition if there's x : A such that
g • x - x = f(g) for all g : G.
Equations
- groupCohomology.IsCoboundary₁ f = ∃ (x : A), ∀ (g : G), g • x - x = f g
Instances For
Alias of groupCohomology.IsCoboundary₁.
A function f : G → A satisfies the 1-coboundary condition if there's x : A such that
g • x - x = f(g) for all g : G.
Instances For
A function f : G × G → A satisfies the 2-coboundary condition if there's x : G → A such
that g • x(h) - x(gh) + x(g) = f(g, h) for all g, h : G.
Equations
Instances For
Alias of groupCohomology.IsCoboundary₂.
A function f : G × G → A satisfies the 2-coboundary condition if there's x : G → A such
that g • x(h) - x(gh) + x(g) = f(g, h) for all g, h : G.
Instances For
Given a k-module A with a compatible DistribMulAction of G, and a function
f : G → A satisfying the 1-cocycle condition, produces a 1-cocycle for the representation on
A induced by the DistribMulAction.
Equations
Instances For
Alias of groupCohomology.cocyclesOfIsCocycle₁.
Given a k-module A with a compatible DistribMulAction of G, and a function
f : G → A satisfying the 1-cocycle condition, produces a 1-cocycle for the representation on
A induced by the DistribMulAction.
Instances For
Given a k-module A with a compatible DistribMulAction of G, and a function
f : G → A satisfying the 1-coboundary condition, produces a 1-coboundary for the representation
on A induced by the DistribMulAction.
Equations
Instances For
Alias of groupCohomology.coboundariesOfIsCoboundary₁.
Given a k-module A with a compatible DistribMulAction of G, and a function
f : G → A satisfying the 1-coboundary condition, produces a 1-coboundary for the representation
on A induced by the DistribMulAction.
Equations
Instances For
Alias of groupCohomology.isCoboundary₁_of_mem_coboundaries₁.
Given a k-module A with a compatible DistribMulAction of G, and a function
f : G × G → A satisfying the 2-cocycle condition, produces a 2-cocycle for the representation on
A induced by the DistribMulAction.
Equations
Instances For
Alias of groupCohomology.cocyclesOfIsCocycle₂.
Given a k-module A with a compatible DistribMulAction of G, and a function
f : G × G → A satisfying the 2-cocycle condition, produces a 2-cocycle for the representation on
A induced by the DistribMulAction.
Instances For
Given a k-module A with a compatible DistribMulAction of G, and a function
f : G × G → A satisfying the 2-coboundary condition, produces a 2-coboundary for the
representation on A induced by the DistribMulAction.
Equations
Instances For
Alias of groupCohomology.coboundariesOfIsCoboundary₂.
Given a k-module A with a compatible DistribMulAction of G, and a function
f : G × G → A satisfying the 2-coboundary condition, produces a 2-coboundary for the
representation on A induced by the DistribMulAction.
Equations
Instances For
Alias of groupCohomology.isCoboundary₂_of_mem_coboundaries₂.
The next few sections, until the section CocyclesIso, are a multiplicative copy of the
previous few sections beginning with IsCocycle. Unfortunately @[to_additive] doesn't work with
scalar actions.
Alias of groupCohomology.IsMulCocycle₁.
A function f : G → M satisfies the multiplicative 1-cocycle condition if
f(gh) = g • f(h) * f(g) for all g, h : G.
Instances For
Alias of groupCohomology.IsMulCocycle₂.
A function f : G × G → M satisfies the multiplicative 2-cocycle condition if
f(gh, j) * f(g, h) = g • f(h, j) * f(g, hj) for all g, h : G.
Instances For
Alias of groupCohomology.map_one_of_isMulCocycle₁.
Alias of groupCohomology.map_inv_of_isMulCocycle₁.
Alias of groupCohomology.smul_map_inv_div_map_inv_of_isMulCocycle₂.
A function f : G → M satisfies the multiplicative 1-coboundary condition if there's x : M
such that g • x / x = f(g) for all g : G.
Equations
- groupCohomology.IsMulCoboundary₁ f = ∃ (x : M), ∀ (g : G), g • x / x = f g
Instances For
Alias of groupCohomology.IsMulCoboundary₁.
A function f : G → M satisfies the multiplicative 1-coboundary condition if there's x : M
such that g • x / x = f(g) for all g : G.
Instances For
Alias of groupCohomology.IsMulCoboundary₂.
A function f : G × G → M satisfies the 2-coboundary condition if there's x : G → M such
that g • x(h) / x(gh) * x(g) = f(g, h) for all g, h : G.
Instances For
Given an abelian group M with a MulDistribMulAction of G, and a function
f : G → M satisfying the multiplicative 1-cocycle condition, produces a 1-cocycle for the
representation on Additive M induced by the MulDistribMulAction.
Equations
Instances For
Alias of groupCohomology.cocyclesOfIsMulCocycle₁.
Given an abelian group M with a MulDistribMulAction of G, and a function
f : G → M satisfying the multiplicative 1-cocycle condition, produces a 1-cocycle for the
representation on Additive M induced by the MulDistribMulAction.
Instances For
Given an abelian group M with a MulDistribMulAction of G, and a function
f : G → M satisfying the multiplicative 1-coboundary condition, produces a
1-coboundary for the representation on Additive M induced by the MulDistribMulAction.
Equations
Instances For
Alias of groupCohomology.coboundariesOfIsMulCoboundary₁.
Given an abelian group M with a MulDistribMulAction of G, and a function
f : G → M satisfying the multiplicative 1-coboundary condition, produces a
1-coboundary for the representation on Additive M induced by the MulDistribMulAction.
Equations
Instances For
Alias of groupCohomology.isMulCoboundary₁_of_mem_coboundaries₁.
Given an abelian group M with a MulDistribMulAction of G, and a function
f : G × G → M satisfying the multiplicative 2-cocycle condition, produces a 2-cocycle for the
representation on Additive M induced by the MulDistribMulAction.
Equations
Instances For
Alias of groupCohomology.cocyclesOfIsMulCocycle₂.
Given an abelian group M with a MulDistribMulAction of G, and a function
f : G × G → M satisfying the multiplicative 2-cocycle condition, produces a 2-cocycle for the
representation on Additive M induced by the MulDistribMulAction.
Instances For
Given an abelian group M with a MulDistribMulAction of G, and a function
f : G × G → M satisfying the multiplicative 2-coboundary condition, produces a
2-coboundary for the representation on M induced by the MulDistribMulAction.
Equations
Instances For
Alias of groupCohomology.coboundariesOfIsMulCoboundary₂.
Given an abelian group M with a MulDistribMulAction of G, and a function
f : G × G → M satisfying the multiplicative 2-coboundary condition, produces a
2-coboundary for the representation on M induced by the MulDistribMulAction.
Equations
Instances For
Alias of groupCohomology.isMulCoboundary₂_of_mem_coboundaries₂.
The arrow A --d₀₁--> Fun(G, A) is isomorphic to the differential
(inhomogeneousCochains A).d 0 1 of the complex of inhomogeneous cochains of A.
Equations
Instances For
Alias of groupCohomology.dArrowIso₀₁.
The arrow A --d₀₁--> Fun(G, A) is isomorphic to the differential
(inhomogeneousCochains A).d 0 1 of the complex of inhomogeneous cochains of A.
Instances For
The 0-cocycles of the complex of inhomogeneous cochains of A are isomorphic to
A.ρ.invariants, which is a simpler type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of groupCohomology.cocyclesIso₀.
The 0-cocycles of the complex of inhomogeneous cochains of A are isomorphic to
A.ρ.invariants, which is a simpler type.
Instances For
Alias of groupCohomology.cocyclesIso₀.
Alias of groupCohomology.cocyclesIso₀.
The 0-cocycles of the complex of inhomogeneous cochains of A are isomorphic to
A.ρ.invariants, which is a simpler type.
Instances For
Alias of groupCohomology.cocyclesIso₀_hom_comp_f.
Alias of groupCohomology.cocyclesIso₀_hom_comp_f.
Alias of groupCohomology.cocyclesIso₀_hom_comp_f.
Alias of groupCohomology.cocyclesIso₀_inv_comp_iCocycles.
Alias of groupCohomology.cocyclesMk₀_eq.
The short complex A --d₀₁--> Fun(G, A) --d₁₂--> Fun(G × G, A) is isomorphic to the 1st
short complex associated to the complex of inhomogeneous cochains of A.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of groupCohomology.isoShortComplexH1.
The short complex A --d₀₁--> Fun(G, A) --d₁₂--> Fun(G × G, A) is isomorphic to the 1st
short complex associated to the complex of inhomogeneous cochains of A.
Instances For
Alias of groupCohomology.isoCocycles₁.
The 1-cocycles of the complex of inhomogeneous cochains of A are isomorphic to
cocycles₁ A, which is a simpler type.
Instances For
Alias of groupCohomology.isoCocycles₁_hom_comp_i.
Alias of groupCohomology.isoCocycles₁_hom_comp_i.
Alias of groupCohomology.isoCocycles₁_hom_comp_i.
Alias of groupCohomology.cocyclesMk₁_eq.
The short complex Fun(G, A) --d₁₂--> Fun(G × G, A) --dTwo--> Fun(G × G × G, A) is
isomorphic to the 2nd short complex associated to the complex of inhomogeneous cochains of A.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of groupCohomology.isoShortComplexH2.
The short complex Fun(G, A) --d₁₂--> Fun(G × G, A) --dTwo--> Fun(G × G × G, A) is
isomorphic to the 2nd short complex associated to the complex of inhomogeneous cochains of A.
Instances For
Alias of groupCohomology.isoCocycles₂.
The 2-cocycles of the complex of inhomogeneous cochains of A are isomorphic to
cocycles₂ A, which is a simpler type.
Instances For
Alias of groupCohomology.isoCocycles₂_hom_comp_i.
Alias of groupCohomology.isoCocycles₂_hom_comp_i.
Alias of groupCohomology.isoCocycles₂_hom_comp_i.
Alias of groupCohomology.cocyclesMk₂_eq.
Shorthand for the 0th group cohomology of a k-linear G-representation A, H⁰(G, A),
defined as the 0th cohomology of the complex of inhomogeneous cochains of A.
Equations
Instances For
The 0th group cohomology of A, defined as the 0th cohomology of the complex of inhomogeneous
cochains, is isomorphic to the invariants of the representation on A.
Equations
Instances For
Alias of groupCohomology.H0Iso.
The 0th group cohomology of A, defined as the 0th cohomology of the complex of inhomogeneous
cochains, is isomorphic to the invariants of the representation on A.
Equations
Instances For
Alias of groupCohomology.π_comp_H0Iso_hom.
Alias of groupCohomology.H0IsoOfIsTrivial.
When the representation on A is trivial, then H⁰(G, A) is all of A.
Instances For
Alias of groupCohomology.H0IsoOfIsTrivial_hom.
Shorthand for the 1st group cohomology of a k-linear G-representation A, H¹(G, A),
defined as the 1st cohomology of the complex of inhomogeneous cochains of A.
Equations
Instances For
The quotient map from the 1-cocycles of A, as a submodule of G → A, to H¹(G, A).
Equations
Instances For
The 1st group cohomology of A, defined as the 1st cohomology of the complex of inhomogeneous
cochains, is isomorphic to cocycles₁ A ⧸ coboundaries₁ A, which is a simpler type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of groupCohomology.H1Iso.
The 1st group cohomology of A, defined as the 1st cohomology of the complex of inhomogeneous
cochains, is isomorphic to cocycles₁ A ⧸ coboundaries₁ A, which is a simpler type.
Equations
Instances For
Alias of groupCohomology.π_comp_H1Iso_hom.
Alias of groupCohomology.H1IsoOfIsTrivial.
When A : Rep k G is a trivial representation of G, H¹(G, A) is isomorphic to the
group homs G → A.
Instances For
Shorthand for the 2nd group cohomology of a k-linear G-representation A, H²(G, A),
defined as the 2nd cohomology of the complex of inhomogeneous cochains of A.
Equations
Instances For
The quotient map from the 2-cocycles of A, as a submodule of G × G → A, to H²(G, A).
Equations
Instances For
The 2nd group cohomology of A, defined as the 2nd cohomology of the complex of inhomogeneous
cochains, is isomorphic to cocycles₂ A ⧸ coboundaries₂ A, which is a simpler type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of groupCohomology.H2Iso.
The 2nd group cohomology of A, defined as the 2nd cohomology of the complex of inhomogeneous
cochains, is isomorphic to cocycles₂ A ⧸ coboundaries₂ A, which is a simpler type.
Equations
Instances For
Alias of groupCohomology.π_comp_H2Iso_hom.