Module

AbelianGaloisEquiv.lean

Nyll.ClassFieldTheory.Algebra.AbelianGaloisEquiv

2 declarations indexed from sourceView source ↗

Module documentation

Abelian Galois extensions under equivalent field presentations

Compatible equivalences of the base and extension fields identify their Galois automorphisms and preserve the abelian Galois property. These results use only Mathlib's algebra and Galois APIs; they do not depend on local class field theory or ramification.

Imports1

Mathlib.FieldTheory.Galois.Abelian

Imported by5

theorem

isAbelianGalois_of_equiv_equiv

L24 ↗

ClassFieldTheory.isAbelianGalois_of_equiv_equiv

Documentation

Abelian Galois extensions remain abelian Galois after compatible ring equivalences on both the base and extension fields.

Source context 2 commands

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

noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem isAbelianGalois_of_equiv_equiv
    {K L M N : Type*}
    [Field K] [Field L] [Algebra K L] [IsAbelianGalois K L]
    [Field M] [Field N] [Algebra M N]
    (f : K ≃+* M) (g : L ≃+* N)
    (hcomp : (algebraMap M N).comp f.toRingHom =
      g.toRingHom.comp (algebraMap K L)) :
    IsAbelianGalois M N

def

galEquiv_of_equiv_equiv

L70 ↗

ClassFieldTheory.galEquiv_of_equiv_equiv