Module

InfiniteBaseChange.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Galois.InfiniteBaseChange

4 declarations indexed from sourceView source ↗

Module documentation

Infinite Galois base change from finite layers

This module supplies the field-theoretic passage from finite Galois layers to their union after a change of base field. It is stated entirely in terms of mathlib's actual intermediate fields and uses no abstract replacement for the compositum.

Imports3

Mathlib.FieldTheory.Galois.GaloisClosure
Mathlib.FieldTheory.Normal.Basic
Mathlib.FieldTheory.SeparableClosure

Imported by2

theorem

le_iSup_lift_finiteGalois

L30 ↗

IntermediateField.le_iSup_lift_finiteGalois

Documentation

A Galois intermediate field is the union of the lifts of its finite Galois intermediate subfields.

Source context 3 commands

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

noncomputable section
namespace IntermediateField
variable {R U : Type*} [Field R] [Field U] [Algebra R U]

Lean source · statement

theorem le_iSup_lift_finiteGalois
    (B : IntermediateField R U) [IsGalois R B] :
    B ≤ ⨆ E : FiniteGaloisIntermediateField R B,
      IntermediateField.lift E.toIntermediateField

theorem

sup_eq_iSup_finiteGaloisComposita

L50 ↗

IntermediateField.sup_eq_iSup_finiteGaloisComposita

Documentation

A compositum with a Galois intermediate field is the supremum of the composita with its finite Galois intermediate layers.

Source context 3 commands

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

noncomputable section
namespace IntermediateField
variable {R U : Type*} [Field R] [Field U] [Algebra R U]

Lean source · statement

theorem sup_eq_iSup_finiteGaloisComposita
    (A B : IntermediateField R U) [IsGalois R B] :
    A ⊔ B = ⨆ E : FiniteGaloisIntermediateField R B,
      A ⊔ IntermediateField.lift E.toIntermediateField

theorem

extendScalars_sup_eq_iSup_finiteGaloisComposita

L75 ↗

IntermediateField.extendScalars_sup_eq_iSup_finiteGaloisComposita

Documentation

Base change commutes with the supremum of finite Galois composita.

Source context 3 commands

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

noncomputable section
namespace IntermediateField
variable {R U : Type*} [Field R] [Field U] [Algebra R U]

Lean source · statement

theorem extendScalars_sup_eq_iSup_finiteGaloisComposita
    (A B : IntermediateField R U) [IsGalois R B] :
    IntermediateField.extendScalars (F := A) (E := A ⊔ B) le_sup_left =
      ⨆ E : FiniteGaloisIntermediateField R B,
        IntermediateField.extendScalars (F := A)
          (E := A ⊔ IntermediateField.lift E.toIntermediateField)
          le_sup_left

theorem

isGalois_extendScalars_sup_of_forall_finiteGalois

L103 ↗

IntermediateField.isGalois_extendScalars_sup_of_forall_finiteGalois

Documentation

If every finite Galois layer of a compositum remains Galois after base change, then so does the full compositum.

Source context 3 commands

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

noncomputable section
namespace IntermediateField
variable {R U : Type*} [Field R] [Field U] [Algebra R U]

Lean source · statement

theorem isGalois_extendScalars_sup_of_forall_finiteGalois
    (A B : IntermediateField R U) [IsGalois R B]
    (hG : ∀ E : FiniteGaloisIntermediateField R B,
      IsGalois A
        (IntermediateField.extendScalars (F := A)
          (E := A ⊔ IntermediateField.lift E.toIntermediateField)
          le_sup_left)) :
    IsGalois A
      (IntermediateField.extendScalars (F := A) (E := A ⊔ B) le_sup_left)

Module documentation

Infinite Galois base change from finite layers

Declarations

le_iSup_lift_finiteGalois

sup_eq_iSup_finiteGaloisComposita

extendScalars_sup_eq_iSup_finiteGaloisComposita

isGalois_extendScalars_sup_of_forall_finiteGalois