Module

IdeleClassDirectLimitNormQuotient.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.IdeleClassDirectLimitNormQuotient

30 declarations indexed from sourceView source ↗

Module documentation

Finite norm quotients for rational fixed fields

The abstract finite norm subgroup and quotient are identified with the ordinary idele-class norm range and quotient of the actual fixed-field extension.

Imports2

Imported by6

instance

rationalNormQuotientIdeleClassGroupIsMulCommutative

L28 ↗

GlobalClassFieldTheory.Reciprocity.rationalNormQuotientIdeleClassGroupIsMulCommutative

Source context 6 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology

Lean source · statement

instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

instance

rationalNormQuotientIdeleClassSubgroupNormal

L34 ↗

GlobalClassFieldTheory.Reciprocity.rationalNormQuotientIdeleClassSubgroupNormal

Source context 7 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal

def

rationalNormQuotientIdeleClassCommGroup

L41 ↗

GlobalClassFieldTheory.Reciprocity.rationalNormQuotientIdeleClassCommGroup

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

def rationalNormQuotientIdeleClassCommGroup
    (F : Type) [Field F] [NumberField F] :
    CommGroup (IdeleClassGroup F)

theorem

rationalNormQuotientNumberFieldOfFiniteDimensional

L47 ↗

GlobalClassFieldTheory.Reciprocity.rationalNormQuotientNumberFieldOfFiniteDimensional

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem rationalNormQuotientNumberFieldOfFiniteDimensional
    (F : Type*) [Field F] [Algebra ℚ F] [FiniteDimensional ℚ F] :
    NumberField F

theorem

rationalNormQuotientAbstractFixedFieldNumberField

L52 ↗

GlobalClassFieldTheory.Reciprocity.rationalNormQuotientAbstractFixedFieldNumberField

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem rationalNormQuotientAbstractFixedFieldNumberField
    (K : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))] :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K)

theorem

rationalNormQuotientAbstractRelativeFixedFieldNumberField

L72 ↗

GlobalClassFieldTheory.Reciprocity.rationalNormQuotientAbstractRelativeFixedFieldNumberField

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem rationalNormQuotientAbstractRelativeFixedFieldNumberField
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)] :
    NumberField
      (abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK)

theorem

addEquiv_trans_symm_trans_symm_trans_apply_eq

L100 ↗

GlobalClassFieldTheory.Reciprocity.addEquiv_trans_symm_trans_symm_trans_apply_eq

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem addEquiv_trans_symm_trans_symm_trans_apply_eq
    {V A B C D : Type*}
    [Add V] [Add A] [Add B] [Add C] [Add D]
    (eV : V ≃+ D) (eB : B ≃+ D)
    (eA : A ≃+ B) (eC : A ≃+ C)
    {y : V} {z : A} {w : C}
    (h : eV y = eB (eA z))
    (ht : eC z = w) :
    (((eV.trans eB.symm).trans eA.symm).trans eC) y = w

theorem

rationalTowerRelativeClass_baseChange

L113 ↗

GlobalClassFieldTheory.Reciprocity.rationalTowerRelativeClass_baseChange

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem rationalTowerRelativeClass_baseChange
    (F E : Type)
    [Field F] [NumberField F]
    [Field E] [NumberField E]
    [Algebra ℚ F] [Algebra F E] [Algebra ℚ E]
    [IsScalarTower ℚ F E]
    [FiniteDimensional ℚ F] [FiniteDimensional F E]
    (c : Additive (IdeleClassGroup E)) :
    _root_.relativeIdeleClassBaseChangeMulEquiv
        (K := F) (L := E)
        (towerRelativeIdeleClassBaseChangeMulEquiv ℚ F E
          ((TowerRelativeIdeleGroup.classGroupEquiv
            ℚ F E).symm
            ((_root_.relativeIdeleClassBaseChangeMulEquiv
              (K := ℚ) (L := E)).symm (Additive.toMul c)))) =
      Additive.toMul c

theorem

rationalTowerRelativeClass_norm

L139 ↗

