NYLL
Module

HilbertClassFieldMaximalSubextension.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldMaximalSubextension
52 declarations indexed from sourceView source ↗

Module documentation

The maximal finite-unramified abelian subextension

The selected big Hilbert class field is characterized here in actual field order. Its abstract norm subgroup in the rational absolute idele-class formation is identified exactly with the intrinsic big-Hilbert subgroup of its fixed-field base. Every finite abelian subextension whose actual fixed-field extension is unramified at all finite places has a larger norm subgroup, hence lies below the selected big Hilbert class field by the order-reversing finite classification.

Maximality over the original number field

The preceding order statement lives over the fixed-field copy of the base used by the rational absolute class formation. We now embed an arbitrary actual finite abelian extension E / K compatibly with that copy, apply the fixed-field maximality theorem there, and restrict its ambient embedding to the selected big Hilbert class field.

Imports8
Imported by2

Declarations

structure

BigHilbertTransportedAddSubgroupData

L40 ↗
GlobalClassFieldTheory.GlobalClassFields.BigHilbertTransportedAddSubgroupData
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · full declaration
structure BigHilbertTransportedAddSubgroupData
    {A B : Type} [AddGroup A] [AddGroup B]
    (e : A ≃+ B) (H : AddSubgroup A) where
  subgroup : AddSubgroup B
  map_symm : subgroup.map e.symm.toAddMonoidHom = H
  mem_iff (x : B) : x ∈ subgroup ↔ e.symm x ∈ H
def

bigHilbertTransportedAddSubgroupData

L47 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertTransportedAddSubgroupData
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · full declaration
def bigHilbertTransportedAddSubgroupData
    {A B : Type} [AddGroup A] [AddGroup B]
    (e : A ≃+ B) (H : AddSubgroup A) :
    BigHilbertTransportedAddSubgroupData e H where
  subgroup := H.map e.toAddMonoidHom
  map_symm :=
    (AddSubgroup.map_symm_eq_iff_map_eq
      (K := H) (H := H.map e.toAddMonoidHom) (e := e)).2 rfl
  mem_iff := by
    intro x
    constructor
    · rintro ⟨y, hy, rfl⟩
      simpa using hy
    · intro hx
      exact ⟨e.symm x, hx, e.apply_symm_apply x⟩
theorem

bigHilbertAddSubgroup_eq_of_map_symm_eq

L63 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertAddSubgroup_eq_of_map_symm_eq
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem bigHilbertAddSubgroup_eq_of_map_symm_eq
    {A B : Type} [AddGroup A] [AddGroup B]
    (e : A ≃+ B) (H J : AddSubgroup B)
    (h : H.map e.symm.toAddMonoidHom =
      J.map e.symm.toAddMonoidHom) :
    H = J
def

bigHilbertNormSubgroupInRationalClassFormation

L73 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertNormSubgroupInRationalClassFormation
Documentation

The intrinsic big-Hilbert norm subgroup of an actual rational fixed field, transported into the rational absolute idele-class formation.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
def bigHilbertNormSubgroupInRationalClassFormation
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    AddSubgroup
      (ambientFixedAddSubgroup
        rationalIdeleClassRepresentation K.field)
def

finiteAbstractBigHilbertIntrinsicNormSubgroup

L85 ↗
GlobalClassFieldTheory.GlobalClassFields.finiteAbstractBigHilbertIntrinsicNormSubgroup
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
def finiteAbstractBigHilbertIntrinsicNormSubgroup
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    AddSubgroup
      (Additive
        (IdeleClassGroup
          (abstractFixedField ℚ (SeparableClosure ℚ) K.field)))
def

finiteAbstractBigHilbertTransportData

L95 ↗
GlobalClassFieldTheory.GlobalClassFields.finiteAbstractBigHilbertTransportData
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
def finiteAbstractBigHilbertTransportData
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    BigHilbertTransportedAddSubgroupData
      (rationalAbstractFixedFieldIdeleClassEquivFixed K.field)
      (finiteAbstractBigHilbertIntrinsicNormSubgroup K)
theorem

bigHilbertNormSubgroupInRationalClassFormation_mem_iff

L105 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertNormSubgroupInRationalClassFormation_mem_iff
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem bigHilbertNormSubgroupInRationalClassFormation_mem_iff
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (x : ambientFixedAddSubgroup rationalIdeleClassRepresentation K.field) :
    x ∈ bigHilbertNormSubgroupInRationalClassFormation K ↔
      (rationalAbstractFixedFieldIdeleClassEquivFixed K.field).symm x ∈
        finiteAbstractBigHilbertIntrinsicNormSubgroup K
def

bigHilbertClassFieldMaximalIdeleClassEquiv

L116 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldMaximalIdeleClassEquiv
Documentation

