therefore
Sign up
Open navigation

Source-pinned research

Research proof index

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 1 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

1 result

Clear filters
Project-declaredLean 4.33.0-rc1

Infl Ī“ naturality

groupCohomology.infl_Ī“_naturality

Plain-language statement

Assume that we have a short exact sequence 0 ā†’ A ā†’ B ā†’ C ā†’ 0 in Rep R G and that the sequence of H- invariants is also a short exact in Rep R (G ā§ø H) : 0 ā†’ Aį““ ā†’ Bį““ ā†’ Cį““ ā†’ 0. Then we have a commuting square Hāæ(G ā§ø H, Cį““) āŸ¶ H^{n+1}(G ā§ø H, Aį““) | | ā†“ ā†“ Hāæ(G , C) āŸ¶ H^{n+1}(G,A) where the horizontal maps are connecting homomorphisms an...

number theoryclass field theorylocal fields

Source project: Class Field Theory

Person-level attribution pending.

View proof record