NYLL
Module

RamifiedOverextension.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ComplexificationArtin.RamifiedOverextension
21 declarations indexed from sourceView source ↗

Module documentation

The quadratic overextension at a ramified real place

This module constructs the real fixed field of complex conjugation, the quadratic overextension above it, and the faithful cyclotomic restriction.

Imports1
Imported by3

Declarations

def

ramifiedInfinitePlaceRealFixedField

L39 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceRealFixedField
Documentation

The base K' in the archimedean overextension: the fixed field of complex conjugation in L(i).

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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
def ramifiedInfinitePlaceRealFixedField
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    IntermediateField ℚ
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)
theorem

ramifiedInfinitePlaceOverfieldConjugation_fixes_base

L54 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverfieldConjugation_fixes_base
Documentation

Ambient complex conjugation on the overfield fixes the embedded base field at a ramified real place.

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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [FiniteDimensional K L] in
Lean source · statement
theorem ramifiedInfinitePlaceOverfieldConjugation_fixes_base
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (x : K) :
    ramifiedInfinitePlaceOverfieldConjugation
        (K := K) (L := L) v hRamified
        (algebraMap K
          (infinitePlaceComplexificationOverfield
            (K := K) (L := L) v) x) =
      algebraMap K
        (infinitePlaceComplexificationOverfield
          (K := K) (L := L) v) x
def

ramifiedInfinitePlaceRealFixedFieldEmbedding

L99 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceRealFixedFieldEmbedding
Documentation

The compatible embedding K → K' into the real fixed field.

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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
def ramifiedInfinitePlaceRealFixedFieldEmbedding
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    K →ₐ[ℚ]
      ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified
theorem

ramifiedInfinitePlaceRealFixedFieldEmbedding_coe

L138 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceRealFixedFieldEmbedding_coe
Documentation

The fixed-field embedding agrees with the original base-field algebra map after coercion to the 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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [FiniteDimensional K L] in
Lean source · statement
theorem ramifiedInfinitePlaceRealFixedFieldEmbedding_coe
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (x : K) :
    ((ramifiedInfinitePlaceRealFixedFieldEmbedding
        (K := K) (L := L) v hRamified x :
      ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified) :
      infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) =
      algebraMap K
        (infinitePlaceComplexificationOverfield
          (K := K) (L := L) v) x
instance

ramifiedInfinitePlaceRealFixedField_algebra

L177 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceRealFixedField_algebra
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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
instance
    ramifiedInfinitePlaceRealFixedField_algebra
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    Algebra K
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified)
instance

ramifiedInfinitePlaceRealFixedField_ratScalarTower

L188 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceRealFixedField_ratScalarTower
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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
instance ramifiedInfinitePlaceRealFixedField_ratScalarTower
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    IsScalarTower ℚ K
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified)
instance

ramifiedInfinitePlaceRealFixedField_scalarTower

L199 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceRealFixedField_scalarTower
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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
instance ramifiedInfinitePlaceRealFixedField_scalarTower
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    IsScalarTower K
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified)
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)
theorem

ramifiedInfinitePlaceRealFixedField_finiteDimensional

L216 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceRealFixedField_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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceRealFixedField_finiteDimensional
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    FiniteDimensional ℚ
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified)
instance

ramifiedInfinitePlaceRealFixedField_numberField

L230 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceRealFixedField_numberField
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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
instance ramifiedInfinitePlaceRealFixedField_numberField
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    NumberField
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified)
theorem

ramifiedInfinitePlaceRealFixedField_finiteDimensional_over_base

L249 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceRealFixedField_finiteDimensional_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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceRealFixedField_finiteDimensional_over_base
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    FiniteDimensional K
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified)
instance

ramifiedInfinitePlaceRealFixedField_isAbelianGalois_over_base

L261 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceRealFixedField_isAbelianGalois_over_base
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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
instance
    ramifiedInfinitePlaceRealFixedField_isAbelianGalois_over_base
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    IsAbelianGalois K
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified)
theorem

ramifiedInfinitePlaceOverfield_finiteDimensional_over_fixed

L276 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverfield_finiteDimensional_over_fixed
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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceOverfield_finiteDimensional_over_fixed
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    FiniteDimensional
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified)
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)
theorem

ramifiedInfinitePlaceOverextension_isGalois

