NYLL
Module

SmallHilbertTowerConjugation.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.SmallHilbertTowerConjugation
46 declarations indexed from sourceView source ↗

Module documentation

Conjugation of the small Hilbert class-field tower

For a finite abelian tower, conjugation by the lower base carries the relative norm subgroup of the upper extension to the relative norm subgroup of the conjugate extension. In the rational absolute idele-class formation, the subgroup defining the small Hilbert class field is intrinsic under the corresponding automorphism of its actual fixed field. Finite abelian classification therefore identifies every conjugate of the second small Hilbert class field with the original field.

Imports9
Imported by3

Declarations

theorem

addSubgroup_map_map_eq_of_comp_eq

L41 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.addSubgroup_map_map_eq_of_comp_eq
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
Lean source · statement
theorem addSubgroup_map_map_eq_of_comp_eq
    {A B C : Type*} [AddGroup A] [AddGroup B] [AddGroup C]
    (S : AddSubgroup A) (f : A →+ B) (g : B →+ C) (h : A →+ C)
    (hcomp : g.comp f = h) :
    (S.map f).map g = S.map h
theorem

addSubgroup_map_addEquiv_then_symm

L48 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.addSubgroup_map_addEquiv_then_symm
Source context 6 commands

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

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

addSubgroup_map_le_of_le_map_symm

L66 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.addSubgroup_map_le_of_le_map_symm
Source context 6 commands

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

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

addSubgroup_map_eq_of_comp_eq_of_map_eq

L81 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.addSubgroup_map_eq_of_comp_eq_of_map_eq
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
Lean source · statement
theorem addSubgroup_map_eq_of_comp_eq_of_map_eq
    {A B : Type*} [AddGroup A] [AddGroup B]
    (S : AddSubgroup A) (e : A →+ B) (g : A →+ A) (t : B →+ B)
    (hcomp : t.comp e = e.comp g) (hg : S.map g = S) :
    (S.map e).map t = S.map e
theorem

subgroup_toAddSubgroup_map_toAdditive_eq_self

L93 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.subgroup_toAddSubgroup_map_toAdditive_eq_self
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
Lean source · statement
theorem subgroup_toAddSubgroup_map_toAdditive_eq_self
    {G : Type*} [Group G]
    (S : Subgroup G) (f : G →* G) (hf : S.map f = S) :
    S.toAddSubgroup.map (MonoidHom.toAdditive f) =
      S.toAddSubgroup
theorem

conjugateFiniteAbelianSubextensionField_eq_self

L109 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.conjugateFiniteAbelianSubextensionField_eq_self
Documentation

A finite Galois field in an abelian tower is stable under conjugation by every element of its base subgroup.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section AbstractConjugation
variable
    {G : IntegralRepGroupType}
    [Group G] [TopologicalSpace G] [ContinuousMul G]
Lean source · statement
theorem conjugateFiniteAbelianSubextensionField_eq_self
    {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K)
    (s : K.toSubgroup) :
    conjugateClosedSubgroup L.field s.1 = L.field
def

conjugateFixedAddEquiv

L154 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.conjugateFixedAddEquiv
Documentation

Conjugation gives an additive equivalence between the two actual fixed parts of a coefficient representation.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section AbstractConjugation
variable
    {G : IntegralRepGroupType}
    [Group G] [TopologicalSpace G] [ContinuousMul G]
Lean source · full declaration
def conjugateFixedAddEquiv
    (A : Rep ℤ G) (K : ClosedSubgroup G) (s : G) :
    ambientFixedAddSubgroup A K ≃+
      ambientFixedAddSubgroup A (conjugateClosedSubgroup K s) where
  toFun := conjugateFixedElement A K s
  invFun := fun b => by
    refine ⟨A.ρ s b.1, ?_⟩
    intro k
    let kConj :
        (conjugateClosedSubgroup K s).toSubgroup :=
      ⟨s⁻¹ * k.1 * s,
        (conjugateClosedSubgroup_mem K s _).2 (by
          simp [mul_assoc])⟩
    calc
      A.ρ k.1 (A.ρ s b.1) =
          A.ρ (k.1 * s) b.1 := by
            exact congrArg (fun φ => φ b.1)
              (map_mul A.ρ k.1 s).symm
      _ = A.ρ (s * kConj.1) b.1 := by
            congr 2
            simp [kConj, mul_assoc]
      _ = A.ρ s (A.ρ kConj.1 b.1) := by
            exact congrArg (fun φ => φ b.1)
              (map_mul A.ρ s kConj.1)
      _ = A.ρ s b.1 := by rw [b.2 kConj]
  left_inv := by
    intro a
    apply Subtype.ext
    change A.ρ s (A.ρ s⁻¹ a.1) = a.1
    calc
      A.ρ s (A.ρ s⁻¹ a.1) =
          A.ρ (s * s⁻¹) a.1 := by
            exact congrArg (fun φ => φ a.1)
              (map_mul A.ρ s s⁻¹).symm
      _ = a.1 := by simp
  right_inv := by
    intro b
    apply Subtype.ext
    change A.ρ s⁻¹ (A.ρ s b.1) = b.1
    calc
      A.ρ s⁻¹ (A.ρ s b.1) =
          A.ρ (s⁻¹ * s) b.1 := by
            exact congrArg (fun φ => φ b.1)
              (map_mul A.ρ s⁻¹ s).symm
      _ = b.1 := by simp
  map_add' := by
    intro a b
    apply Subtype.ext
    exact map_add (A.ρ s⁻¹) a.1 b.1
