NYLL
Module

GeometricallyIntegralRestriction.lean

Nyll.SchemeTheory.FunctionFields.SeparableClosure.GeometricallyIntegralRestriction
2 declarations indexed from sourceView source ↗

Module documentation

Geometrically integral field extensions and Galois restriction

A field extension K / k is regular in the geometric sense when Spec K → Spec k is geometrically integral. This file derives the linear disjointness with a separable closure directly from that geometric condition, then obtains surjectivity of the corresponding restriction map.

Imports2
Imported by2

Declarations

theorem

separableClosure_linearDisjoint_of_geometricallyIntegral

L39 ↗
EtaleFundamentalGroups.separableClosure_linearDisjoint_of_geometricallyIntegral
Documentation

A geometrically integral field extension is linearly disjoint from the separable closure of its base inside any common overfield.

Source context 10 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits IntermediateField
open AlgebraicGeometry
namespace EtaleFundamentalGroups
variable {k K Ω : Type u}
variable [Field k] [Field K] [Field Ω]
variable [Algebra k K] [Algebra K Ω] [Algebra k Ω]
variable [IsScalarTower k K Ω]
Lean source · statement
theorem separableClosure_linearDisjoint_of_geometricallyIntegral
    [GeometricallyIntegral
      (Spec.map (CommRingCat.ofHom (algebraMap k K)))] :
    (separableClosure k Ω).LinearDisjoint K
theorem

separableClosureRestriction_surjective_of_geometricallyIntegral

L65 ↗
EtaleFundamentalGroups.separableClosureRestriction_surjective_of_geometricallyIntegral
Documentation

Restriction from a separable closure of a geometrically integral field extension onto the separable closure of the base field is surjective.

Source context 10 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits IntermediateField
open AlgebraicGeometry
namespace EtaleFundamentalGroups
variable {k K Ω : Type u}
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_geometricallyIntegral
    [IsSepClosure K Ω]
    [GeometricallyIntegral
      (Spec.map (CommRingCat.ofHom (algebraMap k K)))] :
    Function.Surjective
      (separableClosureRestriction (k := k) (K := K) (Ω := Ω))

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