NYLL
Module

FixedFieldContinuousNaturality.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FixedFieldContinuousNaturality
32 declarations indexed from sourceView source ↗

Module documentation

Continuous fixed-field naturality diagrams

The algebraic norm--restriction and transfer--inclusion diagrams are upgraded here to diagrams of continuous homomorphisms. Every finite fixed field uses the spectral norm extended from the original local field. Thus no source is made discrete merely to obtain continuity.

Multiplicative forms of the algebraic arrows

The norm kernel

Continuous arrows

Continuous norm--restriction square

Continuous transfer--inclusion square

Imports3
Imported by2

Declarations

instance

abelianizationQuotientTopologicalSpace

L33 ↗
LocalClassFieldTheory.abelianizationQuotientTopologicalSpace
Documentation

The quotient topology on the algebraic abelianization. Its underlying quotient is opaque to typeclass search, so expose the canonical topology locally while constructing the continuous finite maps.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · statement
instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G)
def

abstractFixedFieldNormResidueMonoidHom

L44 ↗
LocalClassFieldTheory.abstractFixedFieldNormResidueMonoidHom
Documentation

The fixed-field norm-residue symbol on the native multiplicative unit group. This is the multiplicative form of abstractFixedFieldNormResidueSymbol.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
Lean source · statement
def abstractFixedFieldNormResidueMonoidHom
    (D : DegreeData (Gal(Ω/k)))
    (v : ValuationData D (galoisAmbientUnitsRep k Ω))
    (hcf : SatisfiesClassFieldAxiom (galoisAmbientUnitsRep k Ω))
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup K L hLK).Normal]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    [hKabsolute : Finite
      ((baseField (Gal(Ω/k))).toSubgroup ⧸
        extensionSubgroup (baseField (Gal(Ω/k))) K
          (le_baseField K))] :
    (abstractFixedField k Ω K)ˣ →*
      Abelianization
        Gal(abstractRelativeFixedField k Ω hLK /
          abstractFixedField k Ω K)
def

abstractFixedFieldNormUnitsMonoidHom

L66 ↗
LocalClassFieldTheory.abstractFixedFieldNormUnitsMonoidHom
Documentation

