Module

Compositum.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.Filtered.Compositum

1 declaration indexed from sourceView source ↗

Module documentation

Filtered reciprocity for a compositum

At a nonnegative ramification index, an unramified factor contributes trivially to both the principal-unit Artin image and the upper ramification group. Equality on the other factor can then be recovered upstairs from the joint injectivity of the two restriction maps.

Imports5

Imported by5

theorem

filteredLocalReciprocity_of_compositum

L35 ↗

LocalClassFieldTheory.filteredLocalReciprocity_of_compositum

Documentation

Filtered local reciprocity ascends from one factor of a compositum when both filtrations restrict trivially to the other factor.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace LocalClassFieldTheory
open RamificationTheory.LocalField
open RamificationTheory
open LocalClassFieldTheory
open LocalFieldTheory
open scoped ValuativeRel

Lean source · statement

theorem filteredLocalReciprocity_of_compositum
    (K : Type) [Field K]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (E₁ E₂ F : IntermediateField K (SeparableClosure K))
    (hE₁ : E₁ ≤ F) (hE₂ : E₂ ≤ F)
    [FiniteDimensional K E₁] [FiniteDimensional K E₂]
    [FiniteDimensional K F]
    [IsAbelianGalois K E₁] [IsAbelianGalois K E₂]
    [IsAbelianGalois K F]
    (hsup : E₁ ⊔ E₂ = F)
    (t : ℝ)
    (hArtin₁ : artinPrincipalUnitStepGroup K E₁ t = ⊥)
    (hUpper₁ : localUpperRamificationGroup K E₁ t = ⊥)
    (hfiltered₂ :
      artinPrincipalUnitStepGroup K E₂ t =
        localUpperRamificationGroup K E₂ t) :
    artinPrincipalUnitStepGroup K F t =
      localUpperRamificationGroup K F t

Module documentation

Filtered reciprocity for a compositum

Declarations

filteredLocalReciprocity_of_compositum