The fixed-field idele-class equivalence at the selected big-Hilbert base, named once so later subgroup comparisons do not reconstruct it.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
def bigHilbertClassFieldMaximalIdeleClassEquiv
    (K : Type) [Field K] [NumberField K] :
    Additive (IdeleClassGroup (bigHilbertClassFieldBase K)) ≃+
      ambientFixedAddSubgroup rationalIdeleClassRepresentation
        (bigHilbertClassFieldBaseSubgroup K)
def

bigHilbertClassFieldMaximalIntrinsicNormSubgroup

L126 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldMaximalIntrinsicNormSubgroup
Documentation

The intrinsic ordinary norm subgroup at the selected base, with its additive carrier fixed in the declaration type.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
def bigHilbertClassFieldMaximalIntrinsicNormSubgroup
    (K : Type) [Field K] [NumberField K] :
    AddSubgroup (Additive (IdeleClassGroup (bigHilbertClassFieldBase K)))
def

bigHilbertClassFieldMaximalActualNormEndpoint

L134 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldMaximalActualNormEndpoint
Documentation

The selected abstract norm subgroup, with its ambient additive carrier fixed once in the declaration type.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
def bigHilbertClassFieldMaximalActualNormEndpoint
    (K : Type) [Field K] [NumberField K] :
    AddSubgroup
      (ambientFixedAddSubgroup rationalIdeleClassRepresentation
        (bigHilbertClassFieldBaseSubgroup K))
def

bigHilbertClassFieldMaximalTransportData

L142 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldMaximalTransportData
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
def bigHilbertClassFieldMaximalTransportData
    (K : Type) [Field K] [NumberField K] :
    BigHilbertTransportedAddSubgroupData
      (bigHilbertClassFieldMaximalIdeleClassEquiv K)
      (bigHilbertClassFieldMaximalIntrinsicNormSubgroup K)
def

bigHilbertClassFieldMaximalNormEndpoint

L152 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldMaximalNormEndpoint
Documentation

A short typed name for the transported intrinsic subgroup used below.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
def bigHilbertClassFieldMaximalNormEndpoint
    (K : Type) [Field K] [NumberField K] :
    AddSubgroup
      (ambientFixedAddSubgroup rationalIdeleClassRepresentation
        (bigHilbertClassFieldBaseSubgroup K))
theorem

bigHilbertClassFieldMaximalNormEndpoint_map_symm

L159 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldMaximalNormEndpoint_map_symm
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem bigHilbertClassFieldMaximalNormEndpoint_map_symm
    (K : Type) [Field K] [NumberField K] :
    (bigHilbertClassFieldMaximalNormEndpoint K).map
        (bigHilbertClassFieldMaximalIdeleClassEquiv K).symm.toAddMonoidHom =
      bigHilbertClassFieldMaximalIntrinsicNormSubgroup K
theorem

bigHilbertClassFieldMaximalNormEndpoint_mem_iff

L166 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldMaximalNormEndpoint_mem_iff
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem bigHilbertClassFieldMaximalNormEndpoint_mem_iff
    (K : Type) [Field K] [NumberField K]
    (x : ambientFixedAddSubgroup rationalIdeleClassRepresentation
      (bigHilbertClassFieldBaseSubgroup K)) :
    x ∈ bigHilbertClassFieldMaximalNormEndpoint K ↔
      (bigHilbertClassFieldMaximalIdeleClassEquiv K).symm x ∈
        bigHilbertClassFieldMaximalIntrinsicNormSubgroup K
theorem

bigHilbertClassFieldMaximalNormEndpoint_eq_public

L175 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldMaximalNormEndpoint_eq_public
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem bigHilbertClassFieldMaximalNormEndpoint_eq_public
    (K : Type) [Field K] [NumberField K] :
    bigHilbertClassFieldMaximalNormEndpoint K =
      bigHilbertNormSubgroupInRationalClassFormation
        (numberFieldTowerFiniteAbstractField K
          (bigHilbertClassFieldNormAmbient K))
theorem

bigHilbertClassFieldMaximalNormSubgroup_map_symm

L185 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldMaximalNormSubgroup_map_symm
Documentation

Mapping the selected abstract norm subgroup back to the ordinary idele-class group gives the named intrinsic subgroup.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem bigHilbertClassFieldMaximalNormSubgroup_map_symm
    (K : Type) [Field K] [NumberField K] :
    (bigHilbertClassFieldMaximalActualNormEndpoint K).map
      (bigHilbertClassFieldMaximalIdeleClassEquiv K).symm.toAddMonoidHom =
        bigHilbertClassFieldMaximalIntrinsicNormSubgroup K
theorem

bigHilbertClassFieldMaximalActualNormEndpoint_mem_iff

L231 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldMaximalActualNormEndpoint_mem_iff
Documentation

Membership in the selected abstract norm subgroup is detected after applying the named inverse fixed-field equivalence.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem bigHilbertClassFieldMaximalActualNormEndpoint_mem_iff
    (K : Type) [Field K] [NumberField K] :
    ∀ x : ambientFixedAddSubgroup rationalIdeleClassRepresentation
        (bigHilbertClassFieldBaseSubgroup K),
      x ∈ bigHilbertClassFieldMaximalActualNormEndpoint K ↔
        (bigHilbertClassFieldMaximalIdeleClassEquiv K).symm x ∈
          bigHilbertClassFieldMaximalIntrinsicNormSubgroup K
