Module

BinaryUnramifiedCompositum.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.BinaryUnramifiedCompositum

4 declarations indexed from sourceView source ↗

Module documentation

Binary everywhere-unramified composita

This file proves that the compositum of two finite Galois number-field extensions unramified at finite places is again unramified at finite places. An odd-degree hypothesis on the compositum then supplies the infinite-place condition.

Imports3

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.EverywhereUnramifiedBridge
Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.CompositumUnramified
Mathlib.FieldTheory.Galois.GaloisClosure

Imported by2

instance

finiteIntermediateFieldNumberField

L28 ↗

ClassFieldTower.Martinet.finiteIntermediateFieldNumberField

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u v
namespace ClassFieldTower.Martinet

Lean source · statement

instance finiteIntermediateFieldNumberField
    {K : Type u} {Omega : Type v}
    [Field K] [NumberField K]
    [Field Omega] [Algebra K Omega]
    (E : IntermediateField K Omega) [FiniteDimensional K E] :
    NumberField E

theorem

restrict_left_sup_restrict_right_eq_top

L37 ↗

ClassFieldTower.Martinet.restrict_left_sup_restrict_right_eq_top

Documentation

The two restricted factors generate their compositum.

Source context 5 commands

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

open scoped NumberField
noncomputable section
universe u v
namespace ClassFieldTower.Martinet
private local instance finiteIntermediateFieldNumberField
    {K : Type u} {Omega : Type v}
    [Field K] [NumberField K]
    [Field Omega] [Algebra K Omega]
    (E : IntermediateField K Omega) [FiniteDimensional K E] :
    NumberField E :=
  NumberField.of_module_finite K E

Lean source · full declaration

theorem restrict_left_sup_restrict_right_eq_top
    {K : Type u} {Omega : Type v}
    [Field K] [Field Omega] [Algebra K Omega]
    (E₁ E₂ : IntermediateField K Omega) :
    IntermediateField.restrict
          (show E₁ ≤ E₁ ⊔ E₂ from le_sup_left) ⊔
        IntermediateField.restrict
          (show E₂ ≤ E₁ ⊔ E₂ from le_sup_right) = ⊤ := by
  apply IntermediateField.lift_injective (E₁ ⊔ E₂)
  rw [IntermediateField.lift_sup,
    IntermediateField.lift_restrict,
    IntermediateField.lift_restrict,
    IntermediateField.lift_top]

theorem

finitePlaceUnramifiedness_sup

L53 ↗

ClassFieldTower.Martinet.finitePlaceUnramifiedness_sup

Documentation

The compositum of two finite Galois extensions unramified at every finite place is again unramified at every finite place.

Source context 5 commands

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

open scoped NumberField
noncomputable section
universe u v
namespace ClassFieldTower.Martinet
private local instance finiteIntermediateFieldNumberField
    {K : Type u} {Omega : Type v}
    [Field K] [NumberField K]
    [Field Omega] [Algebra K Omega]
    (E : IntermediateField K Omega) [FiniteDimensional K E] :
    NumberField E :=
  NumberField.of_module_finite K E

Lean source · statement

theorem finitePlaceUnramifiedness_sup
    {K : Type u} {Omega : Type v}
    [Field K] [NumberField K]
    [Field Omega] [Algebra K Omega]
    (E₁ E₂ : IntermediateField K Omega)
    [FiniteDimensional K E₁] [FiniteDimensional K E₂]
    [IsGalois K E₁] [IsGalois K E₂]
    (h₁ : IsUnramifiedAtFinitePlaces K E₁)
    (h₂ : IsUnramifiedAtFinitePlaces K E₂) :
    IsUnramifiedAtFinitePlaces K ↥(E₁ ⊔ E₂)

theorem

everywhereUnramified_sup_of_odd_finrank

L136 ↗

ClassFieldTower.Martinet.everywhereUnramified_sup_of_odd_finrank

Documentation

If the finite Galois compositum has odd degree, then finite-place unramifiedness of both factors makes the compositum everywhere unramified.

Source context 5 commands

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

open scoped NumberField
noncomputable section
universe u v
namespace ClassFieldTower.Martinet
private local instance finiteIntermediateFieldNumberField
    {K : Type u} {Omega : Type v}
    [Field K] [NumberField K]
    [Field Omega] [Algebra K Omega]
    (E : IntermediateField K Omega) [FiniteDimensional K E] :
    NumberField E :=
  NumberField.of_module_finite K E

Lean source · statement

theorem everywhereUnramified_sup_of_odd_finrank
    {K : Type u} {Omega : Type v}
    [Field K] [NumberField K]
    [Field Omega] [Algebra K Omega]
    (E₁ E₂ : IntermediateField K Omega)
    [FiniteDimensional K E₁] [FiniteDimensional K E₂]
    [IsGalois K E₁] [IsGalois K E₂]
    (h₁ : IsEverywhereUnramified K E₁)
    (h₂ : IsEverywhereUnramified K E₂)
    (hOdd : Odd (Module.finrank K ↥(E₁ ⊔ E₂))) :
    IsEverywhereUnramified K ↥(E₁ ⊔ E₂)

Module documentation

Binary everywhere-unramified composita

Declarations

finiteIntermediateFieldNumberField

restrict_left_sup_restrict_right_eq_top

finitePlaceUnramifiedness_sup

everywhereUnramified_sup_of_odd_finrank