GlobalClassFieldTheory.Reciprocity.rationalTowerRelativeClass_norm

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · full declaration

theorem rationalTowerRelativeClass_norm
    (F E : Type)
    [Field F] [NumberField F]
    [Field E] [NumberField E]
    [Algebra ℚ F] [Algebra F E] [Algebra ℚ E]
    [IsScalarTower ℚ F E]
    [FiniteDimensional ℚ F] [FiniteDimensional F E]
    [IsGalois F E]
    (c : Additive (IdeleClassGroup E)) :
    let dF :=
      towerRelativeIdeleClassBaseChangeMulEquiv ℚ F E
        ((TowerRelativeIdeleGroup.classGroupEquiv
          ℚ F E).symm
          ((_root_.relativeIdeleClassBaseChangeMulEquiv
            (K := ℚ) (L := E)).symm (Additive.toMul c)))
    RelativeIdeleGroup.Cohomology.ideleClassNorm F E dF =
      _root_.ideleClassNorm F E (Additive.toMul c) := by
  let dF :=
    towerRelativeIdeleClassBaseChangeMulEquiv ℚ F E
      ((TowerRelativeIdeleGroup.classGroupEquiv
        ℚ F E).symm
        ((_root_.relativeIdeleClassBaseChangeMulEquiv
          (K := ℚ) (L := E)).symm (Additive.toMul c)))
  have hbase := rationalTowerRelativeClass_baseChange F E c
  change
    _root_.relativeIdeleClassBaseChangeMulEquiv
        (K := F) (L := E) dF = Additive.toMul c at hbase
  exact
    (ordinaryIdeleClassNorm_relativeIdeleClassBaseChange dF).symm.trans
      (congrArg (_root_.ideleClassNorm F E) hbase)

abbrev

rationalRelativeFixedFieldIdeleClassAdditiveType

L170 ↗

GlobalClassFieldTheory.Reciprocity.rationalRelativeFixedFieldIdeleClassAdditiveType

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

abbrev rationalRelativeFixedFieldIdeleClassAdditiveType
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)] : Type

abbrev

rationalOrdinaryNormQuotientAdditiveType

L198 ↗

GlobalClassFieldTheory.Reciprocity.rationalOrdinaryNormQuotientAdditiveType

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

abbrev rationalOrdinaryNormQuotientAdditiveType
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)] : Type

instance

rationalOrdinaryNormQuotientAdditiveTypeAddCommGroup

L233 ↗

GlobalClassFieldTheory.Reciprocity.rationalOrdinaryNormQuotientAdditiveTypeAddCommGroup

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

instance
    rationalOrdinaryNormQuotientAdditiveTypeAddCommGroup
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)] :
    AddCommGroup
      (rationalOrdinaryNormQuotientAdditiveType
        K L hLK hnormal)

def

quotientAddEquivOfEquivMapEq_mk

L324 ↗

