groupCohomology.mem_twoCocycles_iff
theorem groupCohomology.mem_twoCocycles_iff :
∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep k G} (f : G × G → CoeSort.coe A),
f ∈ groupCohomology.twoCocycles A ↔ ∀ (g h j : G), f (g * h, j) + f (g, h) = (A.ρ g) (f (h, j)) + f (g, h * j)
The theorem `groupCohomology.mem_twoCocycles_iff` gives a condition for a function `f` to be in the 2-cocycles `Z²(G, A)` of a representation `A` of a monoid `G` over a commutative ring `k`. Specifically, `f` is a 2-cocycle if and only if for all elements `g`, `h`, `j` of the group `G`, the equation `f (g * h, j) + f (g, h) = ((Rep.ρ A) g) (f (h, j)) + f (g, h * j)` holds. The left-hand side of this equation is the sum of the values of `f` at `(g * h, j)` and `(g, h)`, and the right-hand side is the result of applying the `g`-th action of the representation `A` on the result of `f (h, j)` and adding the value of `f` at `(g, h * j)`. This theorem is central to the study of group cohomology.
More concisely: A function `f` is a 2-cocycle in the group cohomology of a monoid `G` over a commutative ring `k` with respect to a representation `A` if and only if for all `g, h, j` in `G`, `f (g * h, j) + f (g, h) = (Rep.ρ A g) (f (h, j)) + f (g, h * j)`.
|
groupCohomology.dTwo_comp_eq
theorem groupCohomology.dTwo_comp_eq :
∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep k G),
groupCohomology.dTwo A ∘ₗ ↑(groupCohomology.twoCochainsLequiv A) =
↑(groupCohomology.threeCochainsLequiv A) ∘ₗ (groupCohomology.inhomogeneousCochains A).d 2 3
This theorem, `groupCohomology.dTwo_comp_eq`, states that for any commutative ring `k`, any group `G`, and any `k`-linear `G`-representation `A`, the function `dTwo A` composed with the isomorphism `twoCochainsLequiv A` is equal to the isomorphism `threeCochainsLequiv A` composed with the second differential of the complex of inhomogeneous cochains of `A`. This is depicted by the commutative square in the comment, where `C(G, A)` denotes the complex of inhomogeneous cochains of `A`, and `Fun(G × G, A)` and `Fun(G × G × G, A)` are the second and third objects in this complex, respectively. This theorem, thus, provides a simpler expression for the second differential in the inhomogeneous cochains complex of `A`.
More concisely: For any commutative ring `k`, group `G`, and `k`-linear `G`-representation `A`, the composition of `dTwo A` with `twoCohainsLequiv A` equals the composition of `threeCohainsLequiv A` with the second differential in the complex of inhomogeneous cochains of `A`.
|
groupCohomology.mem_oneCocycles_iff
theorem groupCohomology.mem_oneCocycles_iff :
∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep k G} (f : G → CoeSort.coe A),
f ∈ groupCohomology.oneCocycles A ↔ ∀ (g h : G), f (g * h) = (A.ρ g) (f h) + f g
This theorem states that for any commutative ring `k`, any group `G`, any `k`-linear representation `A` of `G`, and any function `f` from `G` to `A`, `f` is a 1-cocycle (i.e., a member of the set of 1-cocycles of `A`) if and only if, for any pair of elements `g` and `h` from `G`, the function `f` evaluated at the product `g * h` is equal to the sum of the action of `g` on `f(h)` and `f(g)`. In mathematical terms, the theorem captures the property of 1-cocycles in group cohomology: $f(g * h) = g.f(h) + f(g)$.
More concisely: A function from a group to a `k`-linear representation of the group is a 1-cocycle if and only if it satisfies the condition `f(gh) = g.f(h) + f(g)` for all `g, h` in the group.
|
groupCohomology.dOne_comp_eq
theorem groupCohomology.dOne_comp_eq :
∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep k G),
groupCohomology.dOne A ∘ₗ ↑(groupCohomology.oneCochainsLequiv A) =
↑(groupCohomology.twoCochainsLequiv A) ∘ₗ (groupCohomology.inhomogeneousCochains A).d 1 2
This theorem is about the group cohomology in the context of inhomogeneous cochains. Specifically, it states that for any `k`-linear `G`-representation `A`, the function `dOne` provides a simpler expression for the first differential in this cochain complex. In other words, if we consider the commutative diagram where `C^1(G, A)` is mapped to `C^2(G, A)` via the first differential, and `Fun(G, A)` is mapped to `Fun(G × G, A)` via `dOne`, the paths from `C^1(G, A)` to `Fun(G × G, A)` via the first map and `oneCochainsLequiv`, and via `twoCochainsLequiv` and the second map, are the same. This is equivalent to saying that the diagram commutes for these specific maps.
More concisely: The first differential of the inhomogeneous group cochain complex of a `k`-linear `G`-representation `A` can be expressed as `dOne` instead of the standard `d` map, resulting in commuting diagrams for the associated cochain maps.
|
groupCohomology.dZero_comp_eq
theorem groupCohomology.dZero_comp_eq :
∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep k G),
groupCohomology.dZero A ∘ₗ ↑(groupCohomology.zeroCochainsLequiv A) =
↑(groupCohomology.oneCochainsLequiv A) ∘ₗ (groupCohomology.inhomogeneousCochains A).d 0 1
This theorem states that in the context of the complex of inhomogeneous cochains of a `k`-linear `G`-representation `A` (denoted as `C(G, A)`), `dZero` provides a simpler form for the 0th differential. It states this by saying that a certain diagram commutes, where the vertical arrows represent the isomorphisms `zeroCochainsLequiv` and `oneCochainsLequiv` respectively. The horizontal arrows represent the 0th differential `dZero` and the function `Fun(G, A)`. In simpler terms, applying `dZero` after `zeroCochainsLequiv` is the same as applying `oneCochainsLequiv` after the differential at indices 0 and 1 in the complex of inhomogeneous cochains.
More concisely: The 0th differential `dZero` in the complex of inhomogeneous cochains of a `k`-linear `G`-representation `A` commutes with the isomorphisms `zeroCochainsLequiv` and `oneCochainsLequiv`, i.e., `dZero ∘ zeroCochainsLequiv = oneCochainsLequiv ∘ Fun(G, A)`.
|