Module

FixedFieldLattice.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Galois.FixedFieldLattice

1 declaration indexed from sourceView source ↗

Module documentation

Fixed fields and subgroup lattice operations

Small order-theoretic facts about fixed fields of automorphism subgroups. They do not depend on class field theory and belong with the general Galois infrastructure rather than a concrete reciprocity construction.

Imports1

Mathlib.FieldTheory.Galois.Basic

Imported by2

theorem

fixedField_sup_eq_inf

L23 ↗

IntermediateField.fixedField_sup_eq_inf

Documentation

Fixed fields turn a supremum of automorphism subgroups into the intersection of their fixed fields.

Source context 1 command

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

namespace IntermediateField

Lean source · statement

theorem fixedField_sup_eq_inf
    {k Ω : Type*} [Field k] [Field Ω] [Algebra k Ω]
    (S T : Subgroup (Gal(Ω/k))) :
    IntermediateField.fixedField (S ⊔ T) =
      IntermediateField.fixedField S ⊓ IntermediateField.fixedField T

Module documentation

Fixed fields and subgroup lattice operations

Declarations

fixedField_sup_eq_inf