Module

InfinitePlaceOverfield.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ComplexificationArtin.InfinitePlaceOverfield

38 declarations indexed from sourceView source ↗

Module documentation

The complex-conjugation overfield at an infinite place

This module realizes the embedded field L(i) inside ℂ, constructs its complex place, and identifies ambient complex conjugation on that field.

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ComplexificationArtin.RationalComplexification

Imported by3

theorem

complexEmbeddingFieldRange_map_complexConjugation

L35 ↗

GlobalClassFieldTheory.Reciprocity.complexEmbeddingFieldRange_map_complexConjugation

Documentation

The field range of a complex embedding is preserved by complex conjugation when a relative automorphism realizes that conjugation.

Source context 7 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem complexEmbeddingFieldRange_map_complexConjugation
    (φ : L →+* ℂ)
    (σ : L ≃ₐ[K] L)
    (hσ : NumberField.ComplexEmbedding.IsConj φ σ) :
    φ.toRatAlgHom.fieldRange.map
        (Complex.conjAe.restrictScalars ℚ).toAlgHom =
      φ.toRatAlgHom.fieldRange

def

infinitePlaceComplexificationOverfield

L64 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfield

Documentation

The concrete field L(i) inside ℂ, formed using the complex embedding belonging to the chosen place above v.

Source context 8 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

def infinitePlaceComplexificationOverfield
    (v : InfinitePlace K) :
    IntermediateField ℚ ℂ

instance

infinitePlaceComplexificationOverfieldRationalAlgebra

L72 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfieldRationalAlgebra

Source context 8 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

instance

infinitePlaceComplexificationOverfield_finiteDimensional

L81 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfield_finiteDimensional

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    infinitePlaceComplexificationOverfield_finiteDimensional
    (v : InfinitePlace K) :
    FiniteDimensional ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

instance

infinitePlaceComplexificationOverfield_numberField

L96 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfield_numberField

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    infinitePlaceComplexificationOverfield_numberField
    (v : InfinitePlace K) :
    NumberField
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

def

infinitePlaceComplexificationOverfieldEmbedding

L107 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfieldEmbedding

Documentation

The chosen top-field embedding L → L(i).

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

def infinitePlaceComplexificationOverfieldEmbedding
    (v : InfinitePlace K) :
    L →ₐ[ℚ]
      infinitePlaceComplexificationOverfield
        (K := K) (L := L) v

theorem

infinitePlaceComplexificationOverfieldEmbedding_coe

L131 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfieldEmbedding_coe

Documentation

The chosen embedding into the complexification overfield agrees with the original complex embedding after coercion to ℂ.

Source context 10 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'
omit [NumberField K] [FiniteDimensional K L] in

Lean source · statement

theorem infinitePlaceComplexificationOverfieldEmbedding_coe
    (v : InfinitePlace K) (x : L) :
    ((infinitePlaceComplexificationOverfieldEmbedding
        (K := K) (L := L) v x :
      infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) : ℂ) =
      InfinitePlace.embedding
        (chosenInfinitePlaceAbove (L := L) v) x

instance

infinitePlaceComplexificationOverfield_algebra

L146 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfield_algebra

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    infinitePlaceComplexificationOverfield_algebra
    (v : InfinitePlace K) :
    Algebra L
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

instance

infinitePlaceComplexificationOverfield_smul

L156 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfield_smul

Documentation

The scalar action belonging to the chosen top-field embedding.

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    infinitePlaceComplexificationOverfield_smul
    (v : InfinitePlace K) :
    SMul L
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

instance

infinitePlaceComplexificationOverfield_ratScalarTower

L165 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfield_ratScalarTower

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    infinitePlaceComplexificationOverfield_ratScalarTower
    (v : InfinitePlace K) :
    IsScalarTower ℚ L
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

instance

infinitePlaceComplexificationOverfield_baseAlgebra

L175 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfield_baseAlgebra

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    infinitePlaceComplexificationOverfield_baseAlgebra
    (v : InfinitePlace K) :
    Algebra K
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

instance

infinitePlaceComplexificationOverfield_baseSmul

L186 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfield_baseSmul

Documentation

The scalar action induced from the original base-field embedding.

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    infinitePlaceComplexificationOverfield_baseSmul
    (v : InfinitePlace K) :
    SMul K
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

instance

infinitePlaceComplexificationOverfield_baseRatScalarTower

L195 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfield_baseRatScalarTower

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    infinitePlaceComplexificationOverfield_baseRatScalarTower
    (v : InfinitePlace K) :
    IsScalarTower ℚ K
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

instance

infinitePlaceComplexificationOverfield_scalarTower

L206 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfield_scalarTower

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    infinitePlaceComplexificationOverfield_scalarTower
    (v : InfinitePlace K) :
    IsScalarTower K L
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

instance

infinitePlaceComplexificationOverfield_finiteDimensional_over_extension

