[Merged by Bors] - feat(RepresentationTheory/Homological/GroupHomology/LowDegree): specialized API for H0, H1, H2#25908
Conversation
…mathlib4 into diagonalsuccisohalf
…ommunity/mathlib4 into diagonalsucciso
…ommunity/mathlib4 into diagonalsucciso
…ommunity/mathlib4 into diagonalsucciso
…mathlib4 into coinvariantsstuffhalf
…mathlib4 into coinvariantsstuffhalf
|
This pull request has conflicts, please merge |
…to gphomlowdeg5
There was a problem hiding this comment.
I thought that the style was to leave spaces after end?
This PR is fine. For years I have had this desire to get group homology and cohomology into mathlib but also this confusion in my head about how to get a usable theory, where we need links both to abstract nonsense (Ext/Tor defined abstractly) and to concrete realisations esp in low degree (e.g. H^1 = these easy-to-write-down-with-no-Fin-1-involved 1-cocycles / easy-to-write-down 1-coboundaries) and also to possible other ways of computing homology or cohomology that I hadn't yet thought of (e.g. maybe one day someone actually wants to compute group cohomology via an injective resolution of M rather than a projective resolution of Z[G]). Even though the definition of group homology is quite abstract, definitions like H2π and theorems like H2π_eq_zero_iff give us some completely concrete way of making elements of H_2 complementing your work with low degree group cohomology earlier. We're going to be starting on class field theory now and this will be an excellent and robust test of your work and Joel Riou's work, but it has now got to the point where everything which I hoped we would have access to is there and this is extremely timely given that the Oxford workshop starts in 10 days! Thanks so much for all your PRs in this area.
maintainer delegate
|
🚀 Pull request has been placed on the maintainer queue by kbuzzard. |
|
This is great, thanks a lot! bors d+ |
|
✌️ 101damnations can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
…alized API for `H0, H1, H2` (#25908) Given a `k`-linear `G`-representation `A`, this PR defines and provides API for: - `groupHomology.H0Iso A`: isomorphism between `H₀(G, A)` and the coinvariants `A_G` of the `G`-representation on `A`. - `groupHomology.H1π A`: epimorphism from the 1-cycles (defined as `Ker(d₀ : (G →₀ A) → A))`) to `H₁(G, A)`. - `groupHomology.H2π A`: epimorphism from the 2-cycles (defined as `Ker(d₁ : (G² →₀ A) → (G →₀ A))`) to `H₂(G, A)`. Co-authored-by: 101damnations <101damnations@github.com>
|
Pull request successfully merged into master. Build succeeded: |
H0, H1, H2H0, H1, H2
…alized API for `H0, H1, H2` (leanprover-community#25908) Given a `k`-linear `G`-representation `A`, this PR defines and provides API for: - `groupHomology.H0Iso A`: isomorphism between `H₀(G, A)` and the coinvariants `A_G` of the `G`-representation on `A`. - `groupHomology.H1π A`: epimorphism from the 1-cycles (defined as `Ker(d₀ : (G →₀ A) → A))`) to `H₁(G, A)`. - `groupHomology.H2π A`: epimorphism from the 2-cycles (defined as `Ker(d₁ : (G² →₀ A) → (G →₀ A))`) to `H₂(G, A)`. Co-authored-by: 101damnations <101damnations@github.com>
…alized API for `H0, H1, H2` (leanprover-community#25908) Given a `k`-linear `G`-representation `A`, this PR defines and provides API for: - `groupHomology.H0Iso A`: isomorphism between `H₀(G, A)` and the coinvariants `A_G` of the `G`-representation on `A`. - `groupHomology.H1π A`: epimorphism from the 1-cycles (defined as `Ker(d₀ : (G →₀ A) → A))`) to `H₁(G, A)`. - `groupHomology.H2π A`: epimorphism from the 2-cycles (defined as `Ker(d₁ : (G² →₀ A) → (G →₀ A))`) to `H₂(G, A)`. Co-authored-by: 101damnations <101damnations@github.com>
…alized API for `H0, H1, H2` (leanprover-community#25908) Given a `k`-linear `G`-representation `A`, this PR defines and provides API for: - `groupHomology.H0Iso A`: isomorphism between `H₀(G, A)` and the coinvariants `A_G` of the `G`-representation on `A`. - `groupHomology.H1π A`: epimorphism from the 1-cycles (defined as `Ker(d₀ : (G →₀ A) → A))`) to `H₁(G, A)`. - `groupHomology.H2π A`: epimorphism from the 2-cycles (defined as `Ker(d₁ : (G² →₀ A) → (G →₀ A))`) to `H₂(G, A)`. Co-authored-by: 101damnations <101damnations@github.com>
Given a
k-linearG-representationA, this PR defines and provides API for:groupHomology.H0Iso A: isomorphism betweenH₀(G, A)and the coinvariantsA_Gof theG-representation onA.groupHomology.H1π A: epimorphism from the 1-cycles (defined asKer(d₀ : (G →₀ A) → A))) toH₁(G, A).groupHomology.H2π A: epimorphism from the 2-cycles (defined asKer(d₁ : (G² →₀ A) → (G →₀ A))) toH₂(G, A).Action.rhoaMonoidHominstead of a morphism inMonCat#21652Finsupp#21732Rep.diagonal k G (n + 1) ≅ Rep.free k G (Fin n → G)#21736IsCycle₁predicate and friends #25884cycles A nwithcyclesₙ Aforn = 0, 1, 2#25888Earlier version at #21759