GlobalClassFieldTheory.Reciprocity.quotientAddEquivOfEquivMapEq_mk

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem quotientAddEquivOfEquivMapEq_mk
    {A B : Type*} [AddCommGroup A] [AddCommGroup B]
    (S : AddSubgroup A) (T : AddSubgroup B)
    (e : B ≃+ A)
    (hmap : S.map e.symm.toAddMonoidHom = T)
    (x : A) :
    quotientAddEquivOfEquivMapEq S T e hmap
        (QuotientAddGroup.mk' S x) =
      QuotientAddGroup.mk' T (e.symm x)

def

quotientAddEquivOfEquivMapEqToQuotient

L383 ↗

GlobalClassFieldTheory.Reciprocity.quotientAddEquivOfEquivMapEqToQuotient

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

def quotientAddEquivOfEquivMapEqToQuotient
    {A G : Type*} [AddCommGroup A] [CommGroup G]
    (S : AddSubgroup A) (N : Subgroup G) [N.Normal]
    (e : Additive G ≃+ A)
    (hmap : S.map e.symm.toAddMonoidHom = N.toAddSubgroup) :
    (A ⧸ S) ≃+ Additive (G ⧸ N)

def

addEquivTransQuotientOfEquivMapEq

L392 ↗

GlobalClassFieldTheory.Reciprocity.addEquivTransQuotientOfEquivMapEq

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

def addEquivTransQuotientOfEquivMapEq
    {Q A G : Type*}
    [AddCommGroup Q] [AddCommGroup A] [CommGroup G]
    (S : AddSubgroup A) (N : Subgroup G) [N.Normal]
    (eConcrete : Q ≃+ (A ⧸ S)) (e : Additive G ≃+ A)
    (hmap : S.map e.symm.toAddMonoidHom = N.toAddSubgroup) :
    Q ≃+ Additive (G ⧸ N)

theorem

map_addRange_eq_monoidRange_toAddSubgroup_of_equiv

L402 ↗

GlobalClassFieldTheory.Reciprocity.map_addRange_eq_monoidRange_toAddSubgroup_of_equiv

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem map_addRange_eq_monoidRange_toAddSubgroup_of_equiv
    {U A G H : Type*}
    [AddCommGroup U] [AddCommGroup A] [CommGroup G] [CommGroup H]
    (f : U →+ A) (g : G →* H)
    (eU : Additive G ≃+ U) (eA : Additive H ≃+ A)
    (hcompat : ∀ c : Additive G,
      eA.symm (f (eU c)) =
        Additive.ofMul (g (Additive.toMul c))) :
    f.range.map eA.symm.toAddMonoidHom = g.range.toAddSubgroup

def

rationalAbstractRelativeFixedFieldIdeleClassEquivFixed

L436 ↗

GlobalClassFieldTheory.Reciprocity.rationalAbstractRelativeFixedFieldIdeleClassEquivFixed

Documentation

The ordinary idele class group of the upper fixed field, identified directly with the corresponding fixed part of the rational absolute idele-class representation. Unlike rationalAbstractExtensionIdeleClassEquiv, this comparison does not package a Galois action and therefore does not require normality.

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

def
    rationalAbstractRelativeFixedFieldIdeleClassEquivFixed
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)] :
    rationalRelativeFixedFieldIdeleClassAdditiveType
        (hKfinite := hKfinite) (hfinite := hfinite)
        K L hLK ≃+
      KummerTheory.ambientFixedAddSubgroup
        rationalIdeleClassRepresentation L

def

rationalRelativeFixedFieldNormComparison

L478 ↗

GlobalClassFieldTheory.Reciprocity.rationalRelativeFixedFieldNormComparison

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

def rationalRelativeFixedFieldNormComparison
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (c : rationalRelativeFixedFieldIdeleClassAdditiveType
      (hKfinite := hKfinite) (hfinite := hfinite)
      K L hLK) :
    (KummerTheory.ambientFixedAddSubgroup
      rationalIdeleClassRepresentation K) ×
        KummerTheory.ambientFixedAddSubgroup
          rationalIdeleClassRepresentation K

def

rationalRelativeFixedFieldNormPreimageComparison

L522 ↗

GlobalClassFieldTheory.Reciprocity.rationalRelativeFixedFieldNormPreimageComparison

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

def rationalRelativeFixedFieldNormPreimageComparison
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (c : rationalRelativeFixedFieldIdeleClassAdditiveType
      (hKfinite := hKfinite) (hfinite := hfinite)
      K L hLK)

theorem

rationalRelativeFixedFieldNormPreimageComparison_eq

L566 ↗

GlobalClassFieldTheory.Reciprocity.rationalRelativeFixedFieldNormPreimageComparison_eq

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem rationalRelativeFixedFieldNormPreimageComparison_eq
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (c : rationalRelativeFixedFieldIdeleClassAdditiveType
      (hKfinite := hKfinite) (hfinite := hfinite)
      K L hLK) :
    (rationalRelativeFixedFieldNormPreimageComparison K L hLK hnormal c).1 =
    (rationalRelativeFixedFieldNormPreimageComparison K L hLK hnormal c).2

def

rationalRelativeFixedFieldNormCohomologyComparison

