Tags: xroblot/mathlib4
Tags
Merge remote-tracking branch 'origin/master' into nightly-testing
Merge remote-tracking branch 'origin/batteries-pr-testing-1220' into … …nightly-testing
feat: define `IsPositive` and Löwner order for `LinearMap` (leanprove… …r-community#24471) Moves: - ContinuousLinearMap.IsPositive.inner_nonneg_left -> ContinuousLinearMap.IsPositive.re_inner_nonneg_left - ContinuousLinearMap.IsPositive.inner_nonneg_right -> ContinuousLinearMap.IsPositive.re_inner_nonneg_right
feat(RepresentationTheory/*): `Rep.diagonal k G (n + 1) ≅ Rep.free k … …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 <[email protected]>
chore: bump toolchain to v4.21.0-rc1 (leanprover-community#25384) Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
PreviousNext