theorem

bigHilbertClassFieldMaximalNormSubgroup_eq_endpoint

L254 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldMaximalNormSubgroup_eq_endpoint
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem bigHilbertClassFieldMaximalNormSubgroup_eq_endpoint
    (K : Type) [Field K] [NumberField K] :
    bigHilbertClassFieldMaximalActualNormEndpoint K =
      bigHilbertClassFieldMaximalNormEndpoint K
theorem

bigHilbertClassFieldSubextension_normSubgroup

L268 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldSubextension_normSubgroup
Documentation

The selected big Hilbert class-field subextension realizes exactly the intrinsic big-Hilbert norm subgroup in the rational absolute class formation.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem bigHilbertClassFieldSubextension_normSubgroup
    (K : Type) [Field K] [NumberField K] :
    (bigHilbertClassFieldSubextension K).normSubgroup
        rationalIdeleClassRepresentation =
      bigHilbertNormSubgroupInRationalClassFormation
        (numberFieldTowerFiniteAbstractField K
          (bigHilbertClassFieldNormAmbient K))
instance

maximalSubextensionBaseQuotientFinite

L295 ↗
GlobalClassFieldTheory.GlobalClassFields.maximalSubextensionBaseQuotientFinite
Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section GeneralFixedFieldContainment
variable
    (K₀ : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (P₀ : FiniteAbelianSubextension K₀.field)
Lean source · statement
instance maximalSubextensionBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K₀.field (le_baseField K₀.field))
instance

maximalSubextensionRelativeQuotientFinite

L305 ↗
GlobalClassFieldTheory.GlobalClassFields.maximalSubextensionRelativeQuotientFinite
Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section GeneralFixedFieldContainment
variable
    (K₀ : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (P₀ : FiniteAbelianSubextension K₀.field)
local instance maximalSubextensionBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K₀.field (le_baseField K₀.field)) :=
  K₀.finite
Lean source · statement
instance maximalSubextensionRelativeQuotientFinite :
    Finite
      (K₀.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K₀.field P₀.field P₀.below)
instance

maximalSubextensionBaseFiniteDimensional

L312 ↗
GlobalClassFieldTheory.GlobalClassFields.maximalSubextensionBaseFiniteDimensional
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 KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section GeneralFixedFieldContainment
variable
    (K₀ : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (P₀ : FiniteAbelianSubextension K₀.field)
local instance maximalSubextensionBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K₀.field (le_baseField K₀.field)) :=
  K₀.finite
local instance maximalSubextensionRelativeQuotientFinite :
    Finite
      (K₀.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K₀.field P₀.field P₀.below) :=
  P₀.finite
Lean source · statement
instance maximalSubextensionBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
instance

maximalSubextensionRelativeFiniteDimensional

L318 ↗
GlobalClassFieldTheory.GlobalClassFields.maximalSubextensionRelativeFiniteDimensional
Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section GeneralFixedFieldContainment
variable
    (K₀ : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (P₀ : FiniteAbelianSubextension K₀.field)
local instance maximalSubextensionBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K₀.field (le_baseField K₀.field)) :=
  K₀.finite
local instance maximalSubextensionRelativeQuotientFinite :
    Finite
      (K₀.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K₀.field P₀.field P₀.below) :=
  P₀.finite
noncomputable local instance maximalSubextensionBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K₀.field K₀.finite
Lean source · statement
instance maximalSubextensionRelativeFiniteDimensional :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below)
instance

maximalSubextensionRelativeScalarTower

L327 ↗
GlobalClassFieldTheory.GlobalClassFields.maximalSubextensionRelativeScalarTower
Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section GeneralFixedFieldContainment
variable
    (K₀ : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (P₀ : FiniteAbelianSubextension K₀.field)
local instance maximalSubextensionBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K₀.field (le_baseField K₀.field)) :=
  K₀.finite
local instance maximalSubextensionRelativeQuotientFinite :
    Finite
      (K₀.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K₀.field P₀.field P₀.below) :=
  P₀.finite
noncomputable local instance maximalSubextensionBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K₀.field K₀.finite
noncomputable local instance maximalSubextensionRelativeFiniteDimensional :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K₀.field P₀.field P₀.below K₀.finite P₀.finite
Lean source · statement
instance maximalSubextensionRelativeScalarTower :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below)
instance

maximalSubextensionTopFiniteDimensional

L334 ↗
GlobalClassFieldTheory.GlobalClassFields.maximalSubextensionTopFiniteDimensional
Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section GeneralFixedFieldContainment
variable
    (K₀ : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (P₀ : FiniteAbelianSubextension K₀.field)
local instance maximalSubextensionBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K₀.field (le_baseField K₀.field)) :=
  K₀.finite
