The embedding of the chosen integral induced block is equivariant for the full global Galois action.
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_smul
(w₀ : HeightOneSpectrum (𝓞 K))
(τ : L ≃ₐ[K] L) :
∀ f : ChosenFinitePlaceInducedIntegerUnits
(K := K) (L := L) w₀,
chosenFinitePlaceIntegralInducedBlockToLocalPlaceBlock
(K := K) (L := L) w₀
((chosenFinitePlaceInducedIntegerUnitsAction
(K := K) (L := L) w₀).smul τ f) =
(chosenFinitePlaceLocalPlaceBlockAction
(K := K) (L := L) w₀).smul τ
(chosenFinitePlaceIntegralInducedBlockToLocalPlaceBlock
(K := K) (L := L) w₀ f)