Module

SixPrimeQuadraticExponent.lean

Nyll.SawinTotallyRealTowers.SixPrimeQuadraticExponent

2 declarations indexed from sourceView source ↗

Module documentation

Exponent two in the five-field quadratic compositum

Restriction to the two factors of a compositum is jointly injective. An exponent bound on both Galois groups therefore holds on their compositum. Each of the five chosen quadratic fields has Galois group of order two, so every automorphism of their finite compositum squares to the identity. Its degree is not used in this argument.

Imports9

Nyll.SawinTotallyRealTowers.SixPrimeQuadraticCompositum
Mathlib.Algebra.Algebra.Equiv
Mathlib.Algebra.Group.Subgroup.Lattice
Mathlib.Data.Finset.Lattice.Fold
Mathlib.FieldTheory.Galois.Basic
Mathlib.FieldTheory.Galois.GaloisClosure
Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Mathlib.FieldTheory.Normal.Defs
Mathlib.GroupTheory.OrderOfElement

Imported by1

Nyll.SawinTotallyRealTowers.All

theorem

galois_pow_eq_one_sup

L31 ↗

ClassFieldTower.Sawin.galois_pow_eq_one_sup

Source context 2 commands

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

universe u v
namespace ClassFieldTower.Sawin

Lean source · statement

theorem galois_pow_eq_one_sup
    {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
    (E F : FiniteGaloisIntermediateField K Ω) (n : ℕ)
    (hE : ∀ σ : E ≃ₐ[K] E, σ ^ n = 1)
    (hF : ∀ σ : F ≃ₐ[K] F, σ ^ n = 1) :
    ∀ σ : (E ⊔ F : FiniteGaloisIntermediateField K Ω) ≃ₐ[K]
      (E ⊔ F : FiniteGaloisIntermediateField K Ω), σ ^ n = 1

theorem

sawinQuadraticCompositum_galois_sq_eq_one

L77 ↗

ClassFieldTower.Sawin.sawinQuadraticCompositum_galois_sq_eq_one

Documentation

Every automorphism of the actual five-quadratic-field compositum has square equal to the identity.