local instance maximalSubextensionRelativeQuotientFinite :
    Finite
      (K₀.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K₀.field P₀.field P₀.below) :=
  P₀.finite
noncomputable local instance maximalSubextensionBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K₀.field K₀.finite
noncomputable local instance maximalSubextensionRelativeFiniteDimensional :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K₀.field P₀.field P₀.below K₀.finite P₀.finite
local instance maximalSubextensionRelativeScalarTower :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
Lean source · statement
instance maximalSubextensionTopFiniteDimensional :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below)
instance

maximalSubextensionBaseNumberField

L343 ↗
GlobalClassFieldTheory.GlobalClassFields.maximalSubextensionBaseNumberField
Source context 14 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section GeneralFixedFieldContainment
variable
    (K₀ : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (P₀ : FiniteAbelianSubextension K₀.field)
local instance maximalSubextensionBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K₀.field (le_baseField K₀.field)) :=
  K₀.finite
local instance maximalSubextensionRelativeQuotientFinite :
    Finite
      (K₀.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K₀.field P₀.field P₀.below) :=
  P₀.finite
noncomputable local instance maximalSubextensionBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K₀.field K₀.finite
noncomputable local instance maximalSubextensionRelativeFiniteDimensional :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K₀.field P₀.field P₀.below K₀.finite P₀.finite
local instance maximalSubextensionRelativeScalarTower :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance maximalSubextensionTopFiniteDimensional :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P₀.below)
Lean source · statement
instance maximalSubextensionBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
instance

maximalSubextensionTopNumberField

L349 ↗
GlobalClassFieldTheory.GlobalClassFields.maximalSubextensionTopNumberField
Source context 15 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section GeneralFixedFieldContainment
variable
    (K₀ : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (P₀ : FiniteAbelianSubextension K₀.field)
local instance maximalSubextensionBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K₀.field (le_baseField K₀.field)) :=
  K₀.finite
local instance maximalSubextensionRelativeQuotientFinite :
    Finite
      (K₀.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K₀.field P₀.field P₀.below) :=
  P₀.finite
noncomputable local instance maximalSubextensionBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K₀.field K₀.finite
noncomputable local instance maximalSubextensionRelativeFiniteDimensional :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K₀.field P₀.field P₀.below K₀.finite P₀.finite
local instance maximalSubextensionRelativeScalarTower :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance maximalSubextensionTopFiniteDimensional :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P₀.below)
noncomputable local instance maximalSubextensionBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
Lean source · statement
instance maximalSubextensionTopNumberField :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below)
instance

maximalSubextensionRelativeIsGalois

L357 ↗
GlobalClassFieldTheory.GlobalClassFields.maximalSubextensionRelativeIsGalois
Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section GeneralFixedFieldContainment
variable
    (K₀ : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (P₀ : FiniteAbelianSubextension K₀.field)
local instance maximalSubextensionBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K₀.field (le_baseField K₀.field)) :=
  K₀.finite
local instance maximalSubextensionRelativeQuotientFinite :
    Finite
      (K₀.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K₀.field P₀.field P₀.below) :=
  P₀.finite
noncomputable local instance maximalSubextensionBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K₀.field K₀.finite
noncomputable local instance maximalSubextensionRelativeFiniteDimensional :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K₀.field P₀.field P₀.below K₀.finite P₀.finite
local instance maximalSubextensionRelativeScalarTower :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance maximalSubextensionTopFiniteDimensional :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P₀.below)
noncomputable local instance maximalSubextensionBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
noncomputable local instance maximalSubextensionTopNumberField :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P₀.below)
Lean source · statement
instance maximalSubextensionRelativeIsGalois :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below)
def

bigHilbertNormSubgroupContainedInRationalClassFormation

L368 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertNormSubgroupContainedInRationalClassFormation
Documentation

The intrinsic big-Hilbert norm subgroup is contained in the norm subgroup of the specified finite abelian subextension.

Source context 17 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section GeneralFixedFieldContainment
variable
    (K₀ : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (P₀ : FiniteAbelianSubextension K₀.field)
local instance maximalSubextensionBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K₀.field (le_baseField K₀.field)) :=
  K₀.finite
local instance maximalSubextensionRelativeQuotientFinite :
    Finite
      (K₀.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K₀.field P₀.field P₀.below) :=
  P₀.finite
noncomputable local instance maximalSubextensionBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K₀.field K₀.finite
noncomputable local instance maximalSubextensionRelativeFiniteDimensional :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K₀.field P₀.field P₀.below K₀.finite P₀.finite
local instance maximalSubextensionRelativeScalarTower :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance maximalSubextensionTopFiniteDimensional :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P₀.below)
noncomputable local instance maximalSubextensionBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
noncomputable local instance maximalSubextensionTopNumberField :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P₀.below)
noncomputable local instance maximalSubextensionRelativeIsGalois :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K₀.field P₀.field P₀.below P₀.normal
Lean source · statement
def bigHilbertNormSubgroupContainedInRationalClassFormation
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (P : FiniteAbelianSubextension K.field) : Prop
def