L214 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfield_finiteDimensional_over_extension

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    infinitePlaceComplexificationOverfield_finiteDimensional_over_extension
    (v : InfinitePlace K) :
    FiniteDimensional L
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

def

rationalComplexificationEmbeddingInInfinitePlaceOverfield

L226 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationEmbeddingInInfinitePlaceOverfield

Documentation

The cyclotomic fourth-root field embeds into the concrete overfield through its copy in ℂ.

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

def
    rationalComplexificationEmbeddingInInfinitePlaceOverfield
    (v : InfinitePlace K) :
    rationalComplexificationCyclotomicField →ₐ[ℚ]
      infinitePlaceComplexificationOverfield
        (K := K) (L := L) v

instance

rationalComplexification_infinitePlaceOverfield_algebra

L240 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexification_infinitePlaceOverfield_algebra

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    rationalComplexification_infinitePlaceOverfield_algebra
    (v : InfinitePlace K) :
    Algebra rationalComplexificationCyclotomicField
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

instance

rationalComplexification_infinitePlaceOverfield_smul

L252 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexification_infinitePlaceOverfield_smul

Documentation

The scalar action induced by the concrete fourth-root-field embedding. Declaring it directly keeps instance search away from unrelated intermediate-field algebra structures.

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    rationalComplexification_infinitePlaceOverfield_smul
    (v : InfinitePlace K) :
    SMul rationalComplexificationCyclotomicField
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

instance

rationalComplexification_infinitePlaceOverfield_scalarTower

L261 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexification_infinitePlaceOverfield_scalarTower

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    rationalComplexification_infinitePlaceOverfield_scalarTower
    (v : InfinitePlace K) :
    IsScalarTower ℚ rationalComplexificationCyclotomicField
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

def

infinitePlaceEmbeddedExtensionField

L273 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceEmbeddedExtensionField

Documentation

The copy of the given abelian extension inside the concrete complexification overfield, viewed over the original base field.

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

def infinitePlaceEmbeddedExtensionField
    (v : InfinitePlace K) :
    IntermediateField K
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

instance

infinitePlaceEmbeddedExtensionField_isAbelianGalois

L282 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceEmbeddedExtensionField_isAbelianGalois

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    infinitePlaceEmbeddedExtensionField_isAbelianGalois
    (v : InfinitePlace K) :
    IsAbelianGalois K
      (infinitePlaceEmbeddedExtensionField
        (K := K) (L := L) v)

def

infinitePlaceBaseFourthRootField

L295 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceBaseFourthRootField

Documentation

The fourth-root cyclotomic factor over the original base field, inside the concrete complexification overfield.

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

def infinitePlaceBaseFourthRootField
    (v : InfinitePlace K) :
    IntermediateField K
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

instance

infinitePlaceBaseFourthRootField_isCyclotomic

L306 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceBaseFourthRootField_isCyclotomic

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    infinitePlaceBaseFourthRootField_isCyclotomic
    (v : InfinitePlace K) :
    IsCyclotomicExtension {4} K
      (infinitePlaceBaseFourthRootField
        (K := K) (L := L) v)

instance

infinitePlaceBaseFourthRootField_isAbelianGalois

L343 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceBaseFourthRootField_isAbelianGalois

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    infinitePlaceBaseFourthRootField_isAbelianGalois
    (v : InfinitePlace K) :
    IsAbelianGalois K
      (infinitePlaceBaseFourthRootField
        (K := K) (L := L) v)

def

infinitePlaceRatEmbeddedExtensionField

L355 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceRatEmbeddedExtensionField

Source context 10 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'
omit [FiniteDimensional K L] in

Lean source · statement

def infinitePlaceRatEmbeddedExtensionField
    (v : InfinitePlace K) :
    IntermediateField ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

def

infinitePlaceRatFourthRootField

L371 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceRatFourthRootField

Source context 10 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'
omit [FiniteDimensional K L] in

Lean source · statement

def infinitePlaceRatFourthRootField
    (v : InfinitePlace K) :
    IntermediateField ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

def

infinitePlaceRatComplexificationFactors

L384 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceRatComplexificationFactors

Source context 10 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'
omit [FiniteDimensional K L] in

Lean source · statement

def infinitePlaceRatComplexificationFactors
    (v : InfinitePlace K) :
    IntermediateField ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

theorem

infinitePlaceRatEmbeddedExtensionField_le_factors

L395 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceRatEmbeddedExtensionField_le_factors

Source context 10 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'
omit [FiniteDimensional K L] in

Lean source · statement

theorem infinitePlaceRatEmbeddedExtensionField_le_factors
    (v : InfinitePlace K) :
    infinitePlaceRatEmbeddedExtensionField
          (K := K) (L := L) v ≤
      infinitePlaceRatComplexificationFactors
          (K := K) (L := L) v

theorem

infinitePlaceRatFourthRootField_le_factors

L439 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceRatFourthRootField_le_factors

Source context 10 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'
omit [FiniteDimensional K L] in

Lean source · statement

