NYLL
Module

SeparableInjectivity.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.SeparableInjectivity
6 declarations indexed from sourceView source ↗

Module documentation

Separable Injectivity

The chosen coefficient component embeds in the pullback of the composite cover.

Imports4
Imported by4

Declarations

def

finiteStagePullbackInclusion

L26 ↗
AlgebraicGeometry.FiniteEtale.finiteStagePullbackInclusion
Documentation

The chosen coefficient component embeds in the pullback of the composite cover.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {S T Y : Scheme.{u}} (b : T ⟶ S) [IsFiniteEtale b]
  (c : Y ⟶ T) (U : FiniteEtale T)
Lean source · statement
def finiteStagePullbackInclusion :
    (FiniteEtale.pullback c).obj U ⟶
      (FiniteEtale.pullback (c ≫ b)).obj (FiniteEtale.mk (U.hom ≫ b))
theorem

finiteStagePullbackInclusion_mono

L39 ↗
AlgebraicGeometry.FiniteEtale.finiteStagePullbackInclusion_mono
Documentation

The component inclusion is a monomorphism, directly by its two projections.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {S T Y : Scheme.{u}} (b : T ⟶ S) [IsFiniteEtale b]
  (c : Y ⟶ T) (U : FiniteEtale T)
Lean source · statement
theorem finiteStagePullbackInclusion_mono : Mono (finiteStagePullbackInclusion b c U)
theorem

exists_mono_into_pullback_of_finiteStage

L59 ↗
AlgebraicGeometry.FiniteEtale.exists_mono_into_pullback_of_finiteStage
Documentation

An actual finite-stage model provides a subobject of an actual cover from the base.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {S T Y : Scheme.{u}} (b : T ⟶ S) [IsFiniteEtale b]
  (c : Y ⟶ T) (U : FiniteEtale T)
Lean source · statement
theorem exists_mono_into_pullback_of_finiteStage
    (a : Y ⟶ S) (ha : c ≫ b = a) (Z : FiniteEtale Y)
    (e : (FiniteEtale.pullback c).obj U ≅ Z) :
    ∃ (V : FiniteEtale S) (m : Z ⟶ (FiniteEtale.pullback a).obj V), Mono m
theorem

finiteSeparable_specMap_isFiniteEtale

L69 ↗
AlgebraicGeometry.FiniteEtale.finiteSeparable_specMap_isFiniteEtale
Documentation

A finite separable field extension gives an actual finite étale map of spectra.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {S T Y : Scheme.{u}} (b : T ⟶ S) [IsFiniteEtale b]
  (c : Y ⟶ T) (U : FiniteEtale T)
omit b c U in
Lean source · statement
theorem finiteSeparable_specMap_isFiniteEtale
    (k H : Type u) [Field k] [Field H] [Algebra k H]
    [FiniteDimensional k H] [Algebra.IsSeparable k H] :
    IsFiniteEtale (Spec.map (CommRingCat.ofHom (algebraMap k H)))
theorem

exists_mono_into_pullback_of_separable_constant_extension

L86 ↗
AlgebraicGeometry.FiniteEtale.exists_mono_into_pullback_of_separable_constant_extension
Documentation

Every finite étale cover after a separable constant extension embeds in the pullback of an actual finite étale cover of the original qcqs scheme.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {S T Y : Scheme.{u}} (b : T ⟶ S) [IsFiniteEtale b]
  (c : Y ⟶ T) (U : FiniteEtale T)
omit b c U in
Lean source · statement
theorem exists_mono_into_pullback_of_separable_constant_extension
    (k L : Type u) [Field k] [Field L] [Algebra k L] [Algebra.IsSeparable k L]
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    (f : X ⟶ Spec (CommRingCat.of k))
    (Z : FiniteEtale (Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)) :
    ∃ (V : FiniteEtale X)
      (m : Z ⟶ (FiniteEtale.pullback
        (Limits.pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)).obj V),
      Mono m
theorem

fundamentalGroupHom_injective_of_separable_constant_extension

L117 ↗
AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_injective_of_separable_constant_extension
Documentation

The homomorphism on geometric fundamental groups is injective after a separable extension of constants for a qcqs scheme.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {S T Y : Scheme.{u}} (b : T ⟶ S) [IsFiniteEtale b]
  (c : Y ⟶ T) (U : FiniteEtale T)
omit b c U in
Lean source · statement
theorem fundamentalGroupHom_injective_of_separable_constant_extension
    (k L : Type u) [Field k] [Field L] [Algebra k L] [Algebra.IsSeparable k L]
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X] [ConnectedSpace X]
    (f : X ⟶ Spec (CommRingCat.of k))
    [ConnectedSpace ↑(Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (CommRingCat.of Ω) ⟶
      Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) :
    Function.Injective (fundamentalGroupHom
      (Limits.pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) ξ)

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