L641 ↗

GlobalClassFieldTheory.Reciprocity.rationalRelativeFixedFieldNormCohomologyComparison

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

def rationalRelativeFixedFieldNormCohomologyComparison
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (c : rationalRelativeFixedFieldIdeleClassAdditiveType
      (hKfinite := hKfinite) (hfinite := hfinite)
      K L hLK)

theorem

rationalRelativeFixedFieldNormCohomologyComparison_eq

L687 ↗

GlobalClassFieldTheory.Reciprocity.rationalRelativeFixedFieldNormCohomologyComparison_eq

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem rationalRelativeFixedFieldNormCohomologyComparison_eq
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (c : rationalRelativeFixedFieldIdeleClassAdditiveType
      (hKfinite := hKfinite) (hfinite := hfinite)
      K L hLK) :
    (rationalRelativeFixedFieldNormCohomologyComparison
      K L hLK hnormal c).1 =
      (rationalRelativeFixedFieldNormCohomologyComparison
        K L hLK hnormal c).2

theorem

rationalAbstractRelativeFixedFieldIdeleClassEquivFixed_relativeNorm

L757 ↗

GlobalClassFieldTheory.Reciprocity.rationalAbstractRelativeFixedFieldIdeleClassEquivFixed_relativeNorm

Documentation

For a finite Galois pair of abstract fixed fields, the direct upper fixed-part comparison intertwines the class-formation relative norm with the ordinary idele-class norm.

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · full declaration

theorem
    rationalAbstractRelativeFixedFieldIdeleClassEquivFixed_relativeNorm
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (c : rationalRelativeFixedFieldIdeleClassAdditiveType
      (hKfinite := hKfinite) (hfinite := hfinite)
      K L hLK) :
    let comparison := rationalRelativeFixedFieldNormComparison
      (hKfinite := hKfinite) (hfinite := hfinite) K L hLK hnormal c
    comparison.1 = comparison.2 := by
  let _ := hnormal
  let F :=
    abstractFixedField ℚ (SeparableClosure ℚ) K
  let E :=
    abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
  let _ : FiniteDimensional ℚ F :=
    abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) K hKfinite
  let _ : FiniteDimensional F E :=
    abstractRelativeFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
  let _ : IsScalarTower ℚ F E :=
    IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
  let _ : FiniteDimensional ℚ E :=
    FiniteDimensional.trans ℚ F E
  let _ : NumberField F :=
    NumberField.of_module_finite ℚ F
  let _ : NumberField E :=
    NumberField.of_module_finite ℚ E
  let _ : IsGalois F E :=
    abstractRelativeFixedField_isGalois
      ℚ (SeparableClosure ℚ) K L hLK hnormal
  change
    relativeNorm rationalIdeleClassRepresentation K L hLK
        (rationalAbstractRelativeFixedFieldIdeleClassEquivFixed
          K L hLK c) =
      rationalAbstractFixedFieldIdeleClassEquivFixed K
        (Additive.ofMul
          (_root_.ideleClassNorm F E (Additive.toMul c)))
  let eUpper :=
    rationalAbstractRelativeFixedFieldIdeleClassEquivFixed
      K L hLK
  let comparison :=
    rationalRelativeFixedFieldNormPreimageComparison
      K L hLK hnormal c
  let dF : RelativeIdeleGroup.ClassGroup F E :=
    Additive.toMul comparison.2
  have hcohom :=
    rationalRelativeFixedFieldNormCohomologyComparison_eq
      K L hLK hnormal c
  change
    (rationalAbstractFixedFieldIdeleClassEquivFixed K).symm
        (relativeNorm rationalIdeleClassRepresentation
          K L hLK (eUpper c)) =
      Additive.ofMul
        (RelativeIdeleGroup.Cohomology.ideleClassNorm F E
          dF)
    at hcohom
  have hbridge := rationalTowerRelativeClass_norm F E c
  change
    RelativeIdeleGroup.Cohomology.ideleClassNorm F E dF =
      _root_.ideleClassNorm F E (Additive.toMul c) at hbridge
  calc
    relativeNorm rationalIdeleClassRepresentation K L hLK (eUpper c) =
        rationalAbstractFixedFieldIdeleClassEquivFixed K
          ((rationalAbstractFixedFieldIdeleClassEquivFixed K).symm
            (relativeNorm rationalIdeleClassRepresentation
              K L hLK (eUpper c))) :=
      ((rationalAbstractFixedFieldIdeleClassEquivFixed K).apply_symm_apply _).symm
    _ = rationalAbstractFixedFieldIdeleClassEquivFixed K
          (Additive.ofMul
            (_root_.ideleClassNorm F E (Additive.toMul c))) :=
      congrArg (rationalAbstractFixedFieldIdeleClassEquivFixed K)
        (hcohom.trans (congrArg Additive.ofMul hbridge))