L293 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextension_isGalois
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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem ramifiedInfinitePlaceOverextension_isGalois
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    IsGalois
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified)
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)
instance

ramifiedInfinitePlaceOverextension_isAbelianGalois

L311 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextension_isAbelianGalois
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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
instance
    ramifiedInfinitePlaceOverextension_isAbelianGalois
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    IsAbelianGalois
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified)
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v)
def

ramifiedInfinitePlaceOverextensionConjugation

L349 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionConjugation
Documentation

The distinguished nontrivial automorphism of the quadratic overextension L(i)/K', obtained from ambient complex conjugation.

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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
def ramifiedInfinitePlaceOverextensionConjugation
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    Gal(
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) /
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified))
theorem

ramifiedInfinitePlaceOverextensionConjugation_apply

L372 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionConjugation_apply
Documentation

The distinguished overextension automorphism is the restriction of ambient complex conjugation.

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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem ramifiedInfinitePlaceOverextensionConjugation_apply
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (z :
      infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) :
    ramifiedInfinitePlaceOverextensionConjugation
        (K := K) (L := L) v hRamified z =
      ramifiedInfinitePlaceOverfieldConjugation
        (K := K) (L := L) v hRamified z
theorem

ramifiedInfinitePlaceOverextension_eq_one_or_conjugation

L388 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextension_eq_one_or_conjugation
Documentation

Every automorphism of the overextension is either the identity or the distinguished complex conjugation.

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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem ramifiedInfinitePlaceOverextension_eq_one_or_conjugation
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (σ : Gal((infinitePlaceComplexificationOverfield
      (K := K) (L := L) v)/(ramifiedInfinitePlaceRealFixedField
      (K := K) (L := L) v hRamified))) :
    σ = 1 ∨
      σ =
        ramifiedInfinitePlaceOverextensionConjugation
          (K := K) (L := L) v hRamified
def

ramifiedInfinitePlaceOverextensionCyclotomicRestriction

L452 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionCyclotomicRestriction
Documentation

Restriction of the quadratic overextension Galois group to the rational fourth-root factor.

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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
Lean source · statement
def
    ramifiedInfinitePlaceOverextensionCyclotomicRestriction
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    Gal(
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) /
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified)) →*
      Gal(rationalComplexificationCyclotomicField / ℚ)
theorem

ramifiedInfinitePlaceOverfieldConjugation_map_zeta_ne

L470 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverfieldConjugation_map_zeta_ne
Documentation

The mapped primitive fourth root in the overfield is not fixed 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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem ramifiedInfinitePlaceOverfieldConjugation_map_zeta_ne
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    ramifiedInfinitePlaceOverfieldConjugation
        (K := K) (L := L) v hRamified
        (algebraMap rationalComplexificationCyclotomicField
          (infinitePlaceComplexificationOverfield
            (K := K) (L := L) v)
          (IsCyclotomicExtension.zeta
            4 ℚ rationalComplexificationCyclotomicField)) ≠
      algebraMap rationalComplexificationCyclotomicField
        (infinitePlaceComplexificationOverfield
          (K := K) (L := L) v)
        (IsCyclotomicExtension.zeta
          4 ℚ rationalComplexificationCyclotomicField)
theorem

ramifiedInfinitePlaceOverextensionCyclotomicRestriction_conjugation_ne_one

L526 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionCyclotomicRestriction_conjugation_ne_one
Documentation

The distinguished overextension conjugation restricts nontrivially to the rational fourth-root factor.

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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceOverextensionCyclotomicRestriction_conjugation_ne_one
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    ramifiedInfinitePlaceOverextensionCyclotomicRestriction
        (K := K) (L := L) v hRamified
        (ramifiedInfinitePlaceOverextensionConjugation
          (K := K) (L := L) v hRamified) ≠
      1
theorem

ramifiedInfinitePlaceOverextensionCyclotomicRestriction_injective

L619 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionCyclotomicRestriction_injective
Documentation

Restriction to the rational fourth-root factor is injective on the quadratic overextension.

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
attribute [local instance]
  infinitePlaceComplexificationOverfieldRationalAlgebra
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
attribute [local instance]
  rationalComplexificationCyclotomicField_isAbelianGalois
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceOverextensionCyclotomicRestriction_injective
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    Function.Injective
      (ramifiedInfinitePlaceOverextensionCyclotomicRestriction
        (K := K) (L := L) v hRamified)

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