The ordinary fixed-field norm on native multiplicative unit groups.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
Lean source · statement
def abstractFixedFieldNormUnitsMonoidHom
    (K K' : ClosedSubgroup (Gal(Ω/k)))
    (hK'K : K'.toSubgroup ≤ K.toSubgroup) :
    (abstractRelativeFixedField k Ω hK'K)ˣ →*
      (abstractFixedField k Ω K)ˣ
def

abstractFixedFieldUnitsInclusionMonoidHom

L75 ↗
LocalClassFieldTheory.abstractFixedFieldUnitsInclusionMonoidHom
Documentation

Inclusion of native multiplicative fixed-field unit groups.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
Lean source · statement
def abstractFixedFieldUnitsInclusionMonoidHom
    (K K' : ClosedSubgroup (Gal(Ω/k)))
    (hK'K : K'.toSubgroup ≤ K.toSubgroup) :
    (abstractFixedField k Ω K)ˣ →*
      (abstractFixedField k Ω K')ˣ
def

abstractFixedFieldAbelianizedRestrictionMonoidHom

L84 ↗
LocalClassFieldTheory.abstractFixedFieldAbelianizedRestrictionMonoidHom
Documentation

Restriction on native multiplicative finite abelianizations.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
Lean source · statement
def abstractFixedFieldAbelianizedRestrictionMonoidHom
    (K K' L L' : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    [hL'normal : (extensionSubgroup K' L' hL'K').Normal] :
    Abelianization
        Gal(abstractRelativeFixedField k Ω hL'K' /
          abstractFixedField k Ω K') →*
      Abelianization
        Gal(abstractRelativeFixedField k Ω hLK /
          abstractFixedField k Ω K)
def

abstractFixedFieldAbelianizedTransferMonoidHom

L103 ↗
LocalClassFieldTheory.abstractFixedFieldAbelianizedTransferMonoidHom
Documentation

Transfer on native multiplicative finite abelianizations.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
Lean source · full declaration
def abstractFixedFieldAbelianizedTransferMonoidHom
    (K K' L : ClosedSubgroup (Gal(Ω/k)))
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal :
      (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [hLfinite : Finite
      (K.toSubgroup ⧸
        extensionSubgroup K L (hLK'.trans hK'K))] :
    letI : (extensionSubgroup K' L hLK').Normal :=
      transferNormNaturality_intermediateExtension_normal
        K K' L hLK' hK'K
    letI : Finite
        (K'.toSubgroup ⧸ extensionSubgroup K' L hLK') :=
      FiniteGaloisSubextension.finite_extension_over_intermediate
        (hLK'.trans hK'K) hK'K hLK'
    Abelianization
        Gal(abstractRelativeFixedField k Ω
            (hLK'.trans hK'K) /
          abstractFixedField k Ω K) →*
      Abelianization
        Gal(abstractRelativeFixedField k Ω hLK' /
          abstractFixedField k Ω K') :=
  MonoidHom.toAdditive.symm
    (abstractFixedFieldAbelianizedTransfer
      k Ω K K' L hLK' hK'K)
theorem

abstractFixedFieldUnitsEquiv_finiteNormSubgroup_preimage

L134 ↗
LocalClassFieldTheory.abstractFixedFieldUnitsEquiv_finiteNormSubgroup_preimage
Documentation

Under the concrete fixed-unit equivalence, the finite abstract norm subgroup pulls back to the ordinary field-norm subgroup.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
Lean source · statement
theorem abstractFixedFieldUnitsEquiv_finiteNormSubgroup_preimage
    [IsSepClosed Ω]
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    [hKabsolute : Finite
      ((baseField (Gal(Ω/k))).toSubgroup ⧸
        extensionSubgroup (baseField (Gal(Ω/k))) K
          (le_baseField K))] :
    (finiteNormSubgroup (galoisAmbientUnitsRep k Ω)
        K L hLK).comap
      (abstractFixedFieldUnitsEquivGaloisFixed
        k Ω K).toAddMonoidHom =
      additiveNormSubgroup
        (abstractFixedField k Ω K)
        (abstractRelativeFixedField k Ω hLK)
theorem

abstractFixedFieldNormResidueSymbol_ker

L188 ↗
LocalClassFieldTheory.abstractFixedFieldNormResidueSymbol_ker
Documentation

The kernel of the additive fixed-field norm-residue symbol is the ordinary norm subgroup, written additively.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
Lean source · statement
theorem abstractFixedFieldNormResidueSymbol_ker
    (D : DegreeData (Gal(Ω/k)))
    (v : ValuationData D (galoisAmbientUnitsRep k Ω))
    (hcf : SatisfiesClassFieldAxiom (galoisAmbientUnitsRep k Ω))
    [IsSepClosed Ω]
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup K L hLK).Normal]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    [hKabsolute : Finite
      ((baseField (Gal(Ω/k))).toSubgroup ⧸
        extensionSubgroup (baseField (Gal(Ω/k))) K
          (le_baseField K))] :
    (abstractFixedFieldNormResidueSymbol
      k Ω D v hcf K L hLK).ker =
      additiveNormSubgroup
        (abstractFixedField k Ω K)
        (abstractRelativeFixedField k Ω hLK)
theorem

abstractFixedFieldNormResidueMonoidHom_ker

L236 ↗
LocalClassFieldTheory.abstractFixedFieldNormResidueMonoidHom_ker
Documentation

The kernel of the multiplicative fixed-field norm-residue homomorphism is the ordinary norm subgroup.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
Lean source · statement
theorem abstractFixedFieldNormResidueMonoidHom_ker
    (D : DegreeData (Gal(Ω/k)))
    (v : ValuationData D (galoisAmbientUnitsRep k Ω))
    (hcf : SatisfiesClassFieldAxiom (galoisAmbientUnitsRep k Ω))
    [IsSepClosed Ω]
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup K L hLK).Normal]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    [hKabsolute : Finite
      ((baseField (Gal(Ω/k))).toSubgroup ⧸
        extensionSubgroup (baseField (Gal(Ω/k))) K
          (le_baseField K))] :
    (abstractFixedFieldNormResidueMonoidHom
      k Ω D v hcf K L hLK).ker =
      localNormSubgroup
        (abstractFixedField k Ω K)
        (abstractRelativeFixedField k Ω hLK)
def

abstractFixedFieldNormResidueMap

L265 ↗
LocalClassFieldTheory.abstractFixedFieldNormResidueMap
Documentation

The fixed-field norm-residue symbol, bundled as a genuinely continuous homomorphism for the spectral topology on the source field.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
Lean source · full declaration
def abstractFixedFieldNormResidueMap
    [ValuativeRel k] [TopologicalSpace k]
    [IsNonarchimedeanLocalField k]
    [IsSepClosed Ω]
    (D : DegreeData (Gal(Ω/k)))
    (v : ValuationData D (galoisAmbientUnitsRep k Ω))
    (hcf : SatisfiesClassFieldAxiom (galoisAmbientUnitsRep k Ω))
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup K L hLK).Normal]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    [hKabsolute : Finite
      ((baseField (Gal(Ω/k))).toSubgroup ⧸
        extensionSubgroup (baseField (Gal(Ω/k))) K
          (le_baseField K))] :
    letI : FiniteDimensional k (abstractFixedField k Ω K) :=
      abstractFixedField_finiteDimensional k Ω K hKabsolute
    letI : NontriviallyNormedField (abstractFixedField k Ω K) :=
      finiteExtensionSpectralNormedField k (abstractFixedField k Ω K)
    (abstractFixedField k Ω K)ˣ →ₜ*
      Abelianization
        Gal(abstractRelativeFixedField k Ω hLK /
          abstractFixedField k Ω K) := by
  let F := abstractFixedField k Ω K
  let E := abstractRelativeFixedField k Ω hLK
  letI : FiniteDimensional k F :=
    abstractFixedField_finiteDimensional k Ω K hKabsolute
  letI : NontriviallyNormedField F :=
    finiteExtensionSpectralNormedField k F
  letI : CompleteSpace F := finiteExtensionSpectralCompleteSpace k F
  letI : ValuativeRel F := finiteExtensionSpectralValuativeRel k F
  letI : IsNonarchimedeanLocalField F :=
    finiteExtensionSpectralIsNonarchimedeanLocalField k F
  letI : FiniteDimensional F E :=
    abstractRelativeFixedField_finiteDimensional
      k Ω K L hLK hKabsolute hfinite
  letI : IsGalois F E :=
    abstractRelativeFixedField_isGalois k Ω K L hLK hnormal
  letI : DiscreteTopology (Abelianization Gal(E / F)) :=
    QuotientGroup.discreteTopology (isOpen_discrete _)
  let f := abstractFixedFieldNormResidueMonoidHom
    k Ω D v hcf K L hLK
  refine { f with continuous_toFun := ?_ }
  apply continuous_of_continuousAt_one f
  rw [ContinuousAt, map_one,
    @nhds_discrete (Abelianization Gal(E / F)) _ _, Filter.tendsto_pure]
  have hopen : IsOpen (f.ker : Set Fˣ) := by
    rw [abstractFixedFieldNormResidueMonoidHom_ker
      k Ω D v hcf K L hLK]
    exact localNormSubgroup_isOpen F E
  exact hopen.mem_nhds (by simp)
def

abstractFixedFieldNormUnitsMap

L320 ↗
LocalClassFieldTheory.abstractFixedFieldNormUnitsMap
Documentation

The ordinary norm on fixed-field units, continuously bundled for the two spectral topologies extended from the original local field.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
Lean source · full declaration
def abstractFixedFieldNormUnitsMap
    [ValuativeRel k] [TopologicalSpace k]
    [IsNonarchimedeanLocalField k]
    (K K' : ClosedSubgroup (Gal(Ω/k)))
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hKabsolute : Finite
      ((baseField (Gal(Ω/k))).toSubgroup ⧸
        extensionSubgroup (baseField (Gal(Ω/k))) K
          (le_baseField K))]
    [hK'absolute : Finite
      ((baseField (Gal(Ω/k))).toSubgroup ⧸
        extensionSubgroup (baseField (Gal(Ω/k))) K'
          (le_baseField K'))]
    [hK'Kfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K K' hK'K)] :
    letI : FiniteDimensional k (abstractFixedField k Ω K) :=
      abstractFixedField_finiteDimensional k Ω K hKabsolute
    letI : FiniteDimensional k
        (abstractRelativeFixedField k Ω hK'K) :=
      abstractFixedField_finiteDimensional k Ω K' hK'absolute
    letI : NontriviallyNormedField (abstractFixedField k Ω K) :=
      finiteExtensionSpectralNormedField k (abstractFixedField k Ω K)
    letI : NontriviallyNormedField
        (abstractRelativeFixedField k Ω hK'K) :=
      finiteExtensionSpectralNormedField k
        (abstractRelativeFixedField k Ω hK'K)
    (abstractRelativeFixedField k Ω hK'K)ˣ →ₜ*
      (abstractFixedField k Ω K)ˣ := by
  let F := abstractFixedField k Ω K
  let F' := abstractRelativeFixedField k Ω hK'K
  letI : FiniteDimensional k F :=
    abstractFixedField_finiteDimensional k Ω K hKabsolute
  letI : FiniteDimensional k F' :=
    abstractFixedField_finiteDimensional k Ω K' hK'absolute
  letI : NontriviallyNormedField F :=
    finiteExtensionSpectralNormedField k F
  letI : NontriviallyNormedField F' :=
    finiteExtensionSpectralNormedField k F'
  letI : IsScalarTower k F F' := IsScalarTower.of_algebraMap_eq' rfl
  letI : FiniteDimensional F F' :=
    abstractRelativeFixedField_finiteDimensional
      k Ω K K' hK'K hKabsolute hK'Kfinite
  letI : CompleteSpace F := finiteExtensionSpectralCompleteSpace k F
  letI : NormedAlgebra F F' :=
    finiteExtensionSpectralNormedAlgebra k F F'
  let f := abstractFixedFieldNormUnitsMonoidHom
    k Ω K K' hK'K
  refine { f with continuous_toFun := ?_ }
  change Continuous (LocalFieldTheory.normUnits F F')
  exact normUnits_continuous_of_finiteDimensional F F'
def

abstractFixedFieldUnitsInclusionMap

L373 ↗
LocalClassFieldTheory.abstractFixedFieldUnitsInclusionMap
Documentation

Inclusion of fixed-field units, continuously bundled for the two spectral topologies extended from the original local field.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
Lean source · full declaration
def abstractFixedFieldUnitsInclusionMap
    [ValuativeRel k] [TopologicalSpace k]
    [IsNonarchimedeanLocalField k]
    (K K' : ClosedSubgroup (Gal(Ω/k)))
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hKabsolute : Finite
      ((baseField (Gal(Ω/k))).toSubgroup ⧸
        extensionSubgroup (baseField (Gal(Ω/k))) K
          (le_baseField K))]
    [hK'absolute : Finite
      ((baseField (Gal(Ω/k))).toSubgroup ⧸
        extensionSubgroup (baseField (Gal(Ω/k))) K'
          (le_baseField K'))] :
    letI : FiniteDimensional k (abstractFixedField k Ω K) :=
      abstractFixedField_finiteDimensional k Ω K hKabsolute
    letI : FiniteDimensional k (abstractFixedField k Ω K') :=
      abstractFixedField_finiteDimensional k Ω K' hK'absolute
    letI : NontriviallyNormedField (abstractFixedField k Ω K) :=
      finiteExtensionSpectralNormedField k (abstractFixedField k Ω K)
    letI : NontriviallyNormedField (abstractFixedField k Ω K') :=
      finiteExtensionSpectralNormedField k (abstractFixedField k Ω K')
    (abstractFixedField k Ω K)ˣ →ₜ*
      (abstractFixedField k Ω K')ˣ := by
  let F := abstractFixedField k Ω K
  let F' := abstractFixedField k Ω K'
  letI : FiniteDimensional k F :=
    abstractFixedField_finiteDimensional k Ω K hKabsolute
  letI : FiniteDimensional k F' :=
    abstractFixedField_finiteDimensional k Ω K' hK'absolute
  letI : NontriviallyNormedField F :=
    finiteExtensionSpectralNormedField k F
  letI : NontriviallyNormedField F' :=
    finiteExtensionSpectralNormedField k F'
  letI : NontriviallyNormedField k :=
    localFieldNontriviallyNormedField k
  letI : IsUltrametricDist k := localFieldIsUltrametricDist k
  letI : CompleteSpace k := inferInstance
  letI : NormedSpace k F := spectralNorm.normedSpace k F
  letI : NormedSpace k F' := spectralNorm.normedSpace k F'
  let f := abstractFixedFieldUnitsInclusionMonoidHom
    k Ω K K' hK'K
  refine { f with continuous_toFun := ?_ }
  exact Continuous.units_map _
    (IntermediateField.inclusion
      (abstractFixedField_le k Ω hK'K)).toLinearMap.continuous_of_finiteDimensional
def

abstractFixedFieldAbelianizedRestrictionMap

L421 ↗
LocalClassFieldTheory.abstractFixedFieldAbelianizedRestrictionMap
Documentation

Abelianized restriction, continuously bundled for the finite native Krull quotient topologies.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
Lean source · statement
def abstractFixedFieldAbelianizedRestrictionMap
    (K K' L L' : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    [hL'normal : (extensionSubgroup K' L' hL'K').Normal]
    [hL'K'finite : Finite
      (K'.toSubgroup ⧸ extensionSubgroup K' L' hL'K')]
    [hK'absolute : Finite
      ((baseField (Gal(Ω/k))).toSubgroup ⧸
        extensionSubgroup (baseField (Gal(Ω/k))) K'
          (le_baseField K'))] :
    Abelianization
        Gal(abstractRelativeFixedField k Ω hL'K' /
          abstractFixedField k Ω K') →ₜ*
      Abelianization
        Gal(abstractRelativeFixedField k Ω hLK /
          abstractFixedField k Ω K)
def

abstractFixedFieldAbelianizedTransferMap

L457 ↗
LocalClassFieldTheory.abstractFixedFieldAbelianizedTransferMap
Documentation

Abelianized transfer, continuously bundled for the finite native Krull quotient topologies.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
Lean source · full declaration
def abstractFixedFieldAbelianizedTransferMap
    (K K' L : ClosedSubgroup (Gal(Ω/k)))
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal :
      (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [hLfinite : Finite
      (K.toSubgroup ⧸
        extensionSubgroup K L (hLK'.trans hK'K))]
    [hKabsolute : Finite
      ((baseField (Gal(Ω/k))).toSubgroup ⧸
        extensionSubgroup (baseField (Gal(Ω/k))) K
          (le_baseField K))] :
    letI : (extensionSubgroup K' L hLK').Normal :=
      transferNormNaturality_intermediateExtension_normal
        K K' L hLK' hK'K
    letI : Finite
        (K'.toSubgroup ⧸ extensionSubgroup K' L hLK') :=
      FiniteGaloisSubextension.finite_extension_over_intermediate
        (hLK'.trans hK'K) hK'K hLK'
    Abelianization
        Gal(abstractRelativeFixedField k Ω
            (hLK'.trans hK'K) /
          abstractFixedField k Ω K) →ₜ*
      Abelianization
        Gal(abstractRelativeFixedField k Ω hLK' /
          abstractFixedField k Ω K') := by
  letI : (extensionSubgroup K' L hLK').Normal :=
    transferNormNaturality_intermediateExtension_normal
      K K' L hLK' hK'K
  letI : Finite
      (K'.toSubgroup ⧸ extensionSubgroup K' L hLK') :=
    FiniteGaloisSubextension.finite_extension_over_intermediate
      (hLK'.trans hK'K) hK'K hLK'
  let F := abstractFixedField k Ω K
  let E := abstractRelativeFixedField k Ω
    (hLK'.trans hK'K)
  letI : FiniteDimensional F E :=
    abstractRelativeFixedField_finiteDimensional
      k Ω K L (hLK'.trans hK'K) hKabsolute hLfinite
  letI : IsGalois F E :=
    abstractRelativeFixedField_isGalois
      k Ω K L (hLK'.trans hK'K) hLnormal
  letI : DiscreteTopology (Abelianization Gal(E / F)) :=
    QuotientGroup.discreteTopology (isOpen_discrete _)
  let f := abstractFixedFieldAbelianizedTransferMonoidHom
    k Ω K K' L hLK' hK'K
  exact { f with continuous_toFun := continuous_of_discreteTopology }
def

lowerNormResidueMap

L514 ↗
LocalClassFieldTheory.LocalFixedFieldNormRestrictionSquare.lowerNormResidueMap
Documentation

The lower horizontal norm-residue arrow as a continuous homomorphism.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldNormRestrictionSquare
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · full declaration
def lowerNormResidueMap
    (T : LocalFixedFieldNormRestrictionSquare k) :
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.lowerBase) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.lowerBase T.lowerAbsoluteFinite
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.lowerBase) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.lowerBase)
    (abstractFixedField k (SeparableClosure k) T.lowerBase)ˣ →ₜ*
      Abelianization
        Gal(abstractRelativeFixedField k (SeparableClosure k)
            T.lowerTop_le_lowerBase /
          abstractFixedField k (SeparableClosure k) T.lowerBase) := by
  letI := T.lowerNormal
  letI := T.lowerFinite
  letI := T.lowerAbsoluteFinite
  exact abstractFixedFieldNormResidueMap
    k (SeparableClosure k)
    (localResidueDatum k) (localHenselianValuation k)
    (separableClosureUnits_isClassFormation k)
    T.lowerBase T.lowerTop T.lowerTop_le_lowerBase
theorem

lowerNormResidueMap_toMonoidHom

L539 ↗
LocalClassFieldTheory.LocalFixedFieldNormRestrictionSquare.lowerNormResidueMap_toMonoidHom
Documentation

Forgetting continuity recovers the lower algebraic norm-residue map.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldNormRestrictionSquare
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · full declaration
theorem lowerNormResidueMap_toMonoidHom
    (T : LocalFixedFieldNormRestrictionSquare k) :
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.lowerBase) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.lowerBase T.lowerAbsoluteFinite
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.lowerBase) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.lowerBase)
    (lowerNormResidueMap T).toMonoidHom =
      MonoidHom.toAdditive.symm (lowerNormResidueSymbol T) := rfl
def

upperNormResidueMap

L553 ↗
LocalClassFieldTheory.LocalFixedFieldNormRestrictionSquare.upperNormResidueMap
Documentation

The upper horizontal norm-residue arrow as a continuous homomorphism.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldNormRestrictionSquare
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · full declaration
def upperNormResidueMap
    (T : LocalFixedFieldNormRestrictionSquare k) :
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.upperBase) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.upperBase (upperAbsoluteFinite T)
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.upperBase) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.upperBase)
    (abstractFixedField k (SeparableClosure k) T.upperBase)ˣ →ₜ*
      Abelianization
        Gal(abstractRelativeFixedField k (SeparableClosure k)
            T.upperTop_le_upperBase /
          abstractFixedField k (SeparableClosure k) T.upperBase) := by
  letI := T.upperNormal
  letI := T.upperFinite
  letI := upperAbsoluteFinite T
  exact abstractFixedFieldNormResidueMap
    k (SeparableClosure k)
    (localResidueDatum k) (localHenselianValuation k)
    (separableClosureUnits_isClassFormation k)
    T.upperBase T.upperTop T.upperTop_le_upperBase
theorem

upperNormResidueMap_toMonoidHom

L578 ↗
LocalClassFieldTheory.LocalFixedFieldNormRestrictionSquare.upperNormResidueMap_toMonoidHom
Documentation

Forgetting continuity recovers the upper algebraic norm-residue map.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldNormRestrictionSquare
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · full declaration
theorem upperNormResidueMap_toMonoidHom
    (T : LocalFixedFieldNormRestrictionSquare k) :
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.upperBase) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.upperBase (upperAbsoluteFinite T)
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.upperBase) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.upperBase)
    (upperNormResidueMap T).toMonoidHom =
      MonoidHom.toAdditive.symm (upperNormResidueSymbol T) := rfl
def

normUnitsMap

L592 ↗
LocalClassFieldTheory.LocalFixedFieldNormRestrictionSquare.normUnitsMap
Documentation

The vertical ordinary norm arrow as a continuous homomorphism.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldNormRestrictionSquare
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · full declaration
def normUnitsMap
    (T : LocalFixedFieldNormRestrictionSquare k) :
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.lowerBase) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.lowerBase T.lowerAbsoluteFinite
    letI : FiniteDimensional k
        (abstractRelativeFixedField k (SeparableClosure k)
          T.upperBase_le_lowerBase) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.upperBase (upperAbsoluteFinite T)
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.lowerBase) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.lowerBase)
    letI : NontriviallyNormedField
        (abstractRelativeFixedField k (SeparableClosure k)
          T.upperBase_le_lowerBase) :=
      finiteExtensionSpectralNormedField k
        (abstractRelativeFixedField k (SeparableClosure k)
          T.upperBase_le_lowerBase)
    (abstractRelativeFixedField k (SeparableClosure k)
        T.upperBase_le_lowerBase)ˣ →ₜ*
      (abstractFixedField k (SeparableClosure k) T.lowerBase)ˣ := by
  letI := T.lowerAbsoluteFinite
  letI := upperAbsoluteFinite T
  letI := T.baseFinite
  exact abstractFixedFieldNormUnitsMap
    k (SeparableClosure k)
    T.lowerBase T.upperBase T.upperBase_le_lowerBase
theorem

normUnitsMap_toMonoidHom

L624 ↗
LocalClassFieldTheory.LocalFixedFieldNormRestrictionSquare.normUnitsMap_toMonoidHom
Documentation

Forgetting continuity recovers the algebraic norm on units.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldNormRestrictionSquare
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · full declaration
theorem normUnitsMap_toMonoidHom
    (T : LocalFixedFieldNormRestrictionSquare k) :
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.lowerBase) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.lowerBase T.lowerAbsoluteFinite
    letI : FiniteDimensional k
        (abstractRelativeFixedField k (SeparableClosure k)
          T.upperBase_le_lowerBase) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.upperBase (upperAbsoluteFinite T)
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.lowerBase) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.lowerBase)
    letI : NontriviallyNormedField
        (abstractRelativeFixedField k (SeparableClosure k)
          T.upperBase_le_lowerBase) :=
      finiteExtensionSpectralNormedField k
        (abstractRelativeFixedField k (SeparableClosure k)
          T.upperBase_le_lowerBase)
    (normUnitsMap T).toMonoidHom =
      MonoidHom.toAdditive.symm (normUnits T) := rfl
def

abelianizedRestrictionMap

L650 ↗
LocalClassFieldTheory.LocalFixedFieldNormRestrictionSquare.abelianizedRestrictionMap
Documentation

The vertical abelianized restriction arrow as a continuous homomorphism.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldNormRestrictionSquare
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · statement
def abelianizedRestrictionMap
    (T : LocalFixedFieldNormRestrictionSquare k)
theorem

abelianizedRestrictionMap_toMonoidHom

L663 ↗
LocalClassFieldTheory.LocalFixedFieldNormRestrictionSquare.abelianizedRestrictionMap_toMonoidHom
Documentation

Forgetting continuity recovers algebraic abelianized restriction.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldNormRestrictionSquare
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · statement
theorem abelianizedRestrictionMap_toMonoidHom
    (T : LocalFixedFieldNormRestrictionSquare k) :
    (abelianizedRestrictionMap T).toMonoidHom =
      MonoidHom.toAdditive.symm (abelianizedRestriction T)
theorem

norm_restriction_commutes_continuous

L670 ↗
LocalClassFieldTheory.LocalFixedFieldNormRestrictionSquare.norm_restriction_commutes_continuous
Documentation

Norm--restriction naturality as a commuting square of continuous homomorphisms.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldNormRestrictionSquare
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · full declaration
theorem norm_restriction_commutes_continuous
    (T : LocalFixedFieldNormRestrictionSquare k) :
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.lowerBase) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.lowerBase T.lowerAbsoluteFinite
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.upperBase) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.upperBase (upperAbsoluteFinite T)
    letI : FiniteDimensional k
        (abstractRelativeFixedField k (SeparableClosure k)
          T.upperBase_le_lowerBase) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.upperBase (upperAbsoluteFinite T)
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.lowerBase) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.lowerBase)
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.upperBase) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.upperBase)
    letI : NontriviallyNormedField
        (abstractRelativeFixedField k (SeparableClosure k)
          T.upperBase_le_lowerBase) :=
      finiteExtensionSpectralNormedField k
        (abstractRelativeFixedField k (SeparableClosure k)
          T.upperBase_le_lowerBase)
    (abelianizedRestrictionMap T).comp (upperNormResidueMap T) =
      (lowerNormResidueMap T).comp (normUnitsMap T) := by
  let : FiniteDimensional k
      (abstractFixedField k (SeparableClosure k) T.lowerBase) :=
    abstractFixedField_finiteDimensional
      k (SeparableClosure k) T.lowerBase T.lowerAbsoluteFinite
  let : FiniteDimensional k
      (abstractFixedField k (SeparableClosure k) T.upperBase) :=
    abstractFixedField_finiteDimensional
      k (SeparableClosure k) T.upperBase (upperAbsoluteFinite T)
  let : FiniteDimensional k
      (abstractRelativeFixedField k (SeparableClosure k)
        T.upperBase_le_lowerBase) :=
    abstractFixedField_finiteDimensional
      k (SeparableClosure k) T.upperBase (upperAbsoluteFinite T)
  let : NontriviallyNormedField
      (abstractFixedField k (SeparableClosure k) T.lowerBase) :=
    finiteExtensionSpectralNormedField k
      (abstractFixedField k (SeparableClosure k) T.lowerBase)
  let : NontriviallyNormedField
      (abstractFixedField k (SeparableClosure k) T.upperBase) :=
    finiteExtensionSpectralNormedField k
      (abstractFixedField k (SeparableClosure k) T.upperBase)
  let : NontriviallyNormedField
      (abstractRelativeFixedField k (SeparableClosure k)
        T.upperBase_le_lowerBase) :=
    finiteExtensionSpectralNormedField k
      (abstractRelativeFixedField k (SeparableClosure k)
        T.upperBase_le_lowerBase)
  apply ContinuousMonoidHom.ext
  intro x
  change Additive.toMul
      (abelianizedRestriction T
        (upperNormResidueSymbol T (Additive.ofMul x))) =
    Additive.toMul
      (lowerNormResidueSymbol T
        (normUnits T (Additive.ofMul x)))
  exact congrArg Additive.toMul
    (DFunLike.congr_fun (norm_restriction_commutes T)
      (Additive.ofMul x))
def

baseNormResidueMap

L750 ↗
LocalClassFieldTheory.LocalFixedFieldTransferTower.baseNormResidueMap
Documentation

The total horizontal norm-residue arrow as a continuous homomorphism.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · full declaration
def baseNormResidueMap
    (T : LocalFixedFieldTransferTower k) :
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.base) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.base T.baseAbsoluteFinite
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.base) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.base)
    (abstractFixedField k (SeparableClosure k) T.base)ˣ →ₜ*
      Abelianization
        Gal(abstractRelativeFixedField k (SeparableClosure k)
            (T.top_le_intermediate.trans T.intermediate_le_base) /
          abstractFixedField k (SeparableClosure k) T.base) := by
  letI := T.totalNormal
  letI := T.totalFinite
  letI := T.baseAbsoluteFinite
  exact abstractFixedFieldNormResidueMap
    k (SeparableClosure k)
    (localResidueDatum k) (localHenselianValuation k)
    (separableClosureUnits_isClassFormation k)
    T.base T.top
    (T.top_le_intermediate.trans T.intermediate_le_base)
theorem

baseNormResidueMap_toMonoidHom

L776 ↗
LocalClassFieldTheory.LocalFixedFieldTransferTower.baseNormResidueMap_toMonoidHom
Documentation

Forgetting continuity recovers the total algebraic norm-residue map.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · full declaration
theorem baseNormResidueMap_toMonoidHom
    (T : LocalFixedFieldTransferTower k) :
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.base) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.base T.baseAbsoluteFinite
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.base) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.base)
    (baseNormResidueMap T).toMonoidHom =
      MonoidHom.toAdditive.symm (baseNormResidueSymbol T) := rfl
def

intermediateNormResidueMap

L791 ↗
LocalClassFieldTheory.LocalFixedFieldTransferTower.intermediateNormResidueMap
Documentation

The intermediate horizontal norm-residue arrow as a continuous homomorphism.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · full declaration
def intermediateNormResidueMap
    (T : LocalFixedFieldTransferTower k) :
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.intermediate) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.intermediate
          (intermediateAbsoluteFinite T)
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.intermediate) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.intermediate)
    (abstractFixedField k (SeparableClosure k) T.intermediate)ˣ →ₜ*
      Abelianization
        Gal(abstractRelativeFixedField k (SeparableClosure k)
            T.top_le_intermediate /
          abstractFixedField k (SeparableClosure k) T.intermediate) := by
  letI := intermediateNormal T
  letI := intermediateFinite T
  letI := intermediateAbsoluteFinite T
  exact abstractFixedFieldNormResidueMap
    k (SeparableClosure k)
    (localResidueDatum k) (localHenselianValuation k)
    (separableClosureUnits_isClassFormation k)
    T.intermediate T.top T.top_le_intermediate
theorem

intermediateNormResidueMap_toMonoidHom

L817 ↗
LocalClassFieldTheory.LocalFixedFieldTransferTower.intermediateNormResidueMap_toMonoidHom
Documentation

Forgetting continuity recovers the intermediate norm-residue map.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · full declaration
theorem intermediateNormResidueMap_toMonoidHom
    (T : LocalFixedFieldTransferTower k) :
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.intermediate) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.intermediate
          (intermediateAbsoluteFinite T)
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.intermediate) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.intermediate)
    (intermediateNormResidueMap T).toMonoidHom =
      MonoidHom.toAdditive.symm (intermediateNormResidueSymbol T) := rfl
def

unitsInclusionMap

L833 ↗
LocalClassFieldTheory.LocalFixedFieldTransferTower.unitsInclusionMap
Documentation

The vertical inclusion of fixed-field units as a continuous homomorphism.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · full declaration
def unitsInclusionMap
    (T : LocalFixedFieldTransferTower k) :
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.base) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.base T.baseAbsoluteFinite
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.intermediate) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.intermediate
          (intermediateAbsoluteFinite T)
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.base) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.base)
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.intermediate) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.intermediate)
    (abstractFixedField k (SeparableClosure k) T.base)ˣ →ₜ*
      (abstractFixedField k (SeparableClosure k) T.intermediate)ˣ := by
  letI := T.baseAbsoluteFinite
  letI := intermediateAbsoluteFinite T
  exact abstractFixedFieldUnitsInclusionMap
    k (SeparableClosure k)
    T.base T.intermediate T.intermediate_le_base