theorem

map_rationalFiniteNormSubgroup_eq_ordinaryIdeleClassNormRange_concrete

L845 ↗

GlobalClassFieldTheory.Reciprocity.map_rationalFiniteNormSubgroup_eq_ordinaryIdeleClassNormRange_concrete

Documentation

The fixed-field comparison carries the abstract finite norm subgroup exactly to the ordinary idele-class norm range of the actual fixed fields.

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · full declaration

theorem
    map_rationalFiniteNormSubgroup_eq_ordinaryIdeleClassNormRange_concrete
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)] :
    let F := abstractFixedField ℚ (SeparableClosure ℚ) K
    let E := abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
    letI := hnormal
    letI : FiniteDimensional ℚ F :=
      abstractFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) K hKfinite
    letI : FiniteDimensional F E :=
      abstractRelativeFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
    letI : IsScalarTower ℚ F E :=
      IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
    letI : FiniteDimensional ℚ E :=
      FiniteDimensional.trans ℚ F E
    letI : NumberField F := NumberField.of_module_finite ℚ F
    letI : NumberField E := NumberField.of_module_finite ℚ E
    letI : IsGalois F E :=
      abstractRelativeFixedField_isGalois
        ℚ (SeparableClosure ℚ) K L hLK hnormal
    (finiteNormSubgroup rationalIdeleClassRepresentation K L hLK).map
        (rationalAbstractFixedFieldIdeleClassEquivFixed
          K).symm.toAddMonoidHom =
      (_root_.ideleClassNorm F E).range.toAddSubgroup := by
  let F := abstractFixedField ℚ (SeparableClosure ℚ) K
  let E := abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK
  let _ := hnormal
  let _ : FiniteDimensional ℚ F :=
    abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) K hKfinite
  let _ : FiniteDimensional F E :=
    abstractRelativeFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
  let _ : IsScalarTower ℚ F E :=
    IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
  let _ : FiniteDimensional ℚ E := FiniteDimensional.trans ℚ F E
  let _ : NumberField F := NumberField.of_module_finite ℚ F
  let _ : NumberField E := NumberField.of_module_finite ℚ E
  let _ : IsGalois F E :=
    abstractRelativeFixedField_isGalois
      ℚ (SeparableClosure ℚ) K L hLK hnormal
  let _ : CommGroup (IdeleClassGroup F) :=
    rationalNormQuotientIdeleClassCommGroup F
  let _ : CommGroup (IdeleClassGroup E) :=
    rationalNormQuotientIdeleClassCommGroup E
  let eK : Additive (IdeleClassGroup F) ≃+
      KummerTheory.ambientFixedAddSubgroup
        rationalIdeleClassRepresentation K :=
    rationalAbstractFixedFieldIdeleClassEquivFixed
      (hfinite := hKfinite) K
  let eUpper : Additive (IdeleClassGroup E) ≃+
      KummerTheory.ambientFixedAddSubgroup
        rationalIdeleClassRepresentation L :=
    rationalAbstractRelativeFixedFieldIdeleClassEquivFixed
      (hKfinite := hKfinite) (hfinite := hfinite) K L hLK
  let f :
      KummerTheory.ambientFixedAddSubgroup
          rationalIdeleClassRepresentation L →+
        KummerTheory.ambientFixedAddSubgroup
          rationalIdeleClassRepresentation K :=
    relativeNorm rationalIdeleClassRepresentation K L hLK
  let g : IdeleClassGroup E →* IdeleClassGroup F :=
    _root_.ideleClassNorm F E
  change f.range.map eK.symm.toAddMonoidHom = g.range.toAddSubgroup
  refine map_addRange_eq_monoidRange_toAddSubgroup_of_equiv
    (U := KummerTheory.ambientFixedAddSubgroup
      rationalIdeleClassRepresentation L)
    (A := KummerTheory.ambientFixedAddSubgroup
      rationalIdeleClassRepresentation K)
    (G := IdeleClassGroup E) (H := IdeleClassGroup F)
    (f := f) (g := g) (eU := eUpper) (eA := eK) ?_
  intro c
  have hcompat :
      f (eUpper c) = eK (Additive.ofMul (g (Additive.toMul c))) := by
    exact
      rationalAbstractRelativeFixedFieldIdeleClassEquivFixed_relativeNorm
        (hKfinite := hKfinite) (hfinite := hfinite) K L hLK hnormal c
  apply eK.injective
  exact Eq.trans (eK.apply_symm_apply (f (eUpper c))) hcompat

