Module

FiniteAbelianClassFieldContainment.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.FiniteAbelianClassFieldContainment

25 declarations indexed from sourceView source ↗

Module documentation

Containment of finite abelian class fields

For actual finite abelian extensions of a number field, containment is exactly reverse containment of their genuine idèle-class norm ranges.

The proof first realizes an arbitrary extension in the same rational separable closure as the class field selected by a closed finite-index subgroup. The abstract finite-abelian classification then gives a literal inclusion of fixing subgroups, which restricts the chosen ambient embedding to an actual algebra embedding into the selected class field. Applying this construction to the norm range of a second extension yields the intrinsic containment criterion over the original number field.

Imports11

Imported by7

theorem

subgroup_map_toAddSubgroup_mulEquiv_eq

L52 ↗

GlobalClassFieldTheory.GlobalClassFields.subgroup_map_toAddSubgroup_mulEquiv_eq

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem subgroup_map_toAddSubgroup_mulEquiv_eq
    {G G₂ : Type*} [Group G] [Group G₂]
    (S : Subgroup G) (T : Subgroup G₂) (e : G ≃* G₂)
    (hmap : S.map e.toMonoidHom = T) :
    T.toAddSubgroup =
      S.toAddSubgroup.map
        (MulEquiv.toAdditive e).toAddMonoidHom

theorem

subgroup_toAddSubgroup_map_mono_mulEquiv

L62 ↗

GlobalClassFieldTheory.GlobalClassFields.subgroup_toAddSubgroup_map_mono_mulEquiv

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem subgroup_toAddSubgroup_map_mono_mulEquiv
    {G G₂ : Type*} [Group G] [Group G₂]
    (S T : Subgroup G) (e : G ≃* G₂)
    (h : S ≤ T) :
    S.toAddSubgroup.map
        (MulEquiv.toAdditive e).toAddMonoidHom ≤
      T.toAddSubgroup.map
        (MulEquiv.toAdditive e).toAddMonoidHom

def

closedFiniteIndexClassFieldBaseEmbedding

L75 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldBaseEmbedding

Documentation

The distinguished embedding of the original number field into the rational separable closure underlying the class field selected by H.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def closedFiniteIndexClassFieldBaseEmbedding
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    K →ₐ[ℚ] SeparableClosure ℚ

theorem

closedFiniteIndexClassFieldBaseEquiv_coe

L87 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldBaseEquiv_coe

Documentation

The canonical fixed-field equivalence has the distinguished base embedding as its underlying map into the rational separable closure.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem closedFiniteIndexClassFieldBaseEquiv_coe
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (x : K) :
    ((closedFiniteIndexClassFieldBaseEquiv
        (K := K) H hclosed x :
      closedFiniteIndexClassFieldBase
        (K := K) H hclosed) :
      SeparableClosure ℚ) =
      closedFiniteIndexClassFieldBaseEmbedding
        (K := K) H hclosed x

def

finiteAbelianClassFieldContainmentIdeleClassEquiv

L101 ↗

GlobalClassFieldTheory.GlobalClassFields.finiteAbelianClassFieldContainmentIdeleClassEquiv

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def
    finiteAbelianClassFieldContainmentIdeleClassEquiv
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    IdeleClassGroup K ≃*
      IdeleClassGroup
        (closedFiniteIndexClassFieldBase
          (K := K) H hclosed)

def

closedFiniteIndexClassFieldCompatibleEmbedding

L117 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldCompatibleEmbedding

Documentation

An actual finite extension of K, embedded into the rational separable closure compatibly with the selected class-field copy of K.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def closedFiniteIndexClassFieldCompatibleEmbedding
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (E : Type) [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E] :
    E →ₐ[ℚ] SeparableClosure ℚ

theorem

closedFiniteIndexClassFieldCompatibleEmbedding_restrictDomain

L134 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldCompatibleEmbedding_restrictDomain

Documentation

The compatible top embedding restricts to the distinguished embedding of the original base field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    closedFiniteIndexClassFieldCompatibleEmbedding_restrictDomain
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (E : Type) [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E] :
    (closedFiniteIndexClassFieldCompatibleEmbedding
      (K := K) H hclosed E).domRestrict K =
      closedFiniteIndexClassFieldBaseEmbedding
        (K := K) H hclosed

theorem

closedFiniteIndexClassFieldCompatibleEmbedding_algebraMap

L155 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldCompatibleEmbedding_algebraMap

Documentation

