…G (Fin n → G) ` (#21736)


The first of 2 PRs refactoring group cohomology to use the bar resolution. Given a comm ring `k` and a group `G`, the bar resolution 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. 

This PR defines an isomorphism between the objects in the standard resolution and the bar resolution, i.e. an isomorphism of representations `k[Gⁿ⁺¹] ≅ (Gⁿ →₀ k[G])`, called `Rep.diagonalSuccIsoFree`.

Moves:
- groupCohomology.resolution.actionDiagonalSucc -> Action.diagonalSuccIsoTensorTrivial
- groupCohomology.resolution.diagonalSucc -> Rep.diagonalSuccIsoTensorTrivial



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

…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.

…G (Fin n → G) ` (#21736)


The first of 2 PRs refactoring group cohomology to use the bar resolution. Given a comm ring `k` and a group `G`, the bar resolution 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. 

This PR defines an isomorphism between the objects in the standard resolution and the bar resolution, i.e. an isomorphism of representations `k[Gⁿ⁺¹] ≅ (Gⁿ →₀ k[G])`, called `Rep.diagonalSuccIsoFree`.

Moves:
- groupCohomology.resolution.actionDiagonalSucc -> Action.diagonalSuccIsoTensorTrivial
- groupCohomology.resolution.diagonalSucc -> Rep.diagonalSuccIsoTensorTrivial



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

…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.

…G (Fin n → G) ` (#21736)


The first of 2 PRs refactoring group cohomology to use the bar resolution. Given a comm ring `k` and a group `G`, the bar resolution 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. 

This PR defines an isomorphism between the objects in the standard resolution and the bar resolution, i.e. an isomorphism of representations `k[Gⁿ⁺¹] ≅ (Gⁿ →₀ k[G])`, called `Rep.diagonalSuccIsoFree`.

Moves:
- groupCohomology.resolution.actionDiagonalSucc -> Action.diagonalSuccIsoTensorTrivial
- groupCohomology.resolution.diagonalSucc -> Rep.diagonalSuccIsoTensorTrivial



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

…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>

…G (Fin n → G) ` (leanprover-community#21736)


The first of 2 PRs refactoring group cohomology to use the bar resolution. Given a comm ring `k` and a group `G`, the bar resolution 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. 

This PR defines an isomorphism between the objects in the standard resolution and the bar resolution, i.e. an isomorphism of representations `k[Gⁿ⁺¹] ≅ (Gⁿ →₀ k[G])`, called `Rep.diagonalSuccIsoFree`.

Moves:
- groupCohomology.resolution.actionDiagonalSucc -> Action.diagonalSuccIsoTensorTrivial
- groupCohomology.resolution.diagonalSucc -> Rep.diagonalSuccIsoTensorTrivial



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>