def

rationalFiniteNormQuotientConcreteStep

L938 ↗

GlobalClassFieldTheory.Reciprocity.rationalFiniteNormQuotientConcreteStep

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

def rationalFiniteNormQuotientConcreteStep
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)] :
    FiniteNormQuotient rationalIdeleClassRepresentation K L hLK ≃+
      KummerTheory.ambientFixedAddSubgroup
          rationalIdeleClassRepresentation K ⧸
        finiteNormSubgroup rationalIdeleClassRepresentation K L hLK

def

rationalFiniteNormQuotientEquivIdeleClassNormQuotient

L954 ↗

GlobalClassFieldTheory.Reciprocity.rationalFiniteNormQuotientEquivIdeleClassNormQuotient

Documentation

The finite norm quotient in the rational absolute representation is the ordinary idele-class quotient by the actual norm subgroup of the fixed-field extension.

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

def
    rationalFiniteNormQuotientEquivIdeleClassNormQuotient
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)] :
    FiniteNormQuotient rationalIdeleClassRepresentation K L hLK ≃+
      rationalOrdinaryNormQuotientAdditiveType K L hLK hnormal

def

rationalFiniteNormQuotientClassValue

L1038 ↗

GlobalClassFieldTheory.Reciprocity.rationalFiniteNormQuotientClassValue

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

def rationalFiniteNormQuotientClassValue
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (a : KummerTheory.ambientFixedAddSubgroup
      rationalIdeleClassRepresentation K) :
    rationalOrdinaryNormQuotientAdditiveType
      (hKfinite := hKfinite) (hfinite := hfinite)
      K L hLK hnormal

theorem

rationalFiniteNormQuotientEquivIdeleClassNormQuotient_finiteNormClass

L1084 ↗

GlobalClassFieldTheory.Reciprocity.rationalFiniteNormQuotientEquivIdeleClassNormQuotient_finiteNormClass

Documentation

The fixed-field norm-quotient comparison sends an abstract finite norm class to the ordinary idele class of the transported representative.

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
local instance
    rationalNormQuotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    rationalNormQuotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem
    rationalFiniteNormQuotientEquivIdeleClassNormQuotient_finiteNormClass
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (a : KummerTheory.ambientFixedAddSubgroup
      rationalIdeleClassRepresentation K) :
    rationalFiniteNormQuotientEquivIdeleClassNormQuotient
        K L hLK hnormal
        (finiteNormClass rationalIdeleClassRepresentation
          K L hLK a) =
      rationalFiniteNormQuotientClassValue
        (hKfinite := hKfinite) (hfinite := hfinite)
        K L hLK hnormal a

Module documentation

Finite norm quotients for rational fixed fields

Declarations