Module

ClassFieldRealization.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ClassFieldRealization

4 declarations indexed from sourceView source ↗

Module documentation

Concrete realization of finite abelian subextensions

A finite abelian subextension in the abstract class-formation lattice is represented by two nested closed subgroups of an ambient Galois group. Its upper relative fixed field is an actual finite extension of the lower fixed field. The quotient-to-Galois-group equivalence transports the commutativity carried by the abstract package, so this actual extension is abelian Galois.

Imports3

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.FiniteAbelianSubextension
Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FiniteAbstractFixedField
Mathlib.FieldTheory.Galois.Abelian

Imported by6

theorem

algEquiv_commutes_algebraMap_of_base_equiv

L35 ↗

GlobalClassFieldTheory.GlobalClassFields.algEquiv_commutes_algebraMap_of_base_equiv

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open scoped IsMulCommutative
universe u v w

Lean source · statement

theorem algEquiv_commutes_algebraMap_of_base_equiv
    {K : Type u} {K' : Type v} {L : Type w}
    [Field K] [Field K'] [Field L]
    [Algebra K L] [Algebra K' L]
    (e : K ≃+* K')
    (h : ∀ x : K,
      algebraMap K L x =
        algebraMap K' L (e x))
    (f : L ≃ₐ[K] L)
    (x : K') :
    f (algebraMap K' L x) =
      algebraMap K' L x

theorem

of_base_equiv

L69 ↗

GlobalClassFieldTheory.GlobalClassFields.IsAbelianGalois.of_base_equiv

Documentation

Abelian Galois structure transports across an equivalence of base fields when the two scalar maps into the common top field commute with that equivalence. The Galois part is supplied separately, typically by Mathlib's IsGalois.of_equiv_equiv; this theorem transports commutativity of the actual automorphism group.

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open scoped IsMulCommutative
universe u v w

Lean source · statement

theorem IsAbelianGalois.of_base_equiv
    {K : Type u} {K' : Type v} {L : Type w}
    [Field K] [Field K'] [Field L]
    [Algebra K L] [Algebra K' L]
    [IsGalois K L] [IsAbelianGalois K' L]
    (e : K ≃+* K')
    (h : ∀ x : K,
      algebraMap K L x =
        algebraMap K' L (e x)) :
    IsAbelianGalois K L

instance

finiteAbelianSubextensionAbstractRelativeFixedFieldFiniteDimensional

L98 ↗

GlobalClassFieldTheory.GlobalClassFields.finiteAbelianSubextensionAbstractRelativeFixedFieldFiniteDimensional

Documentation

The relative fixed field represented by a finite abelian subextension is finite-dimensional over the fixed field represented by its base subgroup.

Source context 9 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open scoped IsMulCommutative
universe u v w
variable
    {k Ω : Type}
    [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
    {K : ClosedSubgroup (Gal(Ω/k))}

Lean source · statement

instance
    finiteAbelianSubextensionAbstractRelativeFixedFieldFiniteDimensional
    [hKfinite : Finite
      ((baseField Gal(Ω/k)).toSubgroup ⧸
        extensionSubgroup
          (baseField Gal(Ω/k)) K (le_baseField K))]
    (L : FiniteAbelianSubextension K) :
    FiniteDimensional
      (abstractFixedField k Ω K)
      (abstractRelativeFixedField k Ω L.below)

instance

finiteAbelianSubextensionAbstractRelativeFixedFieldIsAbelianGalois

L113 ↗

GlobalClassFieldTheory.GlobalClassFields.finiteAbelianSubextensionAbstractRelativeFixedFieldIsAbelianGalois

Documentation

The actual relative fixed field represented by a finite abelian subextension is an abelian Galois extension of the actual base fixed field.

Source context 9 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open scoped IsMulCommutative
universe u v w
variable
    {k Ω : Type}
    [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
    {K : ClosedSubgroup (Gal(Ω/k))}

Lean source · statement

instance
    finiteAbelianSubextensionAbstractRelativeFixedFieldIsAbelianGalois
    (L : FiniteAbelianSubextension K) :
    IsAbelianGalois
      (abstractFixedField k Ω K)
      (abstractRelativeFixedField k Ω L.below)

Module documentation

Concrete realization of finite abelian subextensions

Declarations

algEquiv_commutes_algebraMap_of_base_equiv

of_base_equiv

finiteAbelianSubextensionAbstractRelativeFixedFieldFiniteDimensional

finiteAbelianSubextensionAbstractRelativeFixedFieldIsAbelianGalois