Outside a finite exceptional set, the actual integral tensor-unit subgroup at a finite place is the induced module of the integer units at the chosen extension.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField TensorProduct ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
{K : Type} {L : Type}
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]
section ChosenFinitePlaceLean source · statement
def
relativeLocalTensorDecompositionIntegralUnitSubgroupEquivInducedIntegerUnits
(w₀ : HeightOneSpectrum (𝓞 K)) :
relativeLocalTensorDecompositionIntegralUnitSubgroup
(K := K) (L := L) w₀ ≃*
ChosenFinitePlaceInducedIntegerUnits
(K := K) (L := L) w₀