Module

NumberFieldComplexification.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ComplexificationArtin.NumberFieldComplexification

35 declarations indexed from sourceView source ↗

Module documentation

Complexification of a number field

This module forms the actual compositum with the rational fourth-root field and proves that restriction to the rational cyclotomic factor is faithful.

Imports3

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ComplexificationArtin.RationalComplexification
Nyll.ClassFieldTheory.AlgebraicNumberTheory.SeparableClosureEmbedding
Mathlib.FieldTheory.Galois.Abelian

Imported by2

def

rationalComplexificationAmbientField

L31 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationAmbientField

Source context 6 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois

Lean source · statement

def rationalComplexificationAmbientField :
    IntermediateField ℚ (SeparableClosure ℚ)

def

rationalComplexificationAmbientEquiv

L37 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationAmbientEquiv

Source context 6 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois

Lean source · statement

def rationalComplexificationAmbientEquiv :
    rationalComplexificationCyclotomicField ≃ₐ[ℚ]
      rationalComplexificationAmbientField

def

numberFieldComplexification

L49 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexification

Documentation

The actual compositum of the chosen copy of F with the rational complexification field inside SeparableClosure ℚ.

Source context 7 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]

Lean source · statement

def numberFieldComplexification :
    IntermediateField ℚ (SeparableClosure ℚ)

instance

numberFieldComplexificationRationalAlgebra

L55 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationRationalAlgebra

Source context 7 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]

Lean source · statement

instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F)

instance

numberFieldComplexification_finiteDimensional

L60 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexification_finiteDimensional

Source context 8 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'

Lean source · statement

instance numberFieldComplexification_finiteDimensional :
    FiniteDimensional ℚ (numberFieldComplexification F)

instance

numberFieldComplexification_numberField

L71 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexification_numberField

Source context 8 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'

Lean source · statement

instance numberFieldComplexification_numberField :
    NumberField (numberFieldComplexification F)

def

numberFieldComplexificationEmbedding

L76 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationEmbedding

Documentation

The chosen embedding of F into its actual complexification.

Source context 8 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'

Lean source · statement

def numberFieldComplexificationEmbedding :
    F →ₐ[ℚ] numberFieldComplexification F

def

rationalComplexificationCompositumEmbedding

L89 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationCompositumEmbedding

Documentation

The rational fourth-root cyclotomic field embedded into the complexification of F.

Source context 8 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'

Lean source · statement

def rationalComplexificationCompositumEmbedding :
    rationalComplexificationCyclotomicField →ₐ[ℚ]
      numberFieldComplexification F

instance

numberFieldComplexification_algebra

L95 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexification_algebra

Source context 8 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'

Lean source · statement

instance numberFieldComplexification_algebra :
    Algebra F (numberFieldComplexification F)

instance

numberFieldComplexification_smul

L102 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexification_smul

Documentation

The scalar action belonging to the chosen embedding of F into its complexification. Naming it prevents typeclass search from finding a definitionally different action through the ambient intermediate field.

Source context 8 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'

Lean source · statement

instance numberFieldComplexification_smul :
    SMul F (numberFieldComplexification F)

instance

rationalComplexificationCompositum_algebra

L106 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationCompositum_algebra

Source context 8 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'

Lean source · statement

instance rationalComplexificationCompositum_algebra :
    Algebra rationalComplexificationCyclotomicField
      (numberFieldComplexification F)

instance

rationalComplexificationCompositum_smul

L114 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationCompositum_smul

Documentation

The scalar action induced by the actual fourth-root-field embedding. Declaring it directly prevents instance search from exploring unrelated intermediate-field algebra structures.

Source context 8 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'

Lean source · statement

instance rationalComplexificationCompositum_smul :
    SMul rationalComplexificationCyclotomicField
      (numberFieldComplexification F)

instance

numberFieldComplexification_scalarTower

L119 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexification_scalarTower

Source context 8 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'

Lean source · statement

instance numberFieldComplexification_scalarTower :
    IsScalarTower ℚ F (numberFieldComplexification F)

instance

rationalComplexificationCompositum_scalarTower

L124 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationCompositum_scalarTower

Source context 8 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'

Lean source · statement

instance rationalComplexificationCompositum_scalarTower :
    IsScalarTower ℚ rationalComplexificationCyclotomicField
      (numberFieldComplexification F)

instance

numberFieldComplexification_finiteDimensional_over_base

L130 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexification_finiteDimensional_over_base

Source context 8 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'

Lean source · statement

instance
    numberFieldComplexification_finiteDimensional_over_base :
    FiniteDimensional F (numberFieldComplexification F)

def

numberFieldComplexificationRestriction

L137 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationRestriction

Documentation

Restriction from F(μ₄)/F to the rational fourth-root cyclotomic factor.

Source context 8 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'

Lean source · statement

def numberFieldComplexificationRestriction :
    Gal(numberFieldComplexification F / F) →*
      Gal(rationalComplexificationCyclotomicField / ℚ)

def

numberFieldComplexificationBaseLayer

L144 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationBaseLayer

Source context 8 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'

Lean source · statement

def numberFieldComplexificationBaseLayer :
    IntermediateField ℚ (numberFieldComplexification F)

def

numberFieldComplexificationCyclotomicLayer

L151 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationCyclotomicLayer

Source context 8 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'

Lean source · statement

def numberFieldComplexificationCyclotomicLayer :
    IntermediateField ℚ (numberFieldComplexification F)

instance

numberFieldComplexificationBaseLayerRationalAlgebra

L160 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationBaseLayerRationalAlgebra

Source context 8 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'

Lean source · statement

instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F)

instance

numberFieldComplexificationCyclotomicLayerRationalAlgebra

L166 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationCyclotomicLayerRationalAlgebra

Source context 9 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F) :=
  (numberFieldComplexificationBaseLayer F).algebra'

Lean source · statement

instance
    numberFieldComplexificationCyclotomicLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationCyclotomicLayer F)

def

numberFieldComplexificationBaseEquiv

L171 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationBaseEquiv

Source context 10 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F) :=
  (numberFieldComplexificationBaseLayer F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationCyclotomicLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer F).algebra'

Lean source · statement

def numberFieldComplexificationBaseEquiv :
    F ≃ₐ[ℚ] numberFieldComplexificationBaseLayer F

def

numberFieldComplexificationCyclotomicEquiv

L176 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationCyclotomicEquiv

Source context 10 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F) :=
  (numberFieldComplexificationBaseLayer F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationCyclotomicLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer F).algebra'

Lean source · statement

def numberFieldComplexificationCyclotomicEquiv :
    rationalComplexificationCyclotomicField ≃ₐ[ℚ]
      numberFieldComplexificationCyclotomicLayer F

instance

numberFieldComplexificationCyclotomicLayer_isAbelianGalois

L182 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationCyclotomicLayer_isAbelianGalois

Source context 10 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F) :=
  (numberFieldComplexificationBaseLayer F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationCyclotomicLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer F).algebra'

Lean source · statement

instance
    numberFieldComplexificationCyclotomicLayer_isAbelianGalois :
    IsAbelianGalois ℚ
      (numberFieldComplexificationCyclotomicLayer F)

instance

numberFieldComplexificationCyclotomicLayer_isGalois

L189 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationCyclotomicLayer_isGalois

Source context 11 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F) :=
  (numberFieldComplexificationBaseLayer F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationCyclotomicLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer F).algebra'
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isAbelianGalois :
    IsAbelianGalois ℚ
      (numberFieldComplexificationCyclotomicLayer F) :=
  IsAbelianGalois.of_algHom
    (numberFieldComplexificationCyclotomicEquiv F).symm.toAlgHom

Lean source · statement

instance
    numberFieldComplexificationCyclotomicLayer_isGalois :
    IsGalois ℚ (numberFieldComplexificationCyclotomicLayer F)

instance

numberFieldComplexificationCyclotomicLayer_normal

L195 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationCyclotomicLayer_normal

Source context 12 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F) :=
  (numberFieldComplexificationBaseLayer F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationCyclotomicLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer F).algebra'
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isAbelianGalois :
    IsAbelianGalois ℚ
      (numberFieldComplexificationCyclotomicLayer F) :=
  IsAbelianGalois.of_algHom
    (numberFieldComplexificationCyclotomicEquiv F).symm.toAlgHom
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isGalois :
    IsGalois ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isAbelianGalois
    F).toIsGalois

Lean source · statement

instance
    numberFieldComplexificationCyclotomicLayer_normal :
    Normal ℚ (numberFieldComplexificationCyclotomicLayer F)

theorem

numberFieldComplexificationLayers_sup

L201 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationLayers_sup

Source context 13 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F) :=
  (numberFieldComplexificationBaseLayer F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationCyclotomicLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer F).algebra'
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isAbelianGalois :
    IsAbelianGalois ℚ
      (numberFieldComplexificationCyclotomicLayer F) :=
  IsAbelianGalois.of_algHom
    (numberFieldComplexificationCyclotomicEquiv F).symm.toAlgHom
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isGalois :
    IsGalois ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isAbelianGalois
    F).toIsGalois
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_normal :
    Normal ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isGalois
    F).to_normal

Lean source · statement

theorem numberFieldComplexificationLayers_sup :
    numberFieldComplexificationCyclotomicLayer F ⊔
        numberFieldComplexificationBaseLayer F =
      ⊤

theorem

numberFieldComplexificationBaseEquiv_algebraMap

L215 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationBaseEquiv_algebraMap

Source context 13 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F) :=
  (numberFieldComplexificationBaseLayer F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationCyclotomicLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer F).algebra'
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isAbelianGalois :
    IsAbelianGalois ℚ
      (numberFieldComplexificationCyclotomicLayer F) :=
  IsAbelianGalois.of_algHom
    (numberFieldComplexificationCyclotomicEquiv F).symm.toAlgHom
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isGalois :
    IsGalois ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isAbelianGalois
    F).toIsGalois
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_normal :
    Normal ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isGalois
    F).to_normal

Lean source · statement

theorem numberFieldComplexificationBaseEquiv_algebraMap
    (x : F) :
    algebraMap F (numberFieldComplexification F) x =
      algebraMap (numberFieldComplexificationBaseLayer F)
        (numberFieldComplexification F)
        (numberFieldComplexificationBaseEquiv F x)

def

numberFieldComplexificationChangeBase

L224 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationChangeBase

Source context 13 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F) :=
  (numberFieldComplexificationBaseLayer F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationCyclotomicLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer F).algebra'
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isAbelianGalois :
    IsAbelianGalois ℚ
      (numberFieldComplexificationCyclotomicLayer F) :=
  IsAbelianGalois.of_algHom
    (numberFieldComplexificationCyclotomicEquiv F).symm.toAlgHom
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isGalois :
    IsGalois ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isAbelianGalois
    F).toIsGalois
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_normal :
    Normal ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isGalois
    F).to_normal

Lean source · full declaration

def numberFieldComplexificationChangeBase :
    Gal(numberFieldComplexification F / F) →*
      Gal(numberFieldComplexification F /
        numberFieldComplexificationBaseLayer F) where
  toFun σ :=
    { σ.toRingEquiv with
      commutes' := by
        intro y
        have hy :
            algebraMap F (numberFieldComplexification F)
                ((numberFieldComplexificationBaseEquiv F).symm y) =
              algebraMap (numberFieldComplexificationBaseLayer F)
                (numberFieldComplexification F) y := by
          have hy' :=
            numberFieldComplexificationBaseEquiv_algebraMap F
              ((numberFieldComplexificationBaseEquiv F).symm y)
          rw [(numberFieldComplexificationBaseEquiv F).apply_symm_apply]
            at hy'
          exact hy'
        rw [← hy]
        change
          σ (algebraMap F (numberFieldComplexification F)
              ((numberFieldComplexificationBaseEquiv F).symm y)) =
            algebraMap F (numberFieldComplexification F)
              ((numberFieldComplexificationBaseEquiv F).symm y)
        exact σ.commutes _ }
  map_one' := rfl
  map_mul' _ _ := rfl

theorem

numberFieldComplexificationChangeBase_injective

L253 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationChangeBase_injective

Source context 13 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F) :=
  (numberFieldComplexificationBaseLayer F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationCyclotomicLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer F).algebra'
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isAbelianGalois :
    IsAbelianGalois ℚ
      (numberFieldComplexificationCyclotomicLayer F) :=
  IsAbelianGalois.of_algHom
    (numberFieldComplexificationCyclotomicEquiv F).symm.toAlgHom
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isGalois :
    IsGalois ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isAbelianGalois
    F).toIsGalois
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_normal :
    Normal ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isGalois
    F).to_normal

Lean source · statement

theorem numberFieldComplexificationChangeBase_injective :
    Function.Injective (numberFieldComplexificationChangeBase F)

def

numberFieldComplexificationLayerRestriction

L264 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationLayerRestriction

Source context 13 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F) :=
  (numberFieldComplexificationBaseLayer F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationCyclotomicLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer F).algebra'
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isAbelianGalois :
    IsAbelianGalois ℚ
      (numberFieldComplexificationCyclotomicLayer F) :=
  IsAbelianGalois.of_algHom
    (numberFieldComplexificationCyclotomicEquiv F).symm.toAlgHom
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isGalois :
    IsGalois ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isAbelianGalois
    F).toIsGalois
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_normal :
    Normal ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isGalois
    F).to_normal

Lean source · statement

def numberFieldComplexificationLayerRestriction :
    Gal(numberFieldComplexification F /
        numberFieldComplexificationBaseLayer F) →*
      Gal(numberFieldComplexificationCyclotomicLayer F / ℚ)

theorem

numberFieldComplexificationLayerRestriction_injective

L278 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationLayerRestriction_injective

Source context 13 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F) :=
  (numberFieldComplexificationBaseLayer F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationCyclotomicLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer F).algebra'
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isAbelianGalois :
    IsAbelianGalois ℚ
      (numberFieldComplexificationCyclotomicLayer F) :=
  IsAbelianGalois.of_algHom
    (numberFieldComplexificationCyclotomicEquiv F).symm.toAlgHom
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isGalois :
    IsGalois ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isAbelianGalois
    F).toIsGalois
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_normal :
    Normal ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isGalois
    F).to_normal

Lean source · statement

theorem numberFieldComplexificationLayerRestriction_injective :
    Function.Injective
      (numberFieldComplexificationLayerRestriction F)

def

numberFieldComplexificationTransportCyclotomic

L291 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationTransportCyclotomic

Source context 13 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F) :=
  (numberFieldComplexificationBaseLayer F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationCyclotomicLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer F).algebra'
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isAbelianGalois :
    IsAbelianGalois ℚ
      (numberFieldComplexificationCyclotomicLayer F) :=
  IsAbelianGalois.of_algHom
    (numberFieldComplexificationCyclotomicEquiv F).symm.toAlgHom
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isGalois :
    IsGalois ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isAbelianGalois
    F).toIsGalois
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_normal :
    Normal ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isGalois
    F).to_normal

Lean source · statement

def numberFieldComplexificationTransportCyclotomic :
    Gal(rationalComplexificationCyclotomicField / ℚ) →*
      Gal(numberFieldComplexificationCyclotomicLayer F / ℚ)

theorem

numberFieldComplexificationRestriction_commutes

L297 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationRestriction_commutes

Source context 13 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F) :=
  (numberFieldComplexificationBaseLayer F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationCyclotomicLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer F).algebra'
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isAbelianGalois :
    IsAbelianGalois ℚ
      (numberFieldComplexificationCyclotomicLayer F) :=
  IsAbelianGalois.of_algHom
    (numberFieldComplexificationCyclotomicEquiv F).symm.toAlgHom
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isGalois :
    IsGalois ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isAbelianGalois
    F).toIsGalois
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_normal :
    Normal ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isGalois
    F).to_normal

Lean source · statement

theorem numberFieldComplexificationRestriction_commutes
    (σ : Gal(numberFieldComplexification F/F)) :
    numberFieldComplexificationTransportCyclotomic F
        (numberFieldComplexificationRestriction F σ) =
      numberFieldComplexificationLayerRestriction F
        (numberFieldComplexificationChangeBase F σ)

theorem

numberFieldComplexificationRestriction_injective

L380 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexificationRestriction_injective

Documentation

The rational cyclotomic factor generates the complexification together with F, hence restriction to that factor is injective.

Source context 13 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F) :=
  (numberFieldComplexificationBaseLayer F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationCyclotomicLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer F).algebra'
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isAbelianGalois :
    IsAbelianGalois ℚ
      (numberFieldComplexificationCyclotomicLayer F) :=
  IsAbelianGalois.of_algHom
    (numberFieldComplexificationCyclotomicEquiv F).symm.toAlgHom
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isGalois :
    IsGalois ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isAbelianGalois
    F).toIsGalois
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_normal :
    Normal ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isGalois
    F).to_normal

Lean source · statement

theorem numberFieldComplexificationRestriction_injective :
    Function.Injective (numberFieldComplexificationRestriction F)

instance

numberFieldComplexification_isAbelianGalois

L388 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldComplexification_isAbelianGalois

Source context 13 commands

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

open scoped IsMulCommutative
open AlgebraicNumberTheory NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
variable (F : Type*) [Field F] [NumberField F]
@[reducible]
noncomputable local instance
    numberFieldComplexificationRationalAlgebra :
    Algebra ℚ (numberFieldComplexification F) :=
  (numberFieldComplexification F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationBaseLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationBaseLayer F) :=
  (numberFieldComplexificationBaseLayer F).algebra'
@[reducible]
noncomputable local instance
    numberFieldComplexificationCyclotomicLayerRationalAlgebra :
    Algebra ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer F).algebra'
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isAbelianGalois :
    IsAbelianGalois ℚ
      (numberFieldComplexificationCyclotomicLayer F) :=
  IsAbelianGalois.of_algHom
    (numberFieldComplexificationCyclotomicEquiv F).symm.toAlgHom
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_isGalois :
    IsGalois ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isAbelianGalois
    F).toIsGalois
private noncomputable local instance
    numberFieldComplexificationCyclotomicLayer_normal :
    Normal ℚ (numberFieldComplexificationCyclotomicLayer F) :=
  (numberFieldComplexificationCyclotomicLayer_isGalois
    F).to_normal

Lean source · statement

instance numberFieldComplexification_isAbelianGalois :
    IsAbelianGalois F (numberFieldComplexification F)

Module documentation

Complexification of a number field

Declarations