Evaluation on the original scalar map agrees with the distinguished base embedding.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem closedFiniteIndexClassFieldCompatibleEmbedding_algebraMap
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (E : Type) [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    (x : K) :
    closedFiniteIndexClassFieldCompatibleEmbedding
        (K := K) H hclosed E
        (algebraMap K E x) =
      closedFiniteIndexClassFieldBaseEmbedding
        (K := K) H hclosed x

theorem

closedFiniteIndexClassFieldCompatibleEmbedding_baseSubgroup

L176 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldCompatibleEmbedding_baseSubgroup

Documentation

The fixing subgroup of the compatible embedded copy of K is the base subgroup used by the selected class field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem closedFiniteIndexClassFieldCompatibleEmbedding_baseSubgroup
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (E : Type) [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E] :
    numberFieldEmbeddedBaseSubgroup K E
        (closedFiniteIndexClassFieldCompatibleEmbedding
          (K := K) H hclosed E) =
      closedFiniteIndexClassFieldBaseSubgroup
        (K := K) H hclosed

def

closedFiniteIndexClassFieldEmbeddedAbelianSubextension

L200 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldEmbeddedAbelianSubextension

Documentation

An actual finite abelian extension, represented inside the same rational absolute Galois group as the class field selected by H.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def
    closedFiniteIndexClassFieldEmbeddedAbelianSubextension
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (E : Type) [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    [IsAbelianGalois K E] :
    FiniteAbelianSubextension
      (closedFiniteIndexClassFieldBaseSubgroup
        (K := K) H hclosed)

theorem

closedFiniteIndexClassFieldEmbeddedAbelianSubextension_field

L222 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldEmbeddedAbelianSubextension_field

Documentation

The top subgroup of the embedded abelian subextension is exactly the fixing subgroup of the compatible embedded copy of E.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    closedFiniteIndexClassFieldEmbeddedAbelianSubextension_field
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (E : Type) [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    [IsAbelianGalois K E] :
    (closedFiniteIndexClassFieldEmbeddedAbelianSubextension
      (K := K) H hclosed E).field =
      numberFieldEmbeddedTopSubgroup K E
        (closedFiniteIndexClassFieldCompatibleEmbedding
          (K := K) H hclosed E)

theorem

ordinaryIdeleClassNormSubgroup_embeddedAbelianSubextension_named

L247 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormSubgroup_embeddedAbelianSubextension_named

Documentation

The abstract norm subgroup of the compatibly embedded extension is the genuine idèle-class norm range of the original extension, transported through the selected base-field equivalence.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    ordinaryIdeleClassNormSubgroup_embeddedAbelianSubextension_named
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (E : Type) [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    [IsAbelianGalois K E] :
    ordinaryIdeleClassNormSubgroup
        (numberFieldTowerFiniteAbstractField K
          (closedFiniteIndexClassFieldNormAmbient
            (K := K) H hclosed))
        (closedFiniteIndexClassFieldEmbeddedAbelianSubextension
          (K := K) H hclosed E) =
      (_root_.ideleClassNorm K E).range.toAddSubgroup.map
        (MulEquiv.toAdditive
          (finiteAbelianClassFieldContainmentIdeleClassEquiv
            (K := K) H hclosed)).toAddMonoidHom

theorem

ordinaryIdeleClassNormSubgroup_embeddedAbelianSubextension

L379 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormSubgroup_embeddedAbelianSubextension

Documentation

The abstract norm subgroup of the compatibly embedded extension is the genuine idèle-class norm range of the original extension, expressed at the concrete selected base-field endpoint.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    ordinaryIdeleClassNormSubgroup_embeddedAbelianSubextension
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (E : Type) [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    [IsAbelianGalois K E] :
    ordinaryIdeleClassNormSubgroup
        (numberFieldTowerFiniteAbstractField K
          (closedFiniteIndexClassFieldNormAmbient
            (K := K) H hclosed))
        (closedFiniteIndexClassFieldEmbeddedAbelianSubextension
          (K := K) H hclosed E) =
      (_root_.ideleClassNorm K E).range.toAddSubgroup.map
        (MulEquiv.toAdditive
          (ideleClassCongr
            (closedFiniteIndexClassFieldBaseEquiv
              (K := K) H hclosed))).toAddMonoidHom

theorem

ordinaryIdeleClassNormSubgroup_closedFiniteIndexClassFieldSubextension_named

L413 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormSubgroup_closedFiniteIndexClassFieldSubextension_named

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    ordinaryIdeleClassNormSubgroup_closedFiniteIndexClassFieldSubextension_named
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    ordinaryIdeleClassNormSubgroup
        (numberFieldTowerFiniteAbstractField K
          (closedFiniteIndexClassFieldNormAmbient
            (K := K) H hclosed))
        (closedFiniteIndexClassFieldSubextension
          (K := K) H hclosed) =
      H.toAddSubgroup.map
        (MulEquiv.toAdditive
          (finiteAbelianClassFieldContainmentIdeleClassEquiv
            (K := K) H hclosed)).toAddMonoidHom

theorem

embeddedAbelianSubextension_le_closedFiniteIndexClassFieldSubextension

L446 ↗

GlobalClassFieldTheory.GlobalClassFields.embeddedAbelianSubextension_le_closedFiniteIndexClassFieldSubextension

Documentation

If H is contained in the genuine norm range of an actual finite abelian extension, its compatible embedded subextension lies below the finite abelian subextension selected by H.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    embeddedAbelianSubextension_le_closedFiniteIndexClassFieldSubextension
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (E : Type) [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    [IsAbelianGalois K E]
    (hH :
      H ≤ (_root_.ideleClassNorm K E).range) :
    closedFiniteIndexClassFieldEmbeddedAbelianSubextension
        (K := K) H hclosed E ≤
      closedFiniteIndexClassFieldSubextension
        (K := K) H hclosed

theorem

finiteAbelianExtensionEmbedding_ambient_algebraMap_eq_baseEquiv

L504 ↗

GlobalClassFieldTheory.GlobalClassFields.finiteAbelianExtensionEmbedding_ambient_algebraMap_eq_baseEquiv

Documentation

The compatible ambient embedding agrees with the selected base equivalence on scalars from the original number field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    finiteAbelianExtensionEmbedding_ambient_algebraMap_eq_baseEquiv
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (E : Type) [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    (x : K) :
    closedFiniteIndexClassFieldCompatibleEmbedding
        (K := K) H hclosed E (algebraMap K E x) =
      ((closedFiniteIndexClassFieldBaseEquiv
          (K := K) H hclosed x :
        closedFiniteIndexClassFieldBase
          (K := K) H hclosed) :
        SeparableClosure ℚ)

theorem

finiteAbelianExtensionEmbedding_codRestrict_mem

L528 ↗

GlobalClassFieldTheory.GlobalClassFields.finiteAbelianExtensionEmbedding_codRestrict_mem

Documentation

A point of a compatibly embedded subextension belongs to the selected class field whenever the corresponding finite abelian subextension lies below the selected one.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    finiteAbelianExtensionEmbedding_codRestrict_mem
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (E : Type) [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    [IsAbelianGalois K E]
    (hcontain :
      closedFiniteIndexClassFieldEmbeddedAbelianSubextension
          (K := K) H hclosed E ≤
        closedFiniteIndexClassFieldSubextension
          (K := K) H hclosed)
    (x : E) :
    closedFiniteIndexClassFieldCompatibleEmbedding
        (K := K) H hclosed E x ∈
      abstractFixedField ℚ (SeparableClosure ℚ)
        (closedFiniteIndexClassFieldSubextension
          (K := K) H hclosed).field

def

finiteAbelianExtensionEmbeddingIntoClosedFiniteIndexClassField

L575 ↗

GlobalClassFieldTheory.GlobalClassFields.finiteAbelianExtensionEmbeddingIntoClosedFiniteIndexClassField

Documentation

Every finite abelian extension whose genuine norm range contains H admits an actual K-algebra embedding into the class field selected by H.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def
    finiteAbelianExtensionEmbeddingIntoClosedFiniteIndexClassField
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (E : Type) [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    [IsAbelianGalois K E]
    (hH :
      H ≤ (_root_.ideleClassNorm K E).range) :
    E →ₐ[K]
      closedFiniteIndexClassField
        (K := K) H hclosed

theorem

finiteAbelianExtension_nonempty_algHom_closedFiniteIndexClassField

L617 ↗

GlobalClassFieldTheory.GlobalClassFields.finiteAbelianExtension_nonempty_algHom_closedFiniteIndexClassField

Documentation

Containment in a selected finite abelian class field, stated as existence of an actual algebra embedding over the original base.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    finiteAbelianExtension_nonempty_algHom_closedFiniteIndexClassField
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (E : Type) [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    [IsAbelianGalois K E]
    (hH :
      H ≤ (_root_.ideleClassNorm K E).range) :
    Nonempty
      (E →ₐ[K]
        closedFiniteIndexClassField
          (K := K) H hclosed)

def

finiteAbelianExtensionEquivClosedFiniteIndexNormClassField

L636 ↗

GlobalClassFieldTheory.GlobalClassFields.finiteAbelianExtensionEquivClosedFiniteIndexNormClassField

Documentation

A finite abelian extension is isomorphic over the original base to the class field selected by its own genuine idèle-class norm range.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def
    finiteAbelianExtensionEquivClosedFiniteIndexNormClassField
    (E : Type) [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    [IsAbelianGalois K E] :
    E ≃ₐ[K]
      closedFiniteIndexClassField
        (K := K)
        (_root_.ideleClassNorm K E).range
        (ideleClassNorm_range_isClosed
          (K := K) (L := E))

theorem

ideleClassNorm_range_le_of_algHom

L684 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_range_le_of_algHom

Documentation

An algebra embedding of finite extensions reverses inclusion of their genuine idèle-class norm ranges.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem ideleClassNorm_range_le_of_algHom
    (L₁ L₂ : Type)
    [Field L₁] [NumberField L₁]
    [Field L₂] [NumberField L₂]
    [Algebra K L₁] [Algebra K L₂]
    [FiniteDimensional K L₁] [FiniteDimensional K L₂]
    [IsAbelianGalois K L₁] [IsAbelianGalois K L₂]
    (f : L₁ →ₐ[K] L₂) :
    (_root_.ideleClassNorm K L₂).range ≤
      (_root_.ideleClassNorm K L₁).range

def

finiteAbelianExtensionEmbeddingOfNormRangeLE

L708 ↗

GlobalClassFieldTheory.GlobalClassFields.finiteAbelianExtensionEmbeddingOfNormRangeLE

Documentation

Reverse inclusion of genuine idèle-class norm ranges constructs an actual algebra embedding of the corresponding finite abelian extensions over the original base field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def finiteAbelianExtensionEmbeddingOfNormRangeLE
    (L₁ L₂ : Type)
    [Field L₁] [NumberField L₁]
    [Field L₂] [NumberField L₂]
    [Algebra K L₁] [Algebra K L₂]
    [FiniteDimensional K L₁] [FiniteDimensional K L₂]
    [IsAbelianGalois K L₁] [IsAbelianGalois K L₂]
    (h :
      (_root_.ideleClassNorm K L₂).range ≤
        (_root_.ideleClassNorm K L₁).range) :
    L₁ →ₐ[K] L₂

theorem

finiteAbelianExtension_nonempty_algHom_of_normRange_le

L743 ↗

GlobalClassFieldTheory.GlobalClassFields.finiteAbelianExtension_nonempty_algHom_of_normRange_le

Documentation

Reverse norm-range inclusion implies actual field containment over the original number field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem finiteAbelianExtension_nonempty_algHom_of_normRange_le
    (L₁ L₂ : Type)
    [Field L₁] [NumberField L₁]
    [Field L₂] [NumberField L₂]
    [Algebra K L₁] [Algebra K L₂]
    [FiniteDimensional K L₁] [FiniteDimensional K L₂]
    [IsAbelianGalois K L₁] [IsAbelianGalois K L₂]
    (h :
      (_root_.ideleClassNorm K L₂).range ≤
        (_root_.ideleClassNorm K L₁).range) :
    Nonempty (L₁ →ₐ[K] L₂)

theorem

nonempty_algHom_iff_ideleClassNorm_range_le

L759 ↗

GlobalClassFieldTheory.GlobalClassFields.nonempty_algHom_iff_ideleClassNorm_range_le

Documentation

Actual containment of finite abelian extensions is equivalent to reverse inclusion of their genuine idèle-class norm ranges.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem nonempty_algHom_iff_ideleClassNorm_range_le
    (L₁ L₂ : Type)
    [Field L₁] [NumberField L₁]
    [Field L₂] [NumberField L₂]
    [Algebra K L₁] [Algebra K L₂]
    [FiniteDimensional K L₁] [FiniteDimensional K L₂]
    [IsAbelianGalois K L₁] [IsAbelianGalois K L₂] :
    Nonempty (L₁ →ₐ[K] L₂) ↔
      (_root_.ideleClassNorm K L₂).range ≤
        (_root_.ideleClassNorm K L₁).range

theorem

nonempty_algEquiv_iff_ideleClassNorm_range_eq

L780 ↗

GlobalClassFieldTheory.GlobalClassFields.nonempty_algEquiv_iff_ideleClassNorm_range_eq

Documentation

Equality of genuine norm ranges characterizes isomorphism of finite abelian extensions over the original number field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open RamificationTheory
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem nonempty_algEquiv_iff_ideleClassNorm_range_eq
    (L₁ L₂ : Type)
    [Field L₁] [NumberField L₁]
    [Field L₂] [NumberField L₂]
    [Algebra K L₁] [Algebra K L₂]
    [FiniteDimensional K L₁] [FiniteDimensional K L₂]
    [IsAbelianGalois K L₁] [IsAbelianGalois K L₂] :
    Nonempty (L₁ ≃ₐ[K] L₂) ↔
      (_root_.ideleClassNorm K L₁).range =
        (_root_.ideleClassNorm K L₂).range

Module documentation

Containment of finite abelian class fields

Declarations