The integral-block inclusion is compatible with the pre-existing local-block equivalence on underlying field units.
Source context 12 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 ChosenFinitePlace
omit [NumberField L] inLean source · statement
theorem
chosenFinitePlaceIntegralInducedBlockToLocalPlaceBlock_equiv_apply
(w₀ : HeightOneSpectrum (𝓞 K))
(x : relativeLocalTensorDecompositionIntegralUnitSubgroup
(K := K) (L := L) w₀) :
chosenFinitePlaceIntegralInducedBlockToLocalPlaceBlock
(K := K) (L := L) w₀
(relativeLocalTensorDecompositionIntegralUnitSubgroupEquivInducedIntegerUnits
(K := K) (L := L) w₀ x) =
finitePlaceTensorUnitsEquivLocalPlaceBlock
(K := K) (L := L) w₀
(chosenFinitePlaceExtension (L := L) w₀)
(x : (w₀.adicCompletion K ⊗[K] L)ˣ)