The low-degree cohomology of a k
-linear G
-representation #
Let k
be a commutative ring and G
a group. This file gives simple expressions for
the group cohomology of a k
-linear G
-representation A
in degrees 0, 1 and 2.
In RepresentationTheory.GroupCohomology.Basic
, we define the n
th 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. Moreover, cohomology of a complex is defined as an abstract
cokernel, whereas the definitions here are explicit quotients of cocycles by coboundaries.
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 oneCocycles
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.GroupCohomology.Basic
, groupCohomology.cocycles A n
and
groupCohomology A n
, and the nCocycles
and Hn A
in this file, for n = 0, 1, 2
.
Main definitions #
groupCohomology.H0 A
: the invariantsAᴳ
of theG
-representation onA
.groupCohomology.H1 A
: 1-cocycles (i.e.Z¹(G, A) := Ker(d¹ : Fun(G, A) → Fun(G², A)
) modulo 1-coboundaries (i.e.B¹(G, A) := Im(d⁰: A → Fun(G, A))
).groupCohomology.H2 A
: 2-cocycles (i.e.Z²(G, A) := Ker(d² : Fun(G², A) → Fun(G³, A)
) modulo 2-coboundaries (i.e.B²(G, A) := Im(d¹: Fun(G, A) → Fun(G², A))
).groupCohomology.H1LequivOfIsTrivial
: the isomorphismH¹(G, A) ≃ Hom(G, A)
when the representation onA
is trivial.groupCohomology.isoHn
forn = 0, 1, 2
: an isomorphismgroupCohomology A n ≅ groupCohomology.Hn A
.
TODO #
- The relationship between
H2
and group extensions - The inflation-restriction exact sequence
- 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.zeroCochainsLequiv A = LinearEquiv.funUnique (Fin 0 → G) k (CoeSort.coe A)
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.oneCochainsLequiv A = LinearEquiv.funCongrLeft k (CoeSort.coe A) (Equiv.funUnique (Fin 1) G).symm
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.twoCochainsLequiv A = LinearEquiv.funCongrLeft k (CoeSort.coe A) (piFinTwoEquiv fun (x : Fin 2) => G).symm
Instances For
The 3rd object in the complex of inhomogeneous cochains of A : Rep k G
is isomorphic
to Fun(G³, A)
as a k
-module.
Equations
- One or more equations did not get rendered due to their size.
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.dZero A = { toFun := fun (m : CoeSort.coe A) (g : G) => (A.ρ g) m - m, map_add' := ⋯, map_smul' := ⋯ }
Instances For
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
- groupCohomology.dOne A = { toFun := fun (f : G → CoeSort.coe A) (g : G × G) => (A.ρ g.1) (f g.2) - f (g.1 * g.2) + f g.1, map_add' := ⋯, map_smul' := ⋯ }
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
Let C(G, A)
denote the complex of inhomogeneous cochains of A : Rep k G
. This lemma
says dZero
gives a simpler expression for the 0th differential: that is, the following
square commutes:
C⁰(G, A) ---d⁰---> C¹(G, A)
| |
| |
| |
v v
A ---- dZero ---> Fun(G, A)
where the vertical arrows are zeroCochainsLequiv
and oneCochainsLequiv
respectively.
Let C(G, A)
denote the complex of inhomogeneous cochains of A : Rep k G
. This lemma
says dOne
gives a simpler expression for the 1st differential: that is, the following
square commutes:
C¹(G, A) ---d¹-----> C²(G, A)
| |
| |
| |
v v
Fun(G, A) -dOne-> Fun(G × G, A)
where the vertical arrows are oneCochainsLequiv
and twoCochainsLequiv
respectively.
Let C(G, A)
denote the complex of inhomogeneous cochains of A : Rep k G
. This lemma
says dTwo
gives a simpler expression for the 2nd differential: that is, the following
square commutes:
C²(G, A) -------d²-----> C³(G, A)
| |
| |
| |
v v
Fun(G × G, A) --dTwo--> Fun(G × G × G, A)
where the vertical arrows are twoCochainsLequiv
and threeCochainsLequiv
respectively.
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₁).
Equations
Instances For
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₂).
Equations
Instances For
When A : Rep k G
is a trivial representation of G
, Z¹(G, A)
is isomorphic to the
group homs G → A
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Makes a 1-coboundary out of f ∈ Im(d⁰)
.
Equations
- groupCohomology.oneCoboundariesOfMemRange h = ⟨⟨f, ⋯⟩, ⋯⟩
Instances For
Makes a 1-coboundary out of f : G → A
and x
such that
ρ(g)(x) - x = f(g)
for all g : G
.
Instances For
Makes a 2-coboundary out of f ∈ Im(d¹)
.
Equations
- groupCohomology.twoCoboundariesOfMemRange h = ⟨⟨f, ⋯⟩, ⋯⟩
Instances For
Makes a 2-coboundary out of f : G × G → A
and x : G → A
such that
ρ(g)(x(h)) - x(gh) + x(g) = f(g, h)
for all g, h : G
.
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
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
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.IsOneCoboundary f = ∃ (x : A), ∀ (g : G), g • x - x = f 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
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
- groupCohomology.oneCocyclesOfIsOneCocycle hf = ⟨f, ⋯⟩
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
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
- groupCohomology.twoCocyclesOfIsTwoCocycle hf = ⟨f, ⋯⟩
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
The next few sections, until the section Cohomology
, are a multiplicative copy of the
previous few sections beginning with IsCocycle
. Unfortunately @[to_additive]
doesn't work with
scalar actions.
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.IsMulOneCoboundary f = ∃ (x : M), ∀ (g : G), g • x / x = f 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
- groupCohomology.oneCocyclesOfIsMulOneCocycle hf = ⟨⇑Additive.ofMul ∘ f, ⋯⟩
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
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
- groupCohomology.twoCocyclesOfIsMulTwoCocycle hf = ⟨⇑Additive.ofMul ∘ f, ⋯⟩
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
We define the 0th group cohomology of a k
-linear G
-representation A
, H⁰(G, A)
, to be
the invariants of the representation, Aᴳ
.
Equations
- groupCohomology.H0 A = A.ρ.invariants
Instances For
We define the 1st group cohomology of a k
-linear G
-representation A
, H¹(G, A)
, to be
1-cocycles (i.e. Z¹(G, A) := Ker(d¹ : Fun(G, A) → Fun(G², A)
) modulo 1-coboundaries
(i.e. B¹(G, A) := Im(d⁰: A → Fun(G, A))
).
Equations
Instances For
We define the 2nd group cohomology of a k
-linear G
-representation A
, H²(G, A)
, to be
2-cocycles (i.e. Z²(G, A) := Ker(d² : Fun(G², A) → Fun(G³, A)
) modulo 2-coboundaries
(i.e. B²(G, A) := Im(d¹: Fun(G, A) → Fun(G², A))
).
Equations
Instances For
When the representation on A
is trivial, then H⁰(G, A)
is all of A.
Equations
Instances For
When A : Rep k G
is a trivial representation of G
, H¹(G, A)
is isomorphic to the
group homs G → A
.
Equations
- groupCohomology.H1LequivOfIsTrivial A = ((groupCohomology.oneCoboundaries A).quotEquivOfEqBot ⋯).trans (groupCohomology.oneCocyclesLequivOfIsTrivial A)
Instances For
The arrow A --dZero--> Fun(G, A)
is isomorphic to the differential
(inhomogeneousCochains A).d 0 1
of the complex of inhomogeneous cochains of A
.
Equations
- groupCohomology.dZeroArrowIso A = CategoryTheory.Arrow.isoMk (groupCohomology.zeroCochainsLequiv A).toModuleIso (groupCohomology.oneCochainsLequiv A).toModuleIso ⋯
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
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
- groupCohomology.isoH0 A = (groupCohomology.inhomogeneousCochains A).isoHomologyπ₀.symm ≪≫ groupCohomology.isoZeroCocycles A
Instances For
The short complex A --dZero--> Fun(G, A) --dOne--> 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
The 1-cocycles of the complex of inhomogeneous cochains of A
are isomorphic to
oneCocycles A
, which is a simpler type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The 1st group cohomology of A
, defined as the 1st cohomology of the complex of inhomogeneous
cochains, is isomorphic to oneCocycles A ⧸ oneCoboundaries A
, which is a simpler type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The short complex Fun(G, A) --dOne--> 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
The 2-cocycles of the complex of inhomogeneous cochains of A
are isomorphic to
twoCocycles A
, which is a simpler type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The 2nd group cohomology of A
, defined as the 2nd cohomology of the complex of inhomogeneous
cochains, is isomorphic to twoCocycles A ⧸ twoCoboundaries A
, which is a simpler type.
Equations
- One or more equations did not get rendered due to their size.