finiteAbelianSubextensionIsUnramifiedAtFinitePlaces

L377 ↗
GlobalClassFieldTheory.GlobalClassFields.finiteAbelianSubextensionIsUnramifiedAtFinitePlaces
Documentation

The actual fixed-field extension represented by a finite abelian subextension is unramified at every finite place.

Source context 17 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section GeneralFixedFieldContainment
variable
    (K₀ : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (P₀ : FiniteAbelianSubextension K₀.field)
local instance maximalSubextensionBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K₀.field (le_baseField K₀.field)) :=
  K₀.finite
local instance maximalSubextensionRelativeQuotientFinite :
    Finite
      (K₀.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K₀.field P₀.field P₀.below) :=
  P₀.finite
noncomputable local instance maximalSubextensionBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K₀.field K₀.finite
noncomputable local instance maximalSubextensionRelativeFiniteDimensional :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K₀.field P₀.field P₀.below K₀.finite P₀.finite
local instance maximalSubextensionRelativeScalarTower :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance maximalSubextensionTopFiniteDimensional :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P₀.below)
noncomputable local instance maximalSubextensionBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
noncomputable local instance maximalSubextensionTopNumberField :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P₀.below)
noncomputable local instance maximalSubextensionRelativeIsGalois :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K₀.field P₀.field P₀.below P₀.normal
Lean source · statement
def finiteAbelianSubextensionIsUnramifiedAtFinitePlaces
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (P : FiniteAbelianSubextension K.field) : Prop
theorem

bigHilbertNormSubgroupInRationalClassFormation_le_normSubgroup_of_unramifiedAtFinitePlaces

L389 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertNormSubgroupInRationalClassFormation_le_normSubgroup_of_unramifiedAtFinitePlaces
Documentation

Finite-prime unramifiedness of an actual finite abelian fixed-field extension forces its abstract norm subgroup to contain the intrinsic big-Hilbert subgroup.

Source context 17 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section GeneralFixedFieldContainment
variable
    (K₀ : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (P₀ : FiniteAbelianSubextension K₀.field)
local instance maximalSubextensionBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K₀.field (le_baseField K₀.field)) :=
  K₀.finite
local instance maximalSubextensionRelativeQuotientFinite :
    Finite
      (K₀.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K₀.field P₀.field P₀.below) :=
  P₀.finite
noncomputable local instance maximalSubextensionBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K₀.field K₀.finite
noncomputable local instance maximalSubextensionRelativeFiniteDimensional :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K₀.field P₀.field P₀.below K₀.finite P₀.finite
local instance maximalSubextensionRelativeScalarTower :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance maximalSubextensionTopFiniteDimensional :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P₀.below)
noncomputable local instance maximalSubextensionBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
noncomputable local instance maximalSubextensionTopNumberField :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P₀.below)
noncomputable local instance maximalSubextensionRelativeIsGalois :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K₀.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P₀.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K₀.field P₀.field P₀.below P₀.normal
Lean source · statement
theorem
    bigHilbertNormSubgroupInRationalClassFormation_le_normSubgroup_of_unramifiedAtFinitePlaces
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (P : FiniteAbelianSubextension K.field) :
    finiteAbelianSubextensionIsUnramifiedAtFinitePlaces K P →
      bigHilbertNormSubgroupContainedInRationalClassFormation K P
def

bigHilbertFiniteAbelianSubextensionIsUnramifiedAtFinitePlaces

L447 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertFiniteAbelianSubextensionIsUnramifiedAtFinitePlaces
Documentation

A finite abelian subextension of the selected rational fixed-field base is unramified at every finite place.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
def bigHilbertFiniteAbelianSubextensionIsUnramifiedAtFinitePlaces
    (K : Type) [Field K] [NumberField K]
    (P : FiniteAbelianSubextension
      (bigHilbertClassFieldBaseSubgroup K)) : Prop
instance

bigHilbertMaximalRelativeQuotientFinite

L462 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertMaximalRelativeQuotientFinite
Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section FixedFieldMaximalityInstances
variable
    (K : Type) [Field K] [NumberField K]
    (P : FiniteAbelianSubextension
      (bigHilbertClassFieldBaseSubgroup K))
Lean source · statement
instance bigHilbertMaximalRelativeQuotientFinite :
    Finite
      ((bigHilbertClassFieldBaseSubgroup K).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (bigHilbertClassFieldBaseSubgroup K)
          P.field P.below)
instance

bigHilbertMaximalRelativeFiniteDimensional

L470 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertMaximalRelativeFiniteDimensional
Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section FixedFieldMaximalityInstances
variable
    (K : Type) [Field K] [NumberField K]
    (P : FiniteAbelianSubextension
      (bigHilbertClassFieldBaseSubgroup K))
