…25546)

The second of 3 PRs refactoring group cohomology to use the bar resolution. Given a comm ring `k` and a group `G`, this is the projective resolution of `k` as a trivial `G`-representation whose `n`th object is 
`Gⁿ →₀ k[G]` with representation defined pointwise by the left regular representation on k[G], and whose differentials send `(g₀, ..., gₙ)` to `g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁)` for `j = 0, ... , n - 1`.
The refactor means we can reuse this material to set up group homology.

In #21736  we defined an isomorphism `Rep.diagonalSuccIsoFree` between the objects in the standard resolution and bar resolution. In the next PR, #21738, we show that this isomorphism defines a commutative square with the respective differentials, and thus conclude that the bar resolution differential squares to zero and that the 2 complexes are isomorphic. We carry the exactness properties across this isomorphism to conclude the bar resolution is a projective resolution too, in `Rep.barResolution`.

In this PR we factor out some material from #21738, to make it easier to review.

The third of 3 PRs refactoring group cohomology to use the bar resolution. Given a comm ring `k` and a group `G`, this is the projective resolution of `k` as a trivial `G`-representation whose `n`th object is 
`Gⁿ →₀ k[G]` with representation defined pointwise by the left regular representation on k[G], and whose differentials send `(g₀, ..., gₙ)` to `g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁)` for `j = 0, ... , n - 1`.
The refactor means we can reuse this material to set up group homology.

In #21736  we define an isomorphism `Rep.diagonalSuccIsoFree` between the objects in the standard resolution and bar resolution. In this PR we show that this isomorphism defines a commutative square with the respective differentials, and thus conclude that the bar resolution differential squares to zero and that the 2 complexes are isomorphic. We carry the exactness properties across this isomorphism to conclude the bar resolution is a projective resolution too, in `Rep.barResolution`.



Co-authored-by: 101damnations <al3717@ic.ac.uk>

…unity#21738)

The third of 3 PRs refactoring group cohomology to use the bar resolution. Given a comm ring `k` and a group `G`, this is the projective resolution of `k` as a trivial `G`-representation whose `n`th object is 
`Gⁿ →₀ k[G]` with representation defined pointwise by the left regular representation on k[G], and whose differentials send `(g₀, ..., gₙ)` to `g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁)` for `j = 0, ... , n - 1`.
The refactor means we can reuse this material to set up group homology.

In leanprover-community#21736  we define an isomorphism `Rep.diagonalSuccIsoFree` between the objects in the standard resolution and bar resolution. In this PR we show that this isomorphism defines a commutative square with the respective differentials, and thus conclude that the bar resolution differential squares to zero and that the 2 complexes are isomorphic. We carry the exactness properties across this isomorphism to conclude the bar resolution is a projective resolution too, in `Rep.barResolution`.



Co-authored-by: 101damnations <al3717@ic.ac.uk>

…unity#21738)

The third of 3 PRs refactoring group cohomology to use the bar resolution. Given a comm ring `k` and a group `G`, this is the projective resolution of `k` as a trivial `G`-representation whose `n`th object is 
`Gⁿ →₀ k[G]` with representation defined pointwise by the left regular representation on k[G], and whose differentials send `(g₀, ..., gₙ)` to `g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁)` for `j = 0, ... , n - 1`.
The refactor means we can reuse this material to set up group homology.

In leanprover-community#21736  we define an isomorphism `Rep.diagonalSuccIsoFree` between the objects in the standard resolution and bar resolution. In this PR we show that this isomorphism defines a commutative square with the respective differentials, and thus conclude that the bar resolution differential squares to zero and that the 2 complexes are isomorphic. We carry the exactness properties across this isomorphism to conclude the bar resolution is a projective resolution too, in `Rep.barResolution`.



Co-authored-by: 101damnations <al3717@ic.ac.uk>

…eanprover-community#25546)

The second of 3 PRs refactoring group cohomology to use the bar resolution. Given a comm ring `k` and a group `G`, this is the projective resolution of `k` as a trivial `G`-representation whose `n`th object is 
`Gⁿ →₀ k[G]` with representation defined pointwise by the left regular representation on k[G], and whose differentials send `(g₀, ..., gₙ)` to `g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁)` for `j = 0, ... , n - 1`.
The refactor means we can reuse this material to set up group homology.

In leanprover-community#21736  we defined an isomorphism `Rep.diagonalSuccIsoFree` between the objects in the standard resolution and bar resolution. In the next PR, leanprover-community#21738, we show that this isomorphism defines a commutative square with the respective differentials, and thus conclude that the bar resolution differential squares to zero and that the 2 complexes are isomorphic. We carry the exactness properties across this isomorphism to conclude the bar resolution is a projective resolution too, in `Rep.barResolution`.

In this PR we factor out some material from leanprover-community#21738, to make it easier to review.

…unity#21738)

The third of 3 PRs refactoring group cohomology to use the bar resolution. Given a comm ring `k` and a group `G`, this is the projective resolution of `k` as a trivial `G`-representation whose `n`th object is 
`Gⁿ →₀ k[G]` with representation defined pointwise by the left regular representation on k[G], and whose differentials send `(g₀, ..., gₙ)` to `g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁)` for `j = 0, ... , n - 1`.
The refactor means we can reuse this material to set up group homology.

In leanprover-community#21736  we define an isomorphism `Rep.diagonalSuccIsoFree` between the objects in the standard resolution and bar resolution. In this PR we show that this isomorphism defines a commutative square with the respective differentials, and thus conclude that the bar resolution differential squares to zero and that the 2 complexes are isomorphic. We carry the exactness properties across this isomorphism to conclude the bar resolution is a projective resolution too, in `Rep.barResolution`.



Co-authored-by: 101damnations <al3717@ic.ac.uk>