Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 3 research declarations. Search 10,000 more complete Mathlib declarations.
3 results
Clear filtersRep.split.TateTheorem_lemma_1
Plain-language statement
If σ generates H²(G,M) then the map H²(G,M) ⟶ H²(G,split σ) is zero.
Source project: Class Field Theory
Person-level attribution pending.
Rep.split.TateTheorem_lemma_2
Plain-language statement
For any subgroup H of G, the connecting hommorphism in the splitting module long exact sequence H¹(H,aug) ⟶ H²(H,M) is an isomorphism.
Source project: Class Field Theory
Person-level attribution pending.
Rep.split.τ_property
Plain-language statement
Given a 2-cocycle σ, the image of σ in the splitting module of σ is equal to the coboundary of τ σ.
Source project: Class Field Theory
Person-level attribution pending.