Module

ChosenPlaceIntegralBlockInclusion.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Cohomology.SPlaces.OutsideIntegralInduced.ChosenPlaceIntegralBlockInclusion

2 declarations indexed from sourceView source ↗

Module documentation

Inclusion of the chosen integral induced block

This file embeds the chosen induced module of local integer units into the ordinary local multiplicative block and proves injectivity.

Imports1

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Cohomology.SPlaces.OutsideIntegralInduced.ChosenPlaceAction

Imported by8

def

chosenFinitePlaceIntegralInducedBlockToLocalPlaceBlock

L40 ↗

Documentation

Inclusion of the chosen integral block into the ordinary chosen local multiplicative block.

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 ChosenFinitePlace

Lean source · statement

def chosenFinitePlaceIntegralInducedBlockToLocalPlaceBlock
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    ChosenFinitePlaceInducedIntegerUnits
        (K := K) (L := L) w₀ →
      ChosenFinitePlaceLocalPlaceBlock
        (K := K) (L := L) w₀

theorem

chosenFinitePlaceIntegralInducedBlockToLocalPlaceBlock_injective

L72 ↗