local instance bigHilbertMaximalRelativeQuotientFinite :
    Finite
      ((bigHilbertClassFieldBaseSubgroup K).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (bigHilbertClassFieldBaseSubgroup K)
          P.field P.below) :=
  P.finite
Lean source · statement
instance bigHilbertMaximalRelativeFiniteDimensional :
    FiniteDimensional
      (bigHilbertClassFieldBase K)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below)
instance

bigHilbertMaximalRelativeScalarTower

L480 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertMaximalRelativeScalarTower
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 KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section FixedFieldMaximalityInstances
variable
    (K : Type) [Field K] [NumberField K]
    (P : FiniteAbelianSubextension
      (bigHilbertClassFieldBaseSubgroup K))
local instance bigHilbertMaximalRelativeQuotientFinite :
    Finite
      ((bigHilbertClassFieldBaseSubgroup K).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (bigHilbertClassFieldBaseSubgroup K)
          P.field P.below) :=
  P.finite
noncomputable local instance bigHilbertMaximalRelativeFiniteDimensional :
    FiniteDimensional
      (bigHilbertClassFieldBase K)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    (bigHilbertClassFieldBaseSubgroup K)
    P.field P.below inferInstance P.finite
Lean source · statement
instance bigHilbertMaximalRelativeScalarTower :
    IsScalarTower ℚ
      (bigHilbertClassFieldBase K)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below)
instance

bigHilbertMaximalTopFiniteDimensional

L487 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertMaximalTopFiniteDimensional
Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section FixedFieldMaximalityInstances
variable
    (K : Type) [Field K] [NumberField K]
    (P : FiniteAbelianSubextension
      (bigHilbertClassFieldBaseSubgroup K))
local instance bigHilbertMaximalRelativeQuotientFinite :
    Finite
      ((bigHilbertClassFieldBaseSubgroup K).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (bigHilbertClassFieldBaseSubgroup K)
          P.field P.below) :=
  P.finite
noncomputable local instance bigHilbertMaximalRelativeFiniteDimensional :
    FiniteDimensional
      (bigHilbertClassFieldBase K)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    (bigHilbertClassFieldBaseSubgroup K)
    P.field P.below inferInstance P.finite
local instance bigHilbertMaximalRelativeScalarTower :
    IsScalarTower ℚ
      (bigHilbertClassFieldBase K)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
Lean source · statement
instance bigHilbertMaximalTopFiniteDimensional :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below)
instance

bigHilbertMaximalTopNumberField

L496 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertMaximalTopNumberField
Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section FixedFieldMaximalityInstances
variable
    (K : Type) [Field K] [NumberField K]
    (P : FiniteAbelianSubextension
      (bigHilbertClassFieldBaseSubgroup K))
local instance bigHilbertMaximalRelativeQuotientFinite :
    Finite
      ((bigHilbertClassFieldBaseSubgroup K).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (bigHilbertClassFieldBaseSubgroup K)
          P.field P.below) :=
  P.finite
noncomputable local instance bigHilbertMaximalRelativeFiniteDimensional :
    FiniteDimensional
      (bigHilbertClassFieldBase K)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    (bigHilbertClassFieldBaseSubgroup K)
    P.field P.below inferInstance P.finite
local instance bigHilbertMaximalRelativeScalarTower :
    IsScalarTower ℚ
      (bigHilbertClassFieldBase K)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance bigHilbertMaximalTopFiniteDimensional :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below) :=
  FiniteDimensional.trans ℚ
    (bigHilbertClassFieldBase K)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P.below)
Lean source · statement
instance bigHilbertMaximalTopNumberField :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below)
instance

bigHilbertMaximalRelativeIsGalois

L504 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertMaximalRelativeIsGalois
Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section FixedFieldMaximalityInstances
variable
    (K : Type) [Field K] [NumberField K]
    (P : FiniteAbelianSubextension
      (bigHilbertClassFieldBaseSubgroup K))
local instance bigHilbertMaximalRelativeQuotientFinite :
    Finite
      ((bigHilbertClassFieldBaseSubgroup K).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (bigHilbertClassFieldBaseSubgroup K)
          P.field P.below) :=
  P.finite
noncomputable local instance bigHilbertMaximalRelativeFiniteDimensional :
    FiniteDimensional
      (bigHilbertClassFieldBase K)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    (bigHilbertClassFieldBaseSubgroup K)
    P.field P.below inferInstance P.finite
local instance bigHilbertMaximalRelativeScalarTower :
    IsScalarTower ℚ
      (bigHilbertClassFieldBase K)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance bigHilbertMaximalTopFiniteDimensional :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below) :=
  FiniteDimensional.trans ℚ
    (bigHilbertClassFieldBase K)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P.below)
noncomputable local instance bigHilbertMaximalTopNumberField :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P.below)
Lean source · statement
instance bigHilbertMaximalRelativeIsGalois :
    IsGalois
      (bigHilbertClassFieldBase K)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below)
theorem

finiteUnramifiedAbelianSubextension_le_bigHilbertClassFieldSubextension

L517 ↗
GlobalClassFieldTheory.GlobalClassFields.finiteUnramifiedAbelianSubextension_le_bigHilbertClassFieldSubextension
Documentation

Every finite abelian subextension of the same rational fixed-field base which is unramified at all finite places is contained in the selected big Hilbert class-field subextension.

Source context 14 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
section FixedFieldMaximalityInstances
variable
    (K : Type) [Field K] [NumberField K]
    (P : FiniteAbelianSubextension
      (bigHilbertClassFieldBaseSubgroup K))
local instance bigHilbertMaximalRelativeQuotientFinite :
    Finite
      ((bigHilbertClassFieldBaseSubgroup K).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (bigHilbertClassFieldBaseSubgroup K)
          P.field P.below) :=
  P.finite
noncomputable local instance bigHilbertMaximalRelativeFiniteDimensional :
    FiniteDimensional
      (bigHilbertClassFieldBase K)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    (bigHilbertClassFieldBaseSubgroup K)
    P.field P.below inferInstance P.finite
local instance bigHilbertMaximalRelativeScalarTower :
    IsScalarTower ℚ
      (bigHilbertClassFieldBase K)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance bigHilbertMaximalTopFiniteDimensional :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below) :=
  FiniteDimensional.trans ℚ
    (bigHilbertClassFieldBase K)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P.below)
noncomputable local instance bigHilbertMaximalTopNumberField :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P.below)
noncomputable local instance bigHilbertMaximalRelativeIsGalois :
    IsGalois
      (bigHilbertClassFieldBase K)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    (bigHilbertClassFieldBaseSubgroup K)
    P.field P.below P.normal
Lean source · statement
theorem
    finiteUnramifiedAbelianSubextension_le_bigHilbertClassFieldSubextension
    (K : Type) [Field K] [NumberField K]
    (P : FiniteAbelianSubextension
      (bigHilbertClassFieldBaseSubgroup K)) :
    bigHilbertFiniteAbelianSubextensionIsUnramifiedAtFinitePlaces K P →
      P ≤ bigHilbertClassFieldSubextension K
theorem

bigHilbertClassFieldSubextension_isFiniteUnramifiedAndMaximalAbelian

L558 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldSubextension_isFiniteUnramifiedAndMaximalAbelian
Documentation

The selected big Hilbert class field is genuinely finite-unramified, and its finite abelian subextension is maximal among all actual finite-unramified abelian subextensions of the same rational fixed-field base.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem
    bigHilbertClassFieldSubextension_isFiniteUnramifiedAndMaximalAbelian
    (K : Type) [Field K] [NumberField K] :
    IsUnramifiedAtFinitePlaces K (bigHilbertClassField K) ∧
      ∀ P : FiniteAbelianSubextension
          (bigHilbertClassFieldBaseSubgroup K),
        bigHilbertFiniteAbelianSubextensionIsUnramifiedAtFinitePlaces K P →
          P ≤ bigHilbertClassFieldSubextension K
def

bigHilbertClassFieldBaseEmbedding

L586 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldBaseEmbedding
Documentation

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

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
def bigHilbertClassFieldBaseEmbedding
    (K : Type) [Field K] [NumberField K] :
    K →ₐ[ℚ] SeparableClosure ℚ
theorem

bigHilbertClassFieldBaseEquiv_coe

L595 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldBaseEquiv_coe
Documentation

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

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem bigHilbertClassFieldBaseEquiv_coe
    (K : Type) [Field K] [NumberField K]
    (x : K) :
    ((bigHilbertClassFieldBaseEquiv (K := K) x :
        bigHilbertClassFieldBase K) :
      SeparableClosure ℚ) =
      bigHilbertClassFieldBaseEmbedding K x
def

bigHilbertClassFieldCompatibleEmbedding

L607 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldCompatibleEmbedding
Documentation

An actual finite extension of K, embedded into the rational separable closure so that its restriction to K is exactly the base embedding used by the selected big Hilbert class field.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
def bigHilbertClassFieldCompatibleEmbedding
    (K E : Type)
    [Field K] [NumberField K]
    [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E] :
    E →ₐ[ℚ] SeparableClosure ℚ
theorem

bigHilbertClassFieldCompatibleEmbedding_restrictDomain

L622 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldCompatibleEmbedding_restrictDomain
Documentation

Compatibility of the chosen ambient embedding with the selected copy of the original base field.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem bigHilbertClassFieldCompatibleEmbedding_restrictDomain
    (K E : Type)
    [Field K] [NumberField K]
    [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E] :
    (bigHilbertClassFieldCompatibleEmbedding K E).domRestrict K =
      bigHilbertClassFieldBaseEmbedding K
theorem

bigHilbertClassFieldCompatibleEmbedding_algebraMap

L638 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldCompatibleEmbedding_algebraMap
Documentation

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

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem bigHilbertClassFieldCompatibleEmbedding_algebraMap
    (K E : Type)
    [Field K] [NumberField K]
    [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    (x : K) :
    bigHilbertClassFieldCompatibleEmbedding K E
        (algebraMap K E x) =
      bigHilbertClassFieldBaseEmbedding K x
theorem

bigHilbertClassFieldCompatibleEmbedding_baseSubgroup

L655 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldCompatibleEmbedding_baseSubgroup
Documentation

The fixing subgroup of the compatible embedded copy of K is the base subgroup of the selected big Hilbert class field.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem bigHilbertClassFieldCompatibleEmbedding_baseSubgroup
    (K E : Type)
    [Field K] [NumberField K]
    [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E] :
    numberFieldEmbeddedBaseSubgroup K E
        (bigHilbertClassFieldCompatibleEmbedding K E) =
      bigHilbertClassFieldBaseSubgroup K
def

bigHilbertClassFieldEmbeddedAbelianSubextension

L678 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldEmbeddedAbelianSubextension
Documentation

The actual finite abelian extension E / K, represented inside the same rational absolute Galois group as the selected big Hilbert class field.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
def bigHilbertClassFieldEmbeddedAbelianSubextension
    (K E : Type)
    [Field K] [NumberField K]
    [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    [IsAbelianGalois K E] :
    FiniteAbelianSubextension
      (bigHilbertClassFieldBaseSubgroup K)
theorem

bigHilbertClassFieldEmbeddedAbelianSubextension_field

L694 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldEmbeddedAbelianSubextension_field
Documentation

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

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem bigHilbertClassFieldEmbeddedAbelianSubextension_field
    (K E : Type)
    [Field K] [NumberField K]
    [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    [IsAbelianGalois K E] :
    (bigHilbertClassFieldEmbeddedAbelianSubextension K E).field =
      numberFieldEmbeddedTopSubgroup K E
        (bigHilbertClassFieldCompatibleEmbedding K E)
theorem

finitePlaceUnramifiedness_congrTop

L711 ↗
GlobalClassFieldTheory.GlobalClassFields.finitePlaceUnramifiedness_congrTop
Documentation

Finite-prime unramifiedness is preserved when the top number field is replaced by an equivalent K-algebra.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem finitePlaceUnramifiedness_congrTop
    {K L M : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Field M] [NumberField M]
    [Algebra K L] [Algebra K M]
    (e : L ≃ₐ[K] M)
    (h : IsUnramifiedAtFinitePlaces K L) :
    IsUnramifiedAtFinitePlaces K M
def

finiteUnramifiedAbelianExtensionEmbeddingIntoBigHilbertClassField

L743 ↗
GlobalClassFieldTheory.GlobalClassFields.finiteUnramifiedAbelianExtensionEmbeddingIntoBigHilbertClassField
Documentation

Any actual finite unramified abelian extension of K embeds over K into the selected big Hilbert class field.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
def
    finiteUnramifiedAbelianExtensionEmbeddingIntoBigHilbertClassField
    (K E : Type)
    [Field K] [NumberField K]
    [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    [IsAbelianGalois K E]
    (hunramified : IsUnramifiedAtFinitePlaces K E) :
    E →ₐ[K] bigHilbertClassField K
theorem

finiteUnramifiedAbelianExtension_nonempty_algHom_bigHilbertClassField

L863 ↗
GlobalClassFieldTheory.GlobalClassFields.finiteUnramifiedAbelianExtension_nonempty_algHom_bigHilbertClassField
Documentation

Containment form of maximality: every finite unramified abelian extension of K has a K-embedding into the selected big Hilbert class field.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem
    finiteUnramifiedAbelianExtension_nonempty_algHom_bigHilbertClassField
    (K E : Type)
    [Field K] [NumberField K]
    [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    [IsAbelianGalois K E]
    (hunramified : IsUnramifiedAtFinitePlaces K E) :
    Nonempty (E →ₐ[K] bigHilbertClassField K)
theorem

bigHilbertClassField_isMaximalUnramifiedAbelianExtension

L879 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField_isMaximalUnramifiedAbelianExtension
Documentation

The selected big Hilbert class field is the actual maximal finite unramified abelian extension of the original number field: it is finite, abelian Galois and unramified at every finite prime, and it contains every other finite unramified abelian extension over the same base.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open LocalClassFieldTheory NumberField Reciprocity
Lean source · statement
theorem bigHilbertClassField_isMaximalUnramifiedAbelianExtension
    (K : Type) [Field K] [NumberField K] :
    FiniteDimensional K (bigHilbertClassField K) ∧
      IsAbelianGalois K (bigHilbertClassField K) ∧
      IsUnramifiedAtFinitePlaces K (bigHilbertClassField K) ∧
      ∀ (E : Type) [Field E] [NumberField E]
        [Algebra K E] [FiniteDimensional K E]
        [IsAbelianGalois K E],
        IsUnramifiedAtFinitePlaces K E →
          Nonempty (E →ₐ[K] bigHilbertClassField K)

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