NYLL
Module

FixedFieldRelativeNorm.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FixedFieldRelativeNorm
8 declarations indexed from sourceView source ↗

Module documentation

Relative norms on actual fixed fields

This file identifies the class-formation relative norm on ambient fixed units with the ordinary field norm between two concrete fixed fields. The intermediate extension need not be normal: relative left cosets are identified with field embeddings into the common separably closed ambient field, and both norms are then the same product of conjugates.

Imports4
Imported by4

Declarations

instance

finiteSeparableAlgHomFintypeRelative

L36 ↗
LocalClassFieldTheory.finiteSeparableAlgHomFintypeRelative
Source context 6 commands

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

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

abstractFixedFieldCosetToAlgHom

L45 ↗
LocalClassFieldTheory.abstractFixedFieldCosetToAlgHom
Documentation

A left coset of the abstract fixing subgroup restricts to an embedding of the upper concrete fixed field into the common ambient field.

Source context 7 commands

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

noncomputable section
open scoped BigOperators
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω]
  [IsGalois k Ω] [IsSepClosed Ω]
noncomputable local instance finiteSeparableAlgHomFintypeRelative
    {F E T : Type} [Field F] [Field E] [Field T]
    [Algebra F E] [Algebra F T]
    [FiniteDimensional F E] [Algebra.IsSeparable F E] :
    Fintype (E →ₐ[F] T) :=
  PowerBasis.AlgHom.fintype (Field.powerBasisOfFiniteOfSeparable F E)
Lean source · statement
def abstractFixedFieldCosetToAlgHom
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup) :
    (K.toSubgroup ⧸ extensionSubgroup K L hLK) →
      (abstractRelativeFixedField k Ω hLK →ₐ[
        abstractFixedField k Ω K] Ω)
theorem

abstractFixedFieldCosetToAlgHom_mk

L81 ↗
LocalClassFieldTheory.abstractFixedFieldCosetToAlgHom_mk
Documentation

States the theorem abstractFixedFieldCosetToAlgHom_mk.

Source context 8 commands

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

noncomputable section
open scoped BigOperators
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω]
  [IsGalois k Ω] [IsSepClosed Ω]
noncomputable local instance finiteSeparableAlgHomFintypeRelative
    {F E T : Type} [Field F] [Field E] [Field T]
    [Algebra F E] [Algebra F T]
    [FiniteDimensional F E] [Algebra.IsSeparable F E] :
    Fintype (E →ₐ[F] T) :=
  PowerBasis.AlgHom.fintype (Field.powerBasisOfFiniteOfSeparable F E)
omit [IsSepClosed Ω] in
Lean source · statement
theorem abstractFixedFieldCosetToAlgHom_mk
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup) (σ : K.toSubgroup) :
    abstractFixedFieldCosetToAlgHom k Ω K L hLK
        (QuotientGroup.mk σ) =
      (abstractSubgroupEquivGaloisGroup k Ω K σ).toAlgHom.comp
        (abstractRelativeFixedField k Ω hLK).val
theorem

abstractFixedFieldCosetToAlgHom_surjective

L90 ↗
LocalClassFieldTheory.abstractFixedFieldCosetToAlgHom_surjective
Source context 7 commands

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

noncomputable section
open scoped BigOperators
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω]
  [IsGalois k Ω] [IsSepClosed Ω]
noncomputable local instance finiteSeparableAlgHomFintypeRelative
    {F E T : Type} [Field F] [Field E] [Field T]
    [Algebra F E] [Algebra F T]
    [FiniteDimensional F E] [Algebra.IsSeparable F E] :
    Fintype (E →ₐ[F] T) :=
  PowerBasis.AlgHom.fintype (Field.powerBasisOfFiniteOfSeparable F E)
Lean source · statement
theorem abstractFixedFieldCosetToAlgHom_surjective
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [FiniteDimensional (abstractFixedField k Ω K)
      (abstractRelativeFixedField k Ω hLK)] :
    Function.Surjective
      (abstractFixedFieldCosetToAlgHom k Ω K L hLK)
theorem

abstractFixedFieldCosetToAlgHom_injective

L129 ↗
LocalClassFieldTheory.abstractFixedFieldCosetToAlgHom_injective
Source context 8 commands

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

noncomputable section
open scoped BigOperators
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω]
  [IsGalois k Ω] [IsSepClosed Ω]
noncomputable local instance finiteSeparableAlgHomFintypeRelative
    {F E T : Type} [Field F] [Field E] [Field T]
    [Algebra F E] [Algebra F T]
    [FiniteDimensional F E] [Algebra.IsSeparable F E] :
    Fintype (E →ₐ[F] T) :=
  PowerBasis.AlgHom.fintype (Field.powerBasisOfFiniteOfSeparable F E)