theorem

finiteNormSubgroup_map_conjugateFixed

L206 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.finiteNormSubgroup_map_conjugateFixed
Documentation

Relative norm images are carried exactly to the norm images of the conjugate extension.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section AbstractConjugation
variable
    {G : IntegralRepGroupType}
    [Group G] [TopologicalSpace G] [ContinuousMul G]
Lean source · full declaration
theorem finiteNormSubgroup_map_conjugateFixed
    (A : Rep ℤ G)
    (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (s : G)
    [Finite
      (K.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup K L hLK)] :
    letI : Finite
        ((conjugateClosedSubgroup K s).toSubgroup ⧸
          CyclicCohomology.extensionSubgroup
            (conjugateClosedSubgroup K s)
            (conjugateClosedSubgroup L s)
            (conjugateClosedSubgroup_mono hLK s)) :=
      finite_conjugateExtension K L hLK s
    (finiteNormSubgroup A K L hLK).map
        (conjugateFixedElementHom A K s) =
      finiteNormSubgroup A
        (conjugateClosedSubgroup K s)
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s) := by
  let : Finite
      ((conjugateClosedSubgroup K s).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (conjugateClosedSubgroup K s)
          (conjugateClosedSubgroup L s)
          (conjugateClosedSubgroup_mono hLK s)) :=
    finite_conjugateExtension K L hLK s
  ext y
  constructor
  · rintro ⟨_, ⟨a, rfl⟩, rfl⟩
    refine ⟨conjugateFixedElement A L s a, ?_⟩
    exact relativeNorm_conjugate_apply A K L hLK s a
  · rintro ⟨b, rfl⟩
    let a :=
      (conjugateFixedAddEquiv A L s).symm b
    refine
      ⟨relativeNorm A K L hLK a, ⟨a, rfl⟩, ?_⟩
    change
      conjugateFixedElement A K s
          (relativeNorm A K L hLK a) =
        relativeNorm A
          (conjugateClosedSubgroup K s)
          (conjugateClosedSubgroup L s)
          (conjugateClosedSubgroup_mono hLK s) b
    calc
      conjugateFixedElement A K s
          (relativeNorm A K L hLK a) =
          relativeNorm A
            (conjugateClosedSubgroup K s)
            (conjugateClosedSubgroup L s)
            (conjugateClosedSubgroup_mono hLK s)
            (conjugateFixedElement A L s a) :=
        (relativeNorm_conjugate_apply
          A K L hLK s a).symm
      _ =
          relativeNorm A
            (conjugateClosedSubgroup K s)
            (conjugateClosedSubgroup L s)
            (conjugateClosedSubgroup_mono hLK s) b := by
        rw [show conjugateFixedElement A L s a = b by
          exact
            (conjugateFixedAddEquiv A L s).apply_symm_apply b]
def

rebaseFiniteAbelianSubextension

L270 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rebaseFiniteAbelianSubextension
Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section AbstractConjugation
variable
    {G : IntegralRepGroupType}
    [Group G] [TopologicalSpace G] [ContinuousMul G]
Lean source · statement
def rebaseFiniteAbelianSubextension
    {K K' : ClosedSubgroup G} (h : K = K')
    (L : FiniteAbelianSubextension K) :
    FiniteAbelianSubextension K'
theorem

rebaseFiniteAbelianSubextension_field

L278 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rebaseFiniteAbelianSubextension_field
Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section AbstractConjugation
variable
    {G : IntegralRepGroupType}
    [Group G] [TopologicalSpace G] [ContinuousMul G]
omit [ContinuousMul G] in
Lean source · statement
theorem rebaseFiniteAbelianSubextension_field
    {K K' : ClosedSubgroup G} (h : K = K')
    (L : FiniteAbelianSubextension K) :
    (rebaseFiniteAbelianSubextension h L).field = L.field
def

rebaseFixedCodomainHom

L285 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rebaseFixedCodomainHom
Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section AbstractConjugation
variable
    {G : IntegralRepGroupType}
    [Group G] [TopologicalSpace G] [ContinuousMul G]
Lean source · statement
def rebaseFixedCodomainHom
    (A : Rep ℤ G)
    {X : Type*} [AddGroup X]
    {K K' : ClosedSubgroup G} (h : K = K')
    (f : X →+ ambientFixedAddSubgroup A K) :
    X →+
      ambientFixedAddSubgroup A K'
theorem

rebaseFixedCodomainHom_coe

L297 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rebaseFixedCodomainHom_coe
Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section AbstractConjugation
variable
    {G : IntegralRepGroupType}
    [Group G] [TopologicalSpace G] [ContinuousMul G]
