NYLL
Module

CyclotomicRestriction.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.CyclicInertia.CyclotomicRestriction
2 declarations indexed from sourceView source ↗

Module documentation

Restricting cyclotomic inversion to normal extensions

An automorphism of a separable closure which inverts roots of unity restricts to every normal separable subextension. The subextension is first embedded in the separable closure and the restricted automorphism is then transported back across that embedding.

Imports1
Imported by2

Declarations

theorem

exists_intermediateFieldAlgEquiv_inverting_torsionUnits_of_ratEquiv

L25 ↗
EtaleFundamentalGroups.exists_intermediateFieldAlgEquiv_inverting_torsionUnits_of_ratEquiv
Source context 3 commands

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

noncomputable section
universe u v w x
namespace EtaleFundamentalGroups
Lean source · statement
theorem
    exists_intermediateFieldAlgEquiv_inverting_torsionUnits_of_ratEquiv
    {k : Type u} {F : Type v} {Omega : Type w}
    [Field k] [Field F] [Field Omega]
    [Algebra k F] [Algebra F Omega] [Algebra k Omega]
    [IsScalarTower k F Omega] [IsSepClosure F Omega]
    (e : k ≃+* ℚ)
    (hdisjoint : (separableClosure k Omega).LinearDisjoint F)
    (M : IntermediateField F Omega) [Normal F M] :
    ∃ tau : M ≃ₐ[F] M,
      ∀ z : Mˣ, IsOfFinOrder z →
        Units.mapEquiv tau.toMulEquiv z = z⁻¹
theorem

exists_normalAlgEquiv_inverting_torsionUnits_of_separableClosure_linearDisjoint_of_ratEquiv

L66 ↗
EtaleFundamentalGroups.exists_normalAlgEquiv_inverting_torsionUnits_of_separableClosure_linearDisjoint_of_ratEquiv
Documentation

Let Omega be a separable closure of F, with the separable closure of the rational base linearly disjoint from F. Every normal separable extension E / F embedded in Omega inherits an automorphism which inverts all finite-order units.

The embedding is constructed canonically from separable closedness; E itself is not required to be a separable closure.

Source context 3 commands

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

noncomputable section
universe u v w x
namespace EtaleFundamentalGroups
Lean source · statement
theorem
    exists_normalAlgEquiv_inverting_torsionUnits_of_separableClosure_linearDisjoint_of_ratEquiv
    {k : Type u} {F : Type v} {E : Type x} {Omega : Type w}
    [Field k] [Field F] [Field E] [Field Omega]
    [Algebra k F] [Algebra F E] [Algebra F Omega] [Algebra k Omega]
    [IsScalarTower k F Omega] [IsSepClosure F Omega]
    [Normal F E] [Algebra.IsSeparable F E]
    (e : k ≃+* ℚ)
    (hdisjoint : (separableClosure k Omega).LinearDisjoint F) :
    ∃ tau : E ≃ₐ[F] E,
      ∀ z : Eˣ, IsOfFinOrder z →
        Units.mapEquiv tau.toMulEquiv z = z⁻¹

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.