omit [IsSepClosed Ω] in
Lean source · statement
theorem abstractFixedFieldCosetToAlgHom_injective
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup) :
    Function.Injective
      (abstractFixedFieldCosetToAlgHom k Ω K L hLK)
def

abstractFixedFieldCosetEquivAlgHom

L159 ↗
LocalClassFieldTheory.abstractFixedFieldCosetEquivAlgHom
Documentation

Abstract relative left cosets are precisely the embeddings of the upper concrete fixed field into the ambient separably closed field.

Source context 7 commands

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

noncomputable section
open scoped BigOperators
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω]
  [IsGalois k Ω] [IsSepClosed Ω]
noncomputable local instance finiteSeparableAlgHomFintypeRelative
    {F E T : Type} [Field F] [Field E] [Field T]
    [Algebra F E] [Algebra F T]
    [FiniteDimensional F E] [Algebra.IsSeparable F E] :
    Fintype (E →ₐ[F] T) :=
  PowerBasis.AlgHom.fintype (Field.powerBasisOfFiniteOfSeparable F E)
Lean source · statement
def abstractFixedFieldCosetEquivAlgHom
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [FiniteDimensional (abstractFixedField k Ω K)
      (abstractRelativeFixedField k Ω hLK)] :
    (K.toSubgroup ⧸ extensionSubgroup K L hLK) ≃
      (abstractRelativeFixedField k Ω hLK →ₐ[
        abstractFixedField k Ω K] Ω)
theorem

relativeCosetAction_abstractFixedFieldUnit_val

L173 ↗
LocalClassFieldTheory.relativeCosetAction_abstractFixedFieldUnit_val
Documentation

States the theorem relativeCosetAction_abstractFixedFieldUnit_val.

Source context 8 commands

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

noncomputable section
open scoped BigOperators
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω]
  [IsGalois k Ω] [IsSepClosed Ω]
noncomputable local instance finiteSeparableAlgHomFintypeRelative
    {F E T : Type} [Field F] [Field E] [Field T]
    [Algebra F E] [Algebra F T]
    [FiniteDimensional F E] [Algebra.IsSeparable F E] :
    Fintype (E →ₐ[F] T) :=
  PowerBasis.AlgHom.fintype (Field.powerBasisOfFiniteOfSeparable F E)
omit [IsSepClosed Ω] in
Lean source · statement
theorem relativeCosetAction_abstractFixedFieldUnit_val
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (x : (abstractRelativeFixedField k Ω hLK)ˣ)
    (q : K.toSubgroup ⧸ extensionSubgroup K L hLK) :
    ((Additive.toMul
      (relativeCosetAction (galoisAmbientUnitsRep k Ω)
        K L hLK
        (abstractRelativeFixedFieldUnitsEquivGaloisFixed
          k Ω K L hLK (Additive.ofMul x)) q) : Ωˣ) : Ω) =
      abstractFixedFieldCosetToAlgHom k Ω K L hLK q
        (x : abstractRelativeFixedField k Ω hLK)
theorem

relativeNorm_abstractFixedFieldUnit_eq_normUnits

L192 ↗
LocalClassFieldTheory.relativeNorm_abstractFixedFieldUnit_eq_normUnits
Documentation

The class-formation relative norm on fixed coefficients is the ordinary field norm between the two concrete fixed fields, without a normality assumption on the intermediate extension.

Source context 7 commands

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

noncomputable section
open scoped BigOperators
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω]
  [IsGalois k Ω] [IsSepClosed Ω]
noncomputable local instance finiteSeparableAlgHomFintypeRelative
    {F E T : Type} [Field F] [Field E] [Field T]
    [Algebra F E] [Algebra F T]
    [FiniteDimensional F E] [Algebra.IsSeparable F E] :
    Fintype (E →ₐ[F] T) :=
  PowerBasis.AlgHom.fintype (Field.powerBasisOfFiniteOfSeparable F E)
Lean source · statement
theorem relativeNorm_abstractFixedFieldUnit_eq_normUnits
    (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))]
    (x : (abstractRelativeFixedField k Ω hLK)ˣ) :
    relativeNorm (galoisAmbientUnitsRep k Ω) K L hLK
        (abstractRelativeFixedFieldUnitsEquivGaloisFixed
          k Ω K L hLK (Additive.ofMul x)) =
      abstractFixedFieldUnitsEquivGaloisFixed k Ω K
        (Additive.ofMul
          (normUnits (abstractFixedField k Ω K)
            (abstractRelativeFixedField k Ω hLK) x))

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