omit [ContinuousMul G] in
Lean source · statement
theorem rebaseFixedCodomainHom_coe
    (A : Rep ℤ G)
    {X : Type*} [AddGroup X]
    {K K' : ClosedSubgroup G} (h : K = K')
    (f : X →+ ambientFixedAddSubgroup A K)
    (a : X) :
    ((rebaseFixedCodomainHom A h f a :
      ambientFixedAddSubgroup A K') : A.V) =
      (f a : A.V)
def

rebaseFixedAddSubgroup

L309 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rebaseFixedAddSubgroup
Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section AbstractConjugation
variable
    {G : IntegralRepGroupType}
    [Group G] [TopologicalSpace G] [ContinuousMul G]
Lean source · statement
def rebaseFixedAddSubgroup
    (A : Rep ℤ G) {K K' : ClosedSubgroup G}
    (h : K = K')
    (H : AddSubgroup (ambientFixedAddSubgroup A K)) :
    AddSubgroup (ambientFixedAddSubgroup A K')
theorem

rebaseFixedAddSubgroup_map

L318 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rebaseFixedAddSubgroup_map
Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section AbstractConjugation
variable
    {G : IntegralRepGroupType}
    [Group G] [TopologicalSpace G] [ContinuousMul G]
omit [ContinuousMul G] in
Lean source · statement
theorem rebaseFixedAddSubgroup_map
    (A : Rep ℤ G) {K K' : ClosedSubgroup G}
    (h : K = K')
    {X : Type*} [AddGroup X] (H : AddSubgroup X)
    (f : X →+ ambientFixedAddSubgroup A K) :
    rebaseFixedAddSubgroup A h (H.map f) =
      H.map (rebaseFixedCodomainHom A h f)
theorem

rebaseFiniteAbelianSubextension_normSubgroup

L329 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rebaseFiniteAbelianSubextension_normSubgroup
Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section AbstractConjugation
variable
    {G : IntegralRepGroupType}
    [Group G] [TopologicalSpace G] [ContinuousMul G]
omit [ContinuousMul G] in
Lean source · statement
theorem rebaseFiniteAbelianSubextension_normSubgroup
    (A : Rep ℤ G) {K K' : ClosedSubgroup G}
    (h : K = K') (L : FiniteAbelianSubextension K) :
    (rebaseFiniteAbelianSubextension h L).normSubgroup A =
      rebaseFixedAddSubgroup A h (L.normSubgroup A)
def

conjugateFiniteAbelianSubextensionOverBase

L339 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.conjugateFiniteAbelianSubextensionOverBase
Documentation

Conjugation of the upper extension, transported back across the conjugation-stability equality of its abelian base.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section AbstractConjugation
variable
    {G : IntegralRepGroupType}
    [Group G] [TopologicalSpace G] [ContinuousMul G]
Lean source · statement
def conjugateFiniteAbelianSubextensionOverBase
    {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K)
    (M : FiniteAbelianSubextension L.field)
    (s : K.toSubgroup) :
    FiniteAbelianSubextension L.field
theorem

conjugateFiniteAbelianSubextensionOverBase_field

L350 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.conjugateFiniteAbelianSubextensionOverBase_field
Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section AbstractConjugation
variable
    {G : IntegralRepGroupType}
    [Group G] [TopologicalSpace G] [ContinuousMul G]
Lean source · statement
theorem conjugateFiniteAbelianSubextensionOverBase_field
    {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K)
    (M : FiniteAbelianSubextension L.field)
    (s : K.toSubgroup) :
    (conjugateFiniteAbelianSubextensionOverBase L M s).field =
      conjugateClosedSubgroup M.field s.1
def

stableBaseConjugationHom

L365 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.stableBaseConjugationHom
Documentation

The canonical conjugation map on the fixed part, transported along the conjugation-stability equality of the abelian base.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section AbstractConjugation
variable
    {G : IntegralRepGroupType}
    [Group G] [TopologicalSpace G] [ContinuousMul G]
Lean source · statement
def stableBaseConjugationHom
    (A : Rep ℤ G)
    {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K)
    (s : K.toSubgroup) :
    ambientFixedAddSubgroup A L.field →+
      ambientFixedAddSubgroup A L.field
theorem

stableBaseConjugationHom_coe

L377 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.stableBaseConjugationHom_coe
Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section AbstractConjugation
variable
    {G : IntegralRepGroupType}
    [Group G] [TopologicalSpace G] [ContinuousMul G]
Lean source · statement
theorem stableBaseConjugationHom_coe
    (A : Rep ℤ G)
    {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K)
    (s : K.toSubgroup)
    (a : ambientFixedAddSubgroup A L.field) :
    ((stableBaseConjugationHom A L s a :
      ambientFixedAddSubgroup A L.field) : A.V) =
      A.ρ s.1⁻¹ a.1
theorem

conjugateFiniteAbelianSubextensionOverBase_normSubgroup

L401 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.conjugateFiniteAbelianSubextensionOverBase_normSubgroup
Documentation

The norm subgroup of the conjugate upper extension is the image of the original norm subgroup under the actual action on the fixed part of the stable base.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section AbstractConjugation
variable
    {G : IntegralRepGroupType}
    [Group G] [TopologicalSpace G] [ContinuousMul G]
Lean source · statement
theorem conjugateFiniteAbelianSubextensionOverBase_normSubgroup
    (A : Rep ℤ G)
    {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K)
    (M : FiniteAbelianSubextension L.field)
    (s : K.toSubgroup) :
    (conjugateFiniteAbelianSubextensionOverBase L M s).normSubgroup A =
      (M.normSubgroup A).map
        (stableBaseConjugationHom A L s)
instance

smallHilbertTowerBaseQuotientFinite

L446 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerBaseQuotientFinite
Source context 7 commands

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

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

smallHilbertTowerRelativeQuotientFinite

L458 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerRelativeQuotientFinite
Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
Lean source · statement
instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below)
instance

smallHilbertTowerBaseFiniteDimensional

L468 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerBaseFiniteDimensional
Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
Lean source · statement
instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
instance

smallHilbertTowerRelativeFiniteDimensional

L476 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerRelativeFiniteDimensional
Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
Lean source · statement
instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below)
instance

smallHilbertTowerScalarTower

L488 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerScalarTower
Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
Lean source · statement
instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below)
instance

smallHilbertTowerAbsoluteFiniteDimensional

L498 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerAbsoluteFiniteDimensional
Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
Lean source · statement
instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below)
instance

smallHilbertTowerBaseNumberField

L510 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerBaseNumberField
Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
Lean source · statement
instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
instance

smallHilbertTowerRelativeNumberField

L518 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerRelativeNumberField
Source context 14 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
Lean source · statement
instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below)
instance

smallHilbertTowerRelativeIsGalois

L529 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerRelativeIsGalois
Source context 15 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
Lean source · statement
instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below)
def

smallHilbertNormSubgroupInRationalClassFormation

L544 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertNormSubgroupInRationalClassFormation
Documentation

The ordinary small-Hilbert norm subgroup of an actual fixed field, transported into the fixed part of the rational absolute idele-class representation.

Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · statement
def smallHilbertNormSubgroupInRationalClassFormation
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    AddSubgroup
      (ambientFixedAddSubgroup
        rationalIdeleClassRepresentation K.field)
theorem

finiteAbelianNormSubgroup_map_fixedIdeleClassEquiv_symm

L556 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.finiteAbelianNormSubgroup_map_fixedIdeleClassEquiv_symm
Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · statement
theorem finiteAbelianNormSubgroup_map_fixedIdeleClassEquiv_symm
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    (L.normSubgroup rationalIdeleClassRepresentation).map
        (rationalAbstractFixedFieldIdeleClassEquivFixed
          K.field).symm.toAddMonoidHom =
      (_root_.ideleClassNorm
        (abstractFixedField
          ℚ (SeparableClosure ℚ) K.field)
        (abstractRelativeFixedField
          ℚ (SeparableClosure ℚ) L.below)).range.toAddSubgroup
theorem

smallHilbertNormSubgroupInRationalClassFormation_le_normSubgroup_of_fixedFieldNormRange

L571 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertNormSubgroupInRationalClassFormation_le_normSubgroup_of_fixedFieldNormRange
Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · statement
theorem
    smallHilbertNormSubgroupInRationalClassFormation_le_normSubgroup_of_fixedFieldNormRange
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
    (hordinary :
      smallHilbertClassFieldNormSubgroup
          (K := abstractFixedField
            ℚ (SeparableClosure ℚ) K.field) ≤
        (_root_.ideleClassNorm
          (abstractFixedField
            ℚ (SeparableClosure ℚ) K.field)
          (abstractRelativeFixedField
            ℚ (SeparableClosure ℚ) L.below)).range) :
    smallHilbertNormSubgroupInRationalClassFormation K ≤
      L.normSubgroup rationalIdeleClassRepresentation
theorem

smallHilbertNormSubgroupInRationalClassFormation_le_normSubgroup_of_everywhereUnramified

L607 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertNormSubgroupInRationalClassFormation_le_normSubgroup_of_everywhereUnramified
Documentation

Maximality of the intrinsic small-Hilbert norm subgroup, transported from the actual fixed-field extension back into the rational absolute class formation. For an extension unramified at every finite and infinite place, the canonical small-Hilbert subgroup is contained in its genuine abstract norm subgroup.

Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · statement
theorem
    smallHilbertNormSubgroupInRationalClassFormation_le_normSubgroup_of_everywhereUnramified
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsUnramifiedAtInfinitePlaces
        (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
        (abstractRelativeFixedField
          ℚ (SeparableClosure ℚ) L.below) →
      _root_.ramifiedBaseFinitePlaces
          (K := abstractFixedField
            ℚ (SeparableClosure ℚ) K.field)
          (L := abstractRelativeFixedField
            ℚ (SeparableClosure ℚ) L.below) = ∅ →
        smallHilbertNormSubgroupInRationalClassFormation K ≤
          L.normSubgroup rationalIdeleClassRepresentation
theorem

everywhereUnramifiedFiniteAbelianSubextension_le_smallHilbertClassField

L645 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.everywhereUnramifiedFiniteAbelianSubextension_le_smallHilbertClassField
Documentation

Every finite abelian extension of the same actual base which is unramified at all finite and infinite places lies in any realization of the small Hilbert class field. The conclusion is a field-order statement: it follows from the genuine fixed-field norm comparison and the order-reversing finite abelian classification.

Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · statement
theorem everywhereUnramifiedFiniteAbelianSubextension_le_smallHilbertClassField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L P : FiniteAbelianSubextension K.field)
    (hL :
      L.normSubgroup rationalIdeleClassRepresentation =
        smallHilbertNormSubgroupInRationalClassFormation K) :
    IsEverywhereUnramified
        (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
        (abstractRelativeFixedField
          ℚ (SeparableClosure ℚ) P.below) →
      P ≤ L
def

smallHilbertBaseConjugationAutomorphism

L684 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertBaseConjugationAutomorphism
Documentation

The automorphism of the actual upper fixed field induced by the inverse of an element of the lower base subgroup. The inverse is the one appearing in right conjugation and in conjugateFixedElement.

Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · full declaration
def smallHilbertBaseConjugationAutomorphism
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
    (s : K.field.toSubgroup) :
    let E :=
      abstractFixedField ℚ (SeparableClosure ℚ) L.field
    E ≃ₐ[ℚ] E :=
  letI :
      (CyclicCohomology.extensionSubgroup
        K.field L.field L.below).Normal :=
    L.normal
  (abstractExtensionQuotientEquivGaloisGroup
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
    (QuotientGroup.mk'
      (CyclicCohomology.extensionSubgroup
        K.field L.field L.below)
      s⁻¹)).restrictScalars ℚ
theorem

smallHilbertBaseConjugationAutomorphism_apply_val

L706 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertBaseConjugationAutomorphism_apply_val
Documentation

The fixed-field automorphism used for stable conjugation is induced by the inverse ambient automorphism on underlying separable-closure elements.

Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · statement
theorem smallHilbertBaseConjugationAutomorphism_apply_val
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
    (s : K.field.toSubgroup)
    (x : abstractFixedField ℚ (SeparableClosure ℚ) L.field) :
    ((smallHilbertBaseConjugationAutomorphism K L s x :
        abstractFixedField ℚ (SeparableClosure ℚ) L.field) :
      SeparableClosure ℚ) =
      s.1⁻¹ (x : SeparableClosure ℚ)
theorem

rationalSmallHilbertFixedPart_conjugation

L740 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rationalSmallHilbertFixedPart_conjugation
Documentation

On the actual fixed part of the rational idele-class formation, conjugation by an element of the lower base is ordinary idele-class transport along the induced automorphism of the upper fixed field.

Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · full declaration
theorem rationalSmallHilbertFixedPart_conjugation
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
    (s : K.field.toSubgroup) :
    let E :=
      abstractFixedField ℚ (SeparableClosure ℚ) L.field
    letI hLfinite : Finite
        ((baseField
          (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
          CyclicCohomology.extensionSubgroup
            (baseField
              (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
            L.field (le_baseField L.field)) :=
      (L.toFiniteGaloisExtension.toFiniteAbstractFieldExtension).field.finite
    letI : FiniteDimensional ℚ E :=
      abstractFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) L.field hLfinite
    letI : NumberField E :=
      NumberField.of_module_finite ℚ E
    ∀ c : Additive (IdeleClassGroup E),
    stableBaseConjugationHom
        rationalIdeleClassRepresentation L s
        (rationalAbstractFixedFieldIdeleClassEquivFixed
          L.field c) =
      rationalAbstractFixedFieldIdeleClassEquivFixed
        L.field
        (Additive.ofMul
          (ideleClassCongr
            (smallHilbertBaseConjugationAutomorphism K L s)
            (Additive.toMul c))) := by
  dsimp only
  let E :=
    abstractFixedField ℚ (SeparableClosure ℚ) L.field
  let hLfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          L.field (le_baseField L.field)) :=
    (L.toFiniteGaloisExtension.toFiniteAbstractFieldExtension).field.finite
  let : FiniteDimensional ℚ E :=
    abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) L.field hLfinite
  let : NumberField E :=
    NumberField.of_module_finite ℚ E
  intro c
  let τ : E ≃ₐ[ℚ] E :=
    smallHilbertBaseConjugationAutomorphism K L s
  have hστ : ∀ x : E,
      ((τ x : E) : SeparableClosure ℚ) =
        s.1⁻¹ (x : SeparableClosure ℚ) := by
    intro x
    exact smallHilbertBaseConjugationAutomorphism_apply_val K L s x
  let cτ : Additive (IdeleClassGroup E) :=
    Additive.ofMul
      (ideleClassCongr τ (Additive.toMul c))
  have haction :
      rationalIdeleClassRepresentation.ρ s.1⁻¹
          (rationalIdeleClassEquivFixed E c).1 =
        (rationalIdeleClassEquivFixed E cτ).1 := by
    simpa only [cτ, ofMul_toMul] using
      (rationalIdeleClassEquivFixed_ambientAlgEquiv
        s.1⁻¹ τ hστ (Additive.toMul c))
  have hstable
      (a : ambientFixedAddSubgroup
        rationalIdeleClassRepresentation L.field) :
      ((stableBaseConjugationHom
          rationalIdeleClassRepresentation L s a :
        ambientFixedAddSubgroup
          rationalIdeleClassRepresentation L.field) :
      rationalIdeleClassRepresentation.V) =
      rationalIdeleClassRepresentation.ρ s.1⁻¹ a.1 := by
    exact stableBaseConjugationHom_coe
      rationalIdeleClassRepresentation L s a
  have hcoe (z : Additive (IdeleClassGroup E)) :
      (rationalAbstractFixedFieldIdeleClassEquivFixed L.field
          (hfinite := hLfinite) z).1 =
        (rationalIdeleClassEquivFixed E z).1 :=
    rationalAbstractFixedFieldIdeleClassEquivFixed_coe
      L.field (hfinite := hLfinite) z
  apply Subtype.ext
  exact
    (hstable
      (rationalAbstractFixedFieldIdeleClassEquivFixed
        L.field (hfinite := hLfinite) c)).trans
      ((congrArg (rationalIdeleClassRepresentation.ρ s.1⁻¹)
        (hcoe c)).trans
        (haction.trans (hcoe cτ).symm))
theorem

smallHilbertClassFieldNormSubgroup_toAddSubgroup_map_ideleClassCongr

L831 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldNormSubgroup_toAddSubgroup_map_ideleClassCongr
Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · statement
theorem
    smallHilbertClassFieldNormSubgroup_toAddSubgroup_map_ideleClassCongr
    (E : Type*) [Field E] [NumberField E]
    (τ : E ≃ₐ[ℚ] E) :
    (smallHilbertClassFieldNormSubgroup
        (K := E)).toAddSubgroup.map
          (MonoidHom.toAdditive
            (ideleClassCongr τ).toMonoidHom) =
      (smallHilbertClassFieldNormSubgroup
        (K := E)).toAddSubgroup
theorem

rationalSmallHilbertFixedPart_conjugation_comp

L847 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rationalSmallHilbertFixedPart_conjugation_comp
Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · full declaration
theorem rationalSmallHilbertFixedPart_conjugation_comp
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
    (s : K.field.toSubgroup) :
    let E :=
      abstractFixedField ℚ (SeparableClosure ℚ) L.field
    letI hLfinite : Finite
        ((baseField
          (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
          CyclicCohomology.extensionSubgroup
            (baseField
              (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
            L.field (le_baseField L.field)) :=
      (L.toFiniteGaloisExtension.toFiniteAbstractFieldExtension).field.finite
    letI : FiniteDimensional ℚ E :=
      abstractFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) L.field hLfinite
    letI : NumberField E :=
      NumberField.of_module_finite ℚ E
    (stableBaseConjugationHom
        rationalIdeleClassRepresentation L s).comp
        (rationalAbstractFixedFieldIdeleClassEquivFixed
          L.field).toAddMonoidHom =
      (rationalAbstractFixedFieldIdeleClassEquivFixed
        L.field).toAddMonoidHom.comp
        (MonoidHom.toAdditive
          (ideleClassCongr
            (smallHilbertBaseConjugationAutomorphism K L s)).toMonoidHom) := by
  dsimp only
  let E :=
    abstractFixedField ℚ (SeparableClosure ℚ) L.field
  let hLfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          L.field (le_baseField L.field)) :=
    (L.toFiniteGaloisExtension.toFiniteAbstractFieldExtension).field.finite
  let : FiniteDimensional ℚ E :=
    abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) L.field hLfinite
  let : NumberField E :=
    NumberField.of_module_finite ℚ E
  apply AddMonoidHom.ext
  intro c
  change
    stableBaseConjugationHom
        rationalIdeleClassRepresentation L s
        (rationalAbstractFixedFieldIdeleClassEquivFixed L.field c) =
      rationalAbstractFixedFieldIdeleClassEquivFixed L.field
        (Additive.ofMul
          (ideleClassCongr
            (smallHilbertBaseConjugationAutomorphism K L s)
            (Additive.toMul c)))
  exact rationalSmallHilbertFixedPart_conjugation K L s c
theorem

smallHilbertNormSubgroupInRationalClassFormation_map_conjugation_canonical

L905 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertNormSubgroupInRationalClassFormation_map_conjugation_canonical
Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · full declaration
theorem
    smallHilbertNormSubgroupInRationalClassFormation_map_conjugation_canonical
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
    (s : K.field.toSubgroup) :
    let E :=
      abstractFixedField ℚ (SeparableClosure ℚ) L.field
    letI hLfinite : Finite
        ((baseField
          (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
          CyclicCohomology.extensionSubgroup
            (baseField
              (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
            L.field (le_baseField L.field)) :=
      (L.toFiniteGaloisExtension.toFiniteAbstractFieldExtension).field.finite
    letI : FiniteDimensional ℚ E :=
      abstractFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) L.field hLfinite
    letI : NumberField E :=
      NumberField.of_module_finite ℚ E
    ((smallHilbertClassFieldNormSubgroup
        (K := E)).toAddSubgroup.map
          (rationalAbstractFixedFieldIdeleClassEquivFixed
            L.field).toAddMonoidHom).map
        (stableBaseConjugationHom
          rationalIdeleClassRepresentation L s) =
      (smallHilbertClassFieldNormSubgroup
        (K := E)).toAddSubgroup.map
          (rationalAbstractFixedFieldIdeleClassEquivFixed
            L.field).toAddMonoidHom := by
  dsimp only
  let E :=
    abstractFixedField ℚ (SeparableClosure ℚ) L.field
  let hLfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          L.field (le_baseField L.field)) :=
    (L.toFiniteGaloisExtension.toFiniteAbstractFieldExtension).field.finite
  let : FiniteDimensional ℚ E :=
    abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) L.field hLfinite
  let : NumberField E :=
    NumberField.of_module_finite ℚ E
  exact
    addSubgroup_map_eq_of_comp_eq_of_map_eq
      (smallHilbertClassFieldNormSubgroup (K := E)).toAddSubgroup
      (rationalAbstractFixedFieldIdeleClassEquivFixed
        L.field).toAddMonoidHom
      (MonoidHom.toAdditive
        (ideleClassCongr
          (smallHilbertBaseConjugationAutomorphism K L s)).toMonoidHom)
      (stableBaseConjugationHom
        rationalIdeleClassRepresentation L s)
      (rationalSmallHilbertFixedPart_conjugation_comp K L s)
      (smallHilbertClassFieldNormSubgroup_toAddSubgroup_map_ideleClassCongr
        E (smallHilbertBaseConjugationAutomorphism K L s))
theorem

smallHilbertNormSubgroupInRationalClassFormation_map_conjugation

L968 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertNormSubgroupInRationalClassFormation_map_conjugation
Documentation

The canonical small-Hilbert norm subgroup in the rational absolute class formation is fixed by every lower-base conjugation.

Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · statement
theorem smallHilbertNormSubgroupInRationalClassFormation_map_conjugation
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
    (s : K.field.toSubgroup) :
    (smallHilbertNormSubgroupInRationalClassFormation
        (L.toFiniteGaloisExtension.toFiniteAbstractFieldExtension).field).map
        (stableBaseConjugationHom
          rationalIdeleClassRepresentation L s) =
      smallHilbertNormSubgroupInRationalClassFormation
        (L.toFiniteGaloisExtension.toFiniteAbstractFieldExtension).field
theorem

smallHilbertClassField_conjugateSubextension_eq_self

L987 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassField_conjugateSubextension_eq_self
Documentation

If the upper extension realizes the canonical small-Hilbert norm subgroup of the middle field, finite abelian classification identifies its conjugate by every element of the lower base with the original finite abelian subextension.

Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · statement
theorem smallHilbertClassField_conjugateSubextension_eq_self
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
    (M : FiniteAbelianSubextension L.field)
    (hM :
      M.normSubgroup rationalIdeleClassRepresentation =
        smallHilbertNormSubgroupInRationalClassFormation
          (L.toFiniteGaloisExtension.toFiniteAbstractFieldExtension).field)
    (s : K.field.toSubgroup) :
    conjugateFiniteAbelianSubextensionOverBase L M s = M
theorem

smallHilbertClassField_conjugate_eq_self

L1031 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassField_conjugate_eq_self
Documentation

Field-level conjugation stability of the upper small Hilbert class field in the two-stage tower.

Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · statement
theorem smallHilbertClassField_conjugate_eq_self
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
    (M : FiniteAbelianSubextension L.field)
    (hM :
      M.normSubgroup rationalIdeleClassRepresentation =
        smallHilbertNormSubgroupInRationalClassFormation
          (L.toFiniteGaloisExtension.toFiniteAbstractFieldExtension).field)
    (s : K.field.toSubgroup) :
    conjugateClosedSubgroup M.field s.1 = M.field
def

smallHilbertClassFieldGaloisSubextension

L1055 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldGaloisSubextension
Documentation

The second small Hilbert class field in a finite abelian tower is an actual finite Galois extension of the original base.

Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · statement
def smallHilbertClassFieldGaloisSubextension
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
    (M : FiniteAbelianSubextension L.field)
    (hM :
      M.normSubgroup rationalIdeleClassRepresentation =
        smallHilbertNormSubgroupInRationalClassFormation
          (L.toFiniteGaloisExtension.toFiniteAbstractFieldExtension).field) :
    FiniteGaloisSubextension K.field
theorem

smallHilbertTowerBase_le_maximalAbelianSubextension

L1071 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerBase_le_maximalAbelianSubextension
Documentation

The abelian middle field of the two-stage small-Hilbert tower is contained in the maximal abelian intermediate field of the resulting Galois extension over the original base.

Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · statement
theorem smallHilbertTowerBase_le_maximalAbelianSubextension
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
    (M : FiniteAbelianSubextension L.field)
    (hM :
      M.normSubgroup rationalIdeleClassRepresentation =
        smallHilbertNormSubgroupInRationalClassFormation
          (L.toFiniteGaloisExtension.toFiniteAbstractFieldExtension).field) :
    L ≤
      maximalAbelianSubextension
        (smallHilbertClassFieldGaloisSubextension
          K L M hM)
theorem

maximalAbelianSubextension_le_smallHilbertClassField_of_everywhereUnramified

L1098 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.maximalAbelianSubextension_le_smallHilbertClassField_of_everywhereUnramified
Documentation

If an actual finite Galois extension is everywhere unramified over its base fixed field, then its maximal abelian intermediate field lies in every realization of the small Hilbert class field. Unramifiedness is first descended to the genuine commutator-fixed intermediate field; finite abelian classification then gives the field inclusion.

Source context 16 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
open GlobalClassFields LocalClassFieldTheory Reciprocity
section RationalSmallHilbert
local instance smallHilbertTowerBaseQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
local instance smallHilbertTowerRelativeQuotientFinite
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field L.field L.below) :=
  L.finite
noncomputable local instance smallHilbertTowerBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance smallHilbertTowerRelativeFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below K.finite L.finite
local instance smallHilbertTowerScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
noncomputable local instance smallHilbertTowerAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  FiniteDimensional.trans ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
noncomputable local instance smallHilbertTowerRelativeNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  NumberField.of_module_finite ℚ
    (abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below)
noncomputable local instance smallHilbertTowerRelativeIsGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
      (abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below) :=
  abstractRelativeFixedField_isGalois
    ℚ (SeparableClosure ℚ)
    K.field L.field L.below L.normal
Lean source · full declaration
theorem
    maximalAbelianSubextension_le_smallHilbertClassField_of_everywhereUnramified
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
    (P : FiniteGaloisSubextension K.field)
    (hL :
      L.normSubgroup rationalIdeleClassRepresentation =
        smallHilbertNormSubgroupInRationalClassFormation K) :
    let F :=
      abstractFixedField ℚ (SeparableClosure ℚ) K.field
    let T :=
      abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below
    letI hKfinite : Finite
        ((baseField
          (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
          CyclicCohomology.extensionSubgroup
            (baseField
              (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
            K.field (le_baseField K.field)) :=
      K.finite
    letI hPfinite : Finite
        (K.field.toSubgroup ⧸
          CyclicCohomology.extensionSubgroup
            K.field P.field P.below) :=
      P.finite
    letI : FiniteDimensional ℚ F :=
      abstractFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) K.field hKfinite
    letI : FiniteDimensional F T :=
      abstractRelativeFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ)
        K.field P.field P.below hKfinite hPfinite
    letI : IsScalarTower ℚ F T :=
      IsScalarTower.of_algebraMap_eq' rfl
    letI : FiniteDimensional ℚ T :=
      FiniteDimensional.trans ℚ F T
    letI : NumberField F :=
      NumberField.of_module_finite ℚ F
    letI : NumberField T :=
      NumberField.of_module_finite ℚ T
    IsEverywhereUnramified F T →
      maximalAbelianSubextension P ≤ L := by
  classical
  dsimp only
  let F :=
    abstractFixedField ℚ (SeparableClosure ℚ) K.field
  let T :=
    abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P.below
  let A :=
    maximalAbelianSubextension P
  let E :=
    abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) A.below
  let hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
    K.finite
  let hPfinite : Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field P.field P.below) :=
    P.finite
  let hAfinite : Finite
      (K.field.toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          K.field A.field A.below) :=
    A.finite
  let : FiniteDimensional ℚ F :=
    abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) K.field hKfinite
  let : FiniteDimensional F T :=
    abstractRelativeFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ)
      K.field P.field P.below hKfinite hPfinite
  let : IsScalarTower ℚ F T :=
    IsScalarTower.of_algebraMap_eq' rfl
  let : FiniteDimensional ℚ T :=
    FiniteDimensional.trans ℚ F T
  let : FiniteDimensional F E :=
    abstractRelativeFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ)
      K.field A.field A.below hKfinite hAfinite
  let : IsScalarTower ℚ F E :=
    IsScalarTower.of_algebraMap_eq' rfl
  let : FiniteDimensional ℚ E :=
    FiniteDimensional.trans ℚ F E
  let : NumberField F :=
    NumberField.of_module_finite ℚ F
  let : NumberField T :=
    NumberField.of_module_finite ℚ T
  let : NumberField E :=
    NumberField.of_module_finite ℚ E
  intro hunramifiedTop
  have hPA :
      P.field.toSubgroup ≤ A.field.toSubgroup := by
    change
      P.field.toSubgroup ≤
        P.abelianIntermediateField.toSubgroup
    exact
      P.field_le_intermediateField
        (commutator P.extensionQuotient)
  have hET : E ≤ T := by
    intro x hx
    change
      x ∈ abstractFixedField
        ℚ (SeparableClosure ℚ) A.field at hx
    change
      x ∈ abstractFixedField
        ℚ (SeparableClosure ℚ) P.field
    exact
      (abstractFixedField_le
        ℚ (SeparableClosure ℚ) hPA) hx
  let : Algebra E T :=
    (IntermediateField.inclusion hET).toRingHom.toAlgebra
  let : IsScalarTower F E T :=
    IsScalarTower.of_algebraMap_eq' rfl
  have hunramifiedAbelian :
      IsEverywhereUnramified F E :=
    IsEverywhereUnramified.bot hunramifiedTop
  exact
    everywhereUnramifiedFiniteAbelianSubextension_le_smallHilbertClassField
      K L A hL hunramifiedAbelian

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