Module

AbsoluteFiniteQuotientTransitions.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.AbsoluteFiniteQuotientTransitions

5 declarations indexed from sourceView source ↗

Module documentation

Transition maps between absolute finite quotients

The canonical finite quotient identifications commute with quotient transition on the profinite side and restriction on the Galois side.

Imports2

Imported by2

theorem

absoluteFiniteQuotientPreimage_mono

LocalClassFieldTheory.absoluteFiniteQuotientPreimage_mono

Documentation

Pullback of open normal subgroups is monotone.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open RamificationTheory
variable {K : Type} [Field K]

Lean source · statement

theorem absoluteFiniteQuotientPreimage_mono
    {N M : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)}
    (hNM : N ≤ M) :
    absoluteFiniteQuotientPreimage K N ≤
      absoluteFiniteQuotientPreimage K M

theorem

absoluteFiniteQuotientField_antitone

LocalClassFieldTheory.absoluteFiniteQuotientField_antitone

Documentation

Inclusion of open normal subgroups reverses the corresponding fixed fields.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open RamificationTheory
variable {K : Type} [Field K]

Lean source · statement

theorem absoluteFiniteQuotientField_antitone
    {N M : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)}
    (hNM : N ≤ M) :
    absoluteFiniteQuotientField K M ≤
      absoluteFiniteQuotientField K N

def

absoluteFiniteQuotientTransition

LocalClassFieldTheory.absoluteFiniteQuotientTransition

Documentation

The canonical transition map between two finite quotients.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open RamificationTheory
variable {K : Type} [Field K]

Lean source · statement

def absoluteFiniteQuotientTransition
    {N M : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)}
    (hNM : N ≤ M) :
    localAbsoluteAbelianProfinite K ⧸ N.toSubgroup →ₜ*
      localAbsoluteAbelianProfinite K ⧸ M.toSubgroup

theorem

absoluteFiniteQuotientTransition_mk

LocalClassFieldTheory.absoluteFiniteQuotientTransition_mk

Documentation

States the theorem absoluteFiniteQuotientTransition_mk.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open RamificationTheory
variable {K : Type} [Field K]

Lean source · statement

theorem absoluteFiniteQuotientTransition_mk
    {N M : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)}
    (hNM : N ≤ M) (x : localAbsoluteAbelianProfinite K) :
    absoluteFiniteQuotientTransition hNM (QuotientGroup.mk x) =
      QuotientGroup.mk x

theorem

absoluteFiniteQuotientEquiv_transition

LocalClassFieldTheory.absoluteFiniteQuotientEquiv_transition

Documentation

Under the finite quotient identifications, quotient transition is exactly restriction of automorphisms to the smaller fixed field.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open RamificationTheory
variable {K : Type} [Field K]

Lean source · statement

theorem absoluteFiniteQuotientEquiv_transition
    {N M : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)}
    (hNM : N ≤ M) :
    (intermediateFieldRestrictContinuous K
      (absoluteFiniteQuotientField K M)
      (absoluteFiniteQuotientField K N)
      (absoluteFiniteQuotientField_antitone hNM)).comp
        (ContinuousMonoidHom.toContinuousMonoidHom
          (absoluteFiniteQuotientEquiv K N)) =
      (ContinuousMonoidHom.toContinuousMonoidHom
        (absoluteFiniteQuotientEquiv K M)).comp
          (absoluteFiniteQuotientTransition hNM)