Module

SeparableClosureRestriction.lean

Nyll.SchemeTheory.FunctionFields.SeparableClosure.SeparableClosureRestriction

3 declarations indexed from sourceView source ↗

Module documentation

Restriction to a separable closure in a common overfield

For a tower of fields k ⊆ K ⊆ Ω, every K-automorphism of Ω restricts to the separable closure of k inside Ω. When Ω is a separable closure of K, this restriction map is surjective provided that K and the separable closure of k are linearly disjoint over k.

The surjectivity proof extends an automorphism across the tensor compositum; linear disjointness supplies the field structure on that tensor product.

Imports2

Mathlib.FieldTheory.IsSepClosed
Mathlib.FieldTheory.LinearDisjoint

Imported by2

def

separableClosureRestriction

L41 ↗

EtaleFundamentalGroups.separableClosureRestriction

Documentation

Restriction of K-automorphisms of a common overfield to the separable closure of k in that overfield.

Source context 9 commands

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

@[expose] public section
noncomputable section
universe u v w
open IntermediateField
namespace EtaleFundamentalGroups
variable {k : Type u} {K : Type v} {Ω : Type w}
variable [Field k] [Field K] [Field Ω]
variable [Algebra k K] [Algebra K Ω] [Algebra k Ω]
variable [IsScalarTower k K Ω]

Lean source · full declaration

def separableClosureRestriction :
    (Ω ≃ₐ[K] Ω) →* (separableClosure k Ω ≃ₐ[k] separableClosure k Ω) where
  toFun σ := separableClosure.algEquivOfAlgEquiv (σ.restrictScalars k)
  map_one' := by
    ext x
    rfl
  map_mul' σ τ := by
    ext x
    rfl

theorem

separableClosureRestriction_coe

L52 ↗

EtaleFundamentalGroups.separableClosureRestriction_coe

Source context 9 commands

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

@[expose] public section
noncomputable section
universe u v w
open IntermediateField
namespace EtaleFundamentalGroups
variable {k : Type u} {K : Type v} {Ω : Type w}
variable [Field k] [Field K] [Field Ω]
variable [Algebra k K] [Algebra K Ω] [Algebra k Ω]
variable [IsScalarTower k K Ω]

Lean source · statement

theorem separableClosureRestriction_coe
    (σ : Ω ≃ₐ[K] Ω) (x : separableClosure k Ω) :
    ((separableClosureRestriction (k := k) (K := K) (Ω := Ω) σ x :
      separableClosure k Ω) : Ω) = σ (x : Ω)

theorem

separableClosureRestriction_surjective_of_linearDisjoint

L61 ↗

EtaleFundamentalGroups.separableClosureRestriction_surjective_of_linearDisjoint

Documentation

If Ω is a separable closure of K and the separable closure of k inside Ω is linearly disjoint from K, every automorphism of that separable closure over k extends to a K-automorphism of Ω.

Source context 9 commands

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

@[expose] public section
noncomputable section
universe u v w
open IntermediateField
namespace EtaleFundamentalGroups
variable {k : Type u} {K : Type v} {Ω : Type w}
variable [Field k] [Field K] [Field Ω]
variable [Algebra k K] [Algebra K Ω] [Algebra k Ω]
variable [IsScalarTower k K Ω]

Lean source · statement

theorem separableClosureRestriction_surjective_of_linearDisjoint
    [IsSepClosure K Ω]
    (h : (separableClosure k Ω).LinearDisjoint K) :
    Function.Surjective
      (separableClosureRestriction (k := k) (K := K) (Ω := Ω))

Module documentation

Restriction to a separable closure in a common overfield

Declarations

separableClosureRestriction

separableClosureRestriction_coe

separableClosureRestriction_surjective_of_linearDisjoint