NYLL
Module

SeparableFixedFieldNorm.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.SeparableFixedFieldNorm
10 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: norms from arbitrary finite separable fixed fields

The henselian condition in the abstract class-formation framework quantifies over every finite abstract field, not only over normal ones. For an intermediate finite separable field E in a separably closed Galois ambient field, the left cosets of Gal(Ω / E) are canonically the K-embeddings E → Ω. This file uses that identification to compare the abstract class-formation coset norm with the ordinary field norm, without a normality assumption on E / K.

Imports3
Imported by3

Declarations

def

baseFixingCosetToAlgHom

L45 ↗
LocalClassFieldTheory.baseFixingCosetToAlgHom
Documentation

Restriction to E sends a left coset of Gal(Ω/E) to the corresponding K-embedding of E into Ω.

Source context 9 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω] [IsSepClosed Ω]
section CosetsAndEmbeddings
variable (E : IntermediateField K Ω)
Lean source · statement
def baseFixingCosetToAlgHom :
    ((closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω)).toSubgroup ⧸
      extensionSubgroup
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E)) →
      (E →ₐ[K] Ω)
theorem

baseFixingCosetToAlgHom_mk

L84 ↗
LocalClassFieldTheory.baseFixingCosetToAlgHom_mk
Documentation

States the theorem baseFixingCosetToAlgHom_mk.

Source context 10 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω] [IsSepClosed Ω]
section CosetsAndEmbeddings
variable (E : IntermediateField K Ω)
omit [IsSepClosed Ω] in
Lean source · statement
theorem baseFixingCosetToAlgHom_mk
    (σ : (closedFixingSubgroup K Ω
      (⊥ : IntermediateField K Ω)).toSubgroup) :
    baseFixingCosetToAlgHom K Ω E (QuotientGroup.mk σ) =
      σ.1.toAlgHom.comp E.val
theorem

baseFixingCosetToAlgHom_surjective

L91 ↗
LocalClassFieldTheory.baseFixingCosetToAlgHom_surjective
Source context 9 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω] [IsSepClosed Ω]
section CosetsAndEmbeddings
variable (E : IntermediateField K Ω)
Lean source · statement
theorem baseFixingCosetToAlgHom_surjective
    [FiniteDimensional K E] [Algebra.IsSeparable K E] :
    Function.Surjective (baseFixingCosetToAlgHom K Ω E)
theorem

baseFixingCosetToAlgHom_injective

L120 ↗
LocalClassFieldTheory.baseFixingCosetToAlgHom_injective
Source context 10 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω] [IsSepClosed Ω]
section CosetsAndEmbeddings
variable (E : IntermediateField K Ω)
omit [IsSepClosed Ω] in
Lean source · statement
theorem baseFixingCosetToAlgHom_injective :
    Function.Injective (baseFixingCosetToAlgHom K Ω E)
def

baseFixingCosetEquivAlgHom

L143 ↗
LocalClassFieldTheory.baseFixingCosetEquivAlgHom
Documentation

Left cosets of the absolute subgroup fixing E are the actual K-embeddings of E into the separably closed ambient field.

Source context 9 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω] [IsSepClosed Ω]
section CosetsAndEmbeddings
variable (E : IntermediateField K Ω)
Lean source · statement
def baseFixingCosetEquivAlgHom
    [FiniteDimensional K E] [Algebra.IsSeparable K E] :
    ((closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω)).toSubgroup ⧸
      extensionSubgroup
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E)) ≃
      (E →ₐ[K] Ω)
instance

baseFixingExtensionQuotient_finite_of_isSeparable

L155 ↗
LocalClassFieldTheory.baseFixingExtensionQuotient_finite_of_isSeparable
Documentation

Provides the instance baseFixingExtensionQuotient_finite_of_isSeparable.

Source context 9 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω] [IsSepClosed Ω]
section CosetsAndEmbeddings
variable (E : IntermediateField K Ω)
Lean source · statement
instance baseFixingExtensionQuotient_finite_of_isSeparable
    [FiniteDimensional K E] [Algebra.IsSeparable K E] :
    Finite
      ((closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω)).toSubgroup ⧸
        extensionSubgroup
          (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
          (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E))
instance

finiteSeparableAlgHomFintype

L168 ↗
LocalClassFieldTheory.finiteSeparableAlgHomFintype
Source context 8 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω] [IsSepClosed Ω]
section NormAsProduct
Lean source · statement
instance finiteSeparableAlgHomFintype
    {k F T : Type} [Field k] [Field F] [Field T]
    [Algebra k F] [Algebra k T]
    [FiniteDimensional k F] [Algebra.IsSeparable k F] :
    Fintype (F →ₐ[k] T)
