ClassFieldTower.Cohomology.finiteGaloisTowerBaseUnitsH2_inflation_restriction
Inflate a base-unit class from the normal intermediate field and restrict it to the relative Galois group. The result is its actual group restriction with the coefficient map along K → L → N.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K N L M : Type) [Field K] [Field N] [Field L] [Field M]
variable [Algebra K N] [Algebra K L] [Algebra L N] [IsScalarTower K L N]
variable [Algebra K M] [Algebra M N] [IsScalarTower K M N] [Normal K M]Lean source · statement
theorem finiteGaloisTowerBaseUnitsH2_inflation_restriction :
finiteGaloisBaseUnitsH2Map K M ≫ finiteGaloisTowerUnitsH2Inflation K M N ≫
finiteGaloisTowerUnitsH2Restriction K L N =
groupCohomology.map
(A := Rep.trivial ℤ Gal(M/K) (Additive Kˣ))
(B := Rep.trivial ℤ Gal(N/L) (Additive Kˣ))
((AlgEquiv.restrictNormalHom (F := K) (K₁ := N) M).comp
(AlgEquiv.restrictScalarsHom K))
(𝟙 (Rep.trivial ℤ Gal(N/L) (Additive Kˣ))) 2 ≫
finiteTowerBaseUnitsH2Map K L N