Module

SemilinearRestriction.lean

Nyll.GaloisCohomology.Kummer.Concrete.SemilinearRestriction

3 declarations indexed from sourceView source ↗

Module documentation

Restriction of semilinear Galois conjugation

Conjugation by the same ambient field automorphism commutes with restriction of scalars. For two field towers, restriction to a normal field supplies the lower automorphism and its actual compatibility with the upper automorphism. An ambient lift then inherits this lower semilinearity through the tower.

Imports4

Nyll.GaloisCohomology.Kummer.Concrete.SemilinearConjugation
Mathlib.Algebra.Algebra.Tower
Mathlib.FieldTheory.Galois.Basic
Mathlib.FieldTheory.Normal.Defs

Imported by3

theorem

semilinearGaloisConjugate_restrictScalars

L30 ↗

KummerTheory.semilinearGaloisConjugate_restrictScalars

Documentation

Conjugation by one ambient automorphism commutes with restriction of scalars between its two fields of semilinearity.

Source context 3 commands

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

namespace KummerTheory
section ScalarTower
variable {K L Ω : Type*} [Field K] [Field L] [Field Ω]
  [Algebra K L] [Algebra K Ω] [Algebra L Ω] [IsScalarTower K L Ω]

Lean source · statement

theorem semilinearGaloisConjugate_restrictScalars
    (τK : K ≃+* K) (τL : L ≃+* L) (a : Ω ≃+* Ω)
    (haK : ∀ x : K, a (algebraMap K Ω x) = algebraMap K Ω (τK x))
    (haL : ∀ x : L, a (algebraMap L Ω x) = algebraMap L Ω (τL x))
    (σ : Gal(Ω/L)) :
    (semilinearGaloisConjugate τL a haL σ).restrictScalars K =
      semilinearGaloisConjugate τK a haK (σ.restrictScalars K)

theorem

restrictRestrictAlgEquivMapHom_algebraMap

L52 ↗

KummerTheory.restrictRestrictAlgEquivMapHom_algebraMap

Documentation

The actual restriction from Gal(E/L) to Gal(K/F) preserves evaluation on the embedded normal field. No compositum or surjectivity assumption is needed.

Source context 3 commands

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

namespace KummerTheory
section NormalRestriction
variable (F K L E : Type*) [Field F] [Field K] [Field L] [Field E]
  [Algebra F K] [Algebra F L] [Algebra F E] [Algebra K E] [Algebra L E]
  [IsScalarTower F K E] [IsScalarTower F L E] [Normal F K]

Lean source · statement

theorem restrictRestrictAlgEquivMapHom_algebraMap
    (τ : Gal(E/L)) (x : K) :
    τ (algebraMap K E x) = algebraMap K E
      (IntermediateField.restrictRestrictAlgEquivMapHom F K L E τ x)

theorem

semilinear_restrictRestrictAlgEquivMapHom_algebraMap

L64 ↗

KummerTheory.semilinear_restrictRestrictAlgEquivMapHom_algebraMap

Documentation

A lift of the upper automorphism lies over its actual restriction to the normal field. The lower compatibility is generated from restriction and the scalar tower, rather than supplied as a comparison hypothesis.

Source context 4 commands

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

namespace KummerTheory
section NormalRestriction
variable (F K L E : Type*) [Field F] [Field K] [Field L] [Field E]
  [Algebra F K] [Algebra F L] [Algebra F E] [Algebra K E] [Algebra L E]
  [IsScalarTower F K E] [IsScalarTower F L E] [Normal F K]
variable {Ω : Type*} [Field Ω] [Algebra K Ω] [Algebra E Ω]
  [IsScalarTower K E Ω]

Lean source · statement

theorem semilinear_restrictRestrictAlgEquivMapHom_algebraMap
    (τ : Gal(E/L)) (a : Ω ≃+* Ω)
    (ha : ∀ x : E, a (algebraMap E Ω x) = algebraMap E Ω (τ x))
    (x : K) :
    a (algebraMap K Ω x) = algebraMap K Ω
      (IntermediateField.restrictRestrictAlgEquivMapHom F K L E τ x)

Module documentation

Restriction of semilinear Galois conjugation

Declarations

semilinearGaloisConjugate_restrictScalars

restrictRestrictAlgEquivMapHom_algebraMap

semilinear_restrictRestrictAlgEquivMapHom_algebraMap