theorem

relativeCosetAction_intermediateFieldUnit_val_of_isSeparable

L181 ↗
LocalClassFieldTheory.relativeCosetAction_intermediateFieldUnit_val_of_isSeparable
Documentation

The abstract coset action on an E-unit is evaluation under the corresponding actual K-embedding of E.

Source context 11 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω] [IsSepClosed Ω]
section NormAsProduct
noncomputable local instance finiteSeparableAlgHomFintype
    {k F T : Type} [Field k] [Field F] [Field T]
    [Algebra k F] [Algebra k T]
    [FiniteDimensional k F] [Algebra.IsSeparable k F] :
    Fintype (F →ₐ[k] T) :=
  PowerBasis.AlgHom.fintype (Field.powerBasisOfFiniteOfSeparable k F)
variable (E : IntermediateField K Ω)
  [FiniteDimensional K E] [Algebra.IsSeparable K E]
omit [IsSepClosed Ω] [FiniteDimensional K E] [Algebra.IsSeparable K E] in
Lean source · statement
theorem relativeCosetAction_intermediateFieldUnit_val_of_isSeparable
    (x : Eˣ)
    (q : (closedFixingSubgroup K Ω
        (⊥ : IntermediateField K Ω)).toSubgroup ⧸
      extensionSubgroup
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E)) :
    ((Additive.toMul
      (relativeCosetAction (galoisAmbientUnitsRep K Ω)
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E)
        (intermediateFieldUnitsEquivGaloisFixed K Ω E
          (Additive.ofMul x)) q) : Ωˣ) : Ω) =
      baseFixingCosetToAlgHom K Ω E q (x : E)
theorem

relativeNorm_intermediateFieldUnit_val_of_isSeparable

L201 ↗
LocalClassFieldTheory.relativeNorm_intermediateFieldUnit_val_of_isSeparable
Documentation

For every finite separable intermediate field, including a nonnormal one, the abstract class-formation left-coset norm is the ordinary field norm.

Source context 10 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω] [IsSepClosed Ω]
section NormAsProduct
noncomputable local instance finiteSeparableAlgHomFintype
    {k F T : Type} [Field k] [Field F] [Field T]
    [Algebra k F] [Algebra k T]
    [FiniteDimensional k F] [Algebra.IsSeparable k F] :
    Fintype (F →ₐ[k] T) :=
  PowerBasis.AlgHom.fintype (Field.powerBasisOfFiniteOfSeparable k F)
variable (E : IntermediateField K Ω)
  [FiniteDimensional K E] [Algebra.IsSeparable K E]
Lean source · statement
theorem relativeNorm_intermediateFieldUnit_val_of_isSeparable (x : Eˣ) :
    ((Additive.toMul
      ((relativeNorm (galoisAmbientUnitsRep K Ω)
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E)
        (intermediateFieldUnitsEquivGaloisFixed K Ω E
          (Additive.ofMul x))).1 : Additive Ωˣ) : Ωˣ) : Ω) =
      algebraMap K Ω (Algebra.norm K (x : E))
theorem

relativeNorm_intermediateFieldUnit_of_isSeparable

L265 ↗
LocalClassFieldTheory.relativeNorm_intermediateFieldUnit_of_isSeparable
Documentation

Equivariant form of the nonnormal finite-separable norm comparison.

Source context 10 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω] [IsSepClosed Ω]
section NormAsProduct
noncomputable local instance finiteSeparableAlgHomFintype
    {k F T : Type} [Field k] [Field F] [Field T]
    [Algebra k F] [Algebra k T]
    [FiniteDimensional k F] [Algebra.IsSeparable k F] :
    Fintype (F →ₐ[k] T) :=
  PowerBasis.AlgHom.fintype (Field.powerBasisOfFiniteOfSeparable k F)
variable (E : IntermediateField K Ω)
  [FiniteDimensional K E] [Algebra.IsSeparable K E]
Lean source · statement
theorem relativeNorm_intermediateFieldUnit_of_isSeparable (x : Eˣ) :
    relativeNorm (galoisAmbientUnitsRep K Ω)
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E)
        (intermediateFieldUnitsEquivGaloisFixed K Ω E
          (Additive.ofMul x)) =
      baseUnitsEquivGaloisAmbientFixed K Ω
        (Additive.ofMul (normUnits K E x))

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