Module

PurelyInseparablePullback.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.PurelyInseparablePullback

3 declarations indexed from sourceView source ↗

Module documentation

Fully faithful pullback across purely inseparable extensions

Imports2

Nyll.SchemeTheory.FiniteEtale.UniversalHomeomorphismFullyFaithful
Mathlib.FieldTheory.PurelyInseparable.Basic

Imported by3

theorem

purelyInseparable_specMap_universallyInjective

L19 ↗

EtaleFundamentalGroups.purelyInseparable_specMap_universallyInjective

Documentation

A purely inseparable field extension induces a universally injective map of spectra.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups

Lean source · statement

theorem purelyInseparable_specMap_universallyInjective
    (k L : Type u) [Field k] [Field L] [Algebra k L] [IsPurelyInseparable k L] :
    UniversallyInjective (Spec.map (CommRingCat.ofHom (algebraMap k L)))

theorem

purelyInseparable_constantField_projection_properties

L33 ↗

EtaleFundamentalGroups.purelyInseparable_constantField_projection_properties

Documentation

The coefficient projection of a purely inseparable extension is an integral, universally injective, surjective scheme morphism.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups

Lean source · full declaration

theorem purelyInseparable_constantField_projection_properties
    (k L : Type u) [Field k] [Field L] [Algebra k L] [IsPurelyInseparable k L]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) :
    let p := pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f
    IsIntegralHom p ∧ UniversallyInjective p ∧ Surjective p := by
  let φ := Spec.map (CommRingCat.ofHom (algebraMap k L))
  let : IsIntegralHom φ := (IsIntegralHom.SpecMap_iff).2
    (Algebra.IsIntegral.isIntegral (R := k))
  let : UniversallyInjective φ := purelyInseparable_specMap_universallyInjective k L
  let : Surjective φ := ⟨fun y ↦ ⟨Classical.choice (inferInstance : Nonempty (Spec (.of L))),
    Subsingleton.elim _ _⟩⟩
  exact ⟨inferInstance,
    MorphismProperty.pullback_snd
      (P := (show MorphismProperty Scheme.{u} from @UniversallyInjective)) φ f inferInstance,
    inferInstance⟩

def

pullbackFullyFaithful_of_purelyInseparable_constant_extension

L55 ↗

AlgebraicGeometry.FiniteEtale.pullbackFullyFaithful_of_purelyInseparable_constant_extension

Documentation

Canonical finite étale pullback is fully faithful for a purely inseparable constant extension, for arbitrary schemes.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace AlgebraicGeometry.FiniteEtale
open EtaleFundamentalGroups

Lean source · statement

def pullbackFullyFaithful_of_purelyInseparable_constant_extension
    (k L : Type u) [Field k] [Field L] [Algebra k L] [IsPurelyInseparable k L]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) :
    (FiniteEtale.pullback (Limits.pullback.snd
      (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)).FullyFaithful

Module documentation

Fully faithful pullback across purely inseparable extensions

Declarations

purelyInseparable_specMap_universallyInjective

purelyInseparable_constantField_projection_properties

pullbackFullyFaithful_of_purelyInseparable_constant_extension