The two routes through a finite Galois tower are compared using their actual group restriction and coefficient maps. This comparison is used to turn relative norm primitives into vanishing of restricted inflated H² classes.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K N : Type) [Field K] [Field N] [Algebra K N]
variable (L M : IntermediateField K N)def relativeRestrictionHom : Gal(N/L) →* Gal(N/K)Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K N : Type) [Field K] [Field N] [Algebra K N]
variable (L M : IntermediateField K N)def relativeUnitsRepHom :
Rep.res (relativeRestrictionHom K N L) (Rep.ofAlgebraAutOnUnits K N) ⟶
Rep.ofAlgebraAutOnUnits L NSurrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K N : Type) [Field K] [Field N] [Algebra K N]
variable (L M : IntermediateField K N)def relativeSubgroupUnitsRepHom :
Rep.res L.fixingSubgroupEquiv.symm.toMonoidHom
(Rep.res L.fixingSubgroup.subtype (Rep.ofAlgebraAutOnUnits K N)) ⟶
Rep.ofAlgebraAutOnUnits L NSurrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K N : Type) [Field K] [Field N] [Algebra K N]
variable (L M : IntermediateField K N)theorem unitsH2Restriction_eq_map :
finiteGaloisUnitsH2Restriction K N L =
groupCohomology.map (relativeRestrictionHom K N L) (relativeUnitsRepHom K N L) 2Inflate 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.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K N : Type) [Field K] [Field N] [Algebra K N]
variable (L M : IntermediateField K N)
variable [Normal K M]theorem finiteGaloisBaseUnitsH2_inflation_restriction :
finiteGaloisBaseUnitsH2Map K M ≫ finiteGaloisUnitsH2Inflation K N M ≫
finiteGaloisUnitsH2Restriction K N L =
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
(L.fixingSubgroup.subtype.comp L.fixingSubgroupEquiv.symm.toMonoidHom))
(𝟙 (Rep.trivial ℤ Gal(N/L) (Additive Kˣ))) 2 ≫
finiteTowerBaseUnitsH2Map K L N