theorem

unitsInclusionMap_toMonoidHom

L861 ↗
LocalClassFieldTheory.LocalFixedFieldTransferTower.unitsInclusionMap_toMonoidHom
Documentation

Forgetting continuity recovers algebraic inclusion of fixed-field units.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · full declaration
theorem unitsInclusionMap_toMonoidHom
    (T : LocalFixedFieldTransferTower k) :
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.base) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.base T.baseAbsoluteFinite
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.intermediate) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.intermediate
          (intermediateAbsoluteFinite T)
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.base) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.base)
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.intermediate) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.intermediate)
    (unitsInclusionMap T).toMonoidHom =
      MonoidHom.toAdditive.symm (unitsInclusion T) := rfl
def

abelianizedTransferMap

L884 ↗
LocalClassFieldTheory.LocalFixedFieldTransferTower.abelianizedTransferMap
Documentation

The vertical abelianized transfer arrow as a continuous homomorphism.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · statement
def abelianizedTransferMap
    (T : LocalFixedFieldTransferTower k)
theorem

abelianizedTransferMap_toMonoidHom

L895 ↗
LocalClassFieldTheory.LocalFixedFieldTransferTower.abelianizedTransferMap_toMonoidHom
Documentation

Forgetting continuity recovers algebraic abelianized transfer.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · statement
theorem abelianizedTransferMap_toMonoidHom
    (T : LocalFixedFieldTransferTower k) :
    (abelianizedTransferMap T).toMonoidHom =
      MonoidHom.toAdditive.symm (abelianizedTransfer T)
theorem

transfer_inclusion_commutes_continuous

L902 ↗
LocalClassFieldTheory.LocalFixedFieldTransferTower.transfer_inclusion_commutes_continuous
Documentation

Transfer--inclusion naturality as a commuting square of continuous homomorphisms.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
/-- The quotient topology on the algebraic abelianization.  Its underlying
quotient is opaque to typeclass search, so expose the canonical topology
locally while constructing the continuous finite maps. -/
private local instance abelianizationQuotientTopologicalSpace
    (G : Type*) [Group G] [TopologicalSpace G] :
    TopologicalSpace (Abelianization G) := by
  change TopologicalSpace (G ⧸ commutator G)
  exact QuotientGroup.instTopologicalSpace (commutator G)
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
  [IsNonarchimedeanLocalField k]
Lean source · full declaration
theorem transfer_inclusion_commutes_continuous
    (T : LocalFixedFieldTransferTower k) :
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.base) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.base T.baseAbsoluteFinite
    letI : FiniteDimensional k
        (abstractFixedField k (SeparableClosure k) T.intermediate) :=
      abstractFixedField_finiteDimensional
        k (SeparableClosure k) T.intermediate
          (intermediateAbsoluteFinite T)
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.base) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.base)
    letI : NontriviallyNormedField
        (abstractFixedField k (SeparableClosure k) T.intermediate) :=
      finiteExtensionSpectralNormedField k
        (abstractFixedField k (SeparableClosure k) T.intermediate)
    (abelianizedTransferMap T).comp (baseNormResidueMap T) =
      (intermediateNormResidueMap T).comp (unitsInclusionMap T) := by
  let : FiniteDimensional k
      (abstractFixedField k (SeparableClosure k) T.base) :=
    abstractFixedField_finiteDimensional
      k (SeparableClosure k) T.base T.baseAbsoluteFinite
  let : FiniteDimensional k
      (abstractFixedField k (SeparableClosure k) T.intermediate) :=
    abstractFixedField_finiteDimensional
      k (SeparableClosure k) T.intermediate
        (intermediateAbsoluteFinite T)
  let : NontriviallyNormedField
      (abstractFixedField k (SeparableClosure k) T.base) :=
    finiteExtensionSpectralNormedField k
      (abstractFixedField k (SeparableClosure k) T.base)
  let : NontriviallyNormedField
      (abstractFixedField k (SeparableClosure k) T.intermediate) :=
    finiteExtensionSpectralNormedField k
      (abstractFixedField k (SeparableClosure k) T.intermediate)
  apply ContinuousMonoidHom.ext
  intro x
  change Additive.toMul
      (abelianizedTransfer T
        (baseNormResidueSymbol T (Additive.ofMul x))) =
    Additive.toMul
      (intermediateNormResidueSymbol T
        (unitsInclusion T (Additive.ofMul x)))
  exact congrArg Additive.toMul
    (DFunLike.congr_fun (transfer_inclusion_commutes T)
      (Additive.ofMul x))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.