theorem infinitePlaceRatFourthRootField_le_factors
    (v : InfinitePlace K) :
    infinitePlaceRatFourthRootField
          (K := K) (L := L) v ≤
      infinitePlaceRatComplexificationFactors
          (K := K) (L := L) v

theorem

infinitePlaceRatComplexificationFactors_sup

L501 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceRatComplexificationFactors_sup

Source context 10 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'
omit [NumberField K] [FiniteDimensional K L] in

Lean source · statement

theorem infinitePlaceRatComplexificationFactors_sup
    (v : InfinitePlace K) :
    infinitePlaceRatEmbeddedExtensionField
          (K := K) (L := L) v ⊔
        infinitePlaceRatFourthRootField
          (K := K) (L := L) v =
      ⊤

theorem

infinitePlaceComplexificationFactors_sup

L522 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationFactors_sup

Documentation

The embedded abelian extension and the base-changed fourth-root factor generate the whole concrete complexification overfield.

Source context 10 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'
omit [FiniteDimensional K L] in

Lean source · statement

theorem infinitePlaceComplexificationFactors_sup
    (v : InfinitePlace K) :
    infinitePlaceEmbeddedExtensionField
          (K := K) (L := L) v ⊔
        infinitePlaceBaseFourthRootField
          (K := K) (L := L) v =
      ⊤

instance

infinitePlaceComplexificationOverfield_isAbelianGalois_over_base

L545 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfield_isAbelianGalois_over_base

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    infinitePlaceComplexificationOverfield_isAbelianGalois_over_base
    (v : InfinitePlace K) :
    IsAbelianGalois K
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

instance

infinitePlaceComplexificationOverfield_isTotallyComplex

L578 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfield_isTotallyComplex

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

instance
    infinitePlaceComplexificationOverfield_isTotallyComplex
    (v : InfinitePlace K) :
    IsTotallyComplex
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

def

infinitePlaceComplexificationOverfieldComplexPlace

L591 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfieldComplexPlace

Documentation

The infinite place on the concrete overfield induced by its inclusion into ℂ.

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

def infinitePlaceComplexificationOverfieldComplexPlace
    (v : InfinitePlace K) :
    InfinitePlace
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)

theorem

infinitePlaceComplexificationOverfield_map_complexConjugation

L605 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfield_map_complexConjugation

Documentation

Complex conjugation preserves the concrete overfield L(i) at a ramified chosen place. Preservation of the L-factor is the actual local Artin value being a conjugation; preservation of the fourth-root factor is intrinsic.

Source context 10 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'
omit [NumberField K] [FiniteDimensional K L] in

Lean source · statement

theorem infinitePlaceComplexificationOverfield_map_complexConjugation
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v).map
        (Complex.conjAe.restrictScalars ℚ).toAlgHom =
      infinitePlaceComplexificationOverfield
        (K := K) (L := L) v

def

ramifiedInfinitePlaceOverfieldConjugation

L632 ↗

GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverfieldConjugation

Documentation

Complex conjugation restricted to the actual overfield L(i).

Source context 9 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'

Lean source · statement

def ramifiedInfinitePlaceOverfieldConjugation
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    infinitePlaceComplexificationOverfield
          (K := K) (L := L) v ≃ₐ[ℚ]
      infinitePlaceComplexificationOverfield
          (K := K) (L := L) v

theorem

ramifiedInfinitePlaceOverfieldConjugation_apply

L652 ↗

GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverfieldConjugation_apply

Documentation

The restricted overfield automorphism acts by ambient complex conjugation.

Source context 10 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'
omit [NumberField K] [FiniteDimensional K L] in

Lean source · statement

theorem ramifiedInfinitePlaceOverfieldConjugation_apply
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (z :
      infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :
    (ramifiedInfinitePlaceOverfieldConjugation
        (K := K) (L := L) v hRamified z : ℂ) =
      star (z : ℂ)

theorem

ramifiedInfinitePlaceOverfieldConjugation_sq

L667 ↗

GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverfieldConjugation_sq

Documentation

The restricted overfield complex conjugation is an involution.

Source context 10 commands

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

open scoped IsMulCommutative
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K]
    [Field L] [NumberField L] [Algebra K L]
variable
    [NumberField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
@[reducible]
noncomputable local instance
    infinitePlaceComplexificationOverfieldRationalAlgebra
    (v : InfinitePlace K) :
    Algebra ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :=
  (infinitePlaceComplexificationOverfield
    (K := K) (L := L) v).algebra'
omit [NumberField K] [FiniteDimensional K L] in

Lean source · statement

theorem ramifiedInfinitePlaceOverfieldConjugation_sq
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    ramifiedInfinitePlaceOverfieldConjugation
          (K := K) (L := L) v hRamified *
        ramifiedInfinitePlaceOverfieldConjugation
          (K := K) (L := L) v hRamified =
      1

Module documentation

The complex-conjugation overfield at an infinite place

Declarations