NYLL
Module

AlgebraicClosureTower.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.AlgebraicClosureTower
5 declarations indexed from sourceView source ↗

Module documentation

Algebraic Closure Tower

The actual projection from the constant extension to its maximal separable intermediate extension.

Imports4
Imported by3

Declarations

def

separableClosureProjection

L34 ↗
AlgebraicGeometry.FiniteEtale.separableClosureProjection
Documentation

The actual projection from the constant extension to its maximal separable intermediate extension.

Source context 10 commands

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

noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
local notation "K" => separableClosure k L
local notation "φK" => Spec.map (CommRingCat.ofHom (algebraMap k K))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "ψ" =>
  Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (IntermediateField.val (separableClosure k L))))
Lean source · statement
def separableClosureProjection : Limits.pullback φL f ⟶ Limits.pullback φK f
theorem

separableClosureProjection_comp_snd

L41 ↗
AlgebraicGeometry.FiniteEtale.separableClosureProjection_comp_snd
Documentation

The projection to the separable intermediate extension preserves the original scheme coordinate.

Source context 10 commands

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

noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
local notation "K" => separableClosure k L
local notation "φK" => Spec.map (CommRingCat.ofHom (algebraMap k K))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "ψ" =>
  Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (IntermediateField.val (separableClosure k L))))
Lean source · statement
theorem separableClosureProjection_comp_snd :
    separableClosureProjection k L X f ≫ pullback.snd φK f = pullback.snd φL f
theorem

separableClosureProjection_comp_fst

L50 ↗
AlgebraicGeometry.FiniteEtale.separableClosureProjection_comp_fst
Documentation

The projection preserves the coefficient coordinate along the canonical inclusion of the maximal separable subfield.

Source context 10 commands

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

noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
local notation "K" => separableClosure k L
local notation "φK" => Spec.map (CommRingCat.ofHom (algebraMap k K))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "ψ" =>
  Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (IntermediateField.val (separableClosure k L))))
Lean source · statement
theorem separableClosureProjection_comp_fst :
    separableClosureProjection k L X f ≫ pullback.fst φK f =
      pullback.fst φL f ≫ ψ
theorem

separableClosureProjection_isPullback

L60 ↗
AlgebraicGeometry.FiniteEtale.separableClosureProjection_isPullback
Documentation

The projection is the actual base change of the inclusion of the maximal separable subfield.

Source context 10 commands

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

noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
local notation "K" => separableClosure k L
local notation "φK" => Spec.map (CommRingCat.ofHom (algebraMap k K))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "ψ" =>
  Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (IntermediateField.val (separableClosure k L))))
Lean source · statement
theorem separableClosureProjection_isPullback :
    IsPullback (separableClosureProjection k L X f) (pullback.fst φL f)
      (pullback.fst φK f) ψ
theorem

connectedSpace_separableClosure_of_connected_constantField

L75 ↗
AlgebraicGeometry.FiniteEtale.connectedSpace_separableClosure_of_connected_constantField
Documentation

Connectedness descends from the algebraic constant extension to its maximal separable intermediate extension.

Source context 10 commands

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

noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
local notation "K" => separableClosure k L
local notation "φK" => Spec.map (CommRingCat.ofHom (algebraMap k K))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "ψ" =>
  Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (IntermediateField.val (separableClosure k L))))
Lean source · statement
theorem connectedSpace_separableClosure_of_connected_constantField
    [ConnectedSpace ↑(Limits.pullback φL f)] :
    ConnectedSpace ↑(Limits.pullback φK f)

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