Module

FiniteAbelianIntermediateFieldAlgEquiv.lean

Nyll.ClassFieldTheory.Algebra.FiniteAbelianIntermediateFieldAlgEquiv

3 declarations indexed from sourceView source ↗

Module documentation

Finite abelian intermediate fields under an ambient algebra equivalence

An algebra equivalence of ambient fields transports finite-dimensionality and the abelian Galois property of every intermediate field.

Imports2

Imported by2

theorem

intermediateFieldMap_commutes

L29 ↗

ClassFieldTheory.intermediateFieldMap_commutes

Documentation

The equivalence of intermediate fields commutes with their base-field embeddings.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v w
variable {F : Type u} {L : Type v} {L' : Type w}
  [Field F] [Field L] [Field L'] [Algebra F L] [Algebra F L']
  (e : L ≃ₐ[F] L') (E : IntermediateField F L)

Lean source · statement

theorem intermediateFieldMap_commutes :
    (algebraMap F (E.map e.toAlgHom)).comp (RingEquiv.refl F).toRingHom =
      (IntermediateField.intermediateFieldMap e E).toRingHom.comp
        (algebraMap F E)

theorem

finiteDimensional_intermediateField_map_algEquiv

L38 ↗

ClassFieldTheory.finiteDimensional_intermediateField_map_algEquiv

Documentation

Mapping an intermediate field through an ambient algebra equivalence preserves its finite-dimensionality.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v w
variable {F : Type u} {L : Type v} {L' : Type w}
  [Field F] [Field L] [Field L'] [Algebra F L] [Algebra F L']
  (e : L ≃ₐ[F] L') (E : IntermediateField F L)

Lean source · statement

theorem finiteDimensional_intermediateField_map_algEquiv
    [FiniteDimensional F E] :
    FiniteDimensional F (E.map e.toAlgHom)

theorem

isAbelianGalois_intermediateField_map_algEquiv

L47 ↗

ClassFieldTheory.isAbelianGalois_intermediateField_map_algEquiv

Documentation

Mapping an intermediate field through an ambient algebra equivalence preserves its abelian Galois property.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v w
variable {F : Type u} {L : Type v} {L' : Type w}
  [Field F] [Field L] [Field L'] [Algebra F L] [Algebra F L']
  (e : L ≃ₐ[F] L') (E : IntermediateField F L)

Lean source · statement

theorem isAbelianGalois_intermediateField_map_algEquiv
    [IsAbelianGalois F E] :
    IsAbelianGalois F (E.map e.toAlgHom)

Module documentation

Finite abelian intermediate fields under an ambient algebra equivalence

Declarations

intermediateFieldMap_commutes

finiteDimensional_intermediateField_map_algEquiv

isAbelianGalois_intermediateField_map_algEquiv