Module

ThickeningFullyFaithful.lean

Nyll.SchemeTheory.FiniteEtale.ThickeningFullyFaithful

7 declarations indexed from sourceView source ↗

Module documentation

Unique lifting to finite étale schemes across thickenings

Affine lifting supplies local maps on the directed cover by affine opens. Affine uniqueness makes these maps compatible, so they glue to a unique global map. In particular, pullback along any surjective closed immersion is fully faithful on finite étale covers.

Imports4

Nyll.SchemeTheory.FiniteEtale.AffineThickening
Mathlib.AlgebraicGeometry.Cover.Directed
Mathlib.AlgebraicGeometry.Gluing
Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Imported by4

instance

finiteEtaleInfStableUnderBaseChangeThickening

L31 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleInfStableUnderBaseChangeThickening

Source context 4 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

instance finiteEtaleInfStableUnderBaseChangeThickening :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale)

theorem

affine_existsUnique_lift

L36 ↗

AlgebraicGeometry.FiniteEtale.affine_existsUnique_lift

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeThickening :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf

Lean source · statement

theorem affine_existsUnique_lift
    {X Y Z S : Scheme.{u}} [IsAffine Y]
    (i : X ⟶ Y) [IsClosedImmersion i] [Surjective i]
    (p : Z ⟶ S) [IsFinite p] [Etale p]
    (g : Y ⟶ S) (s : X ⟶ Z) (hs : s ≫ p = i ≫ g) :
    ∃! t : Y ⟶ Z, t ≫ p = g ∧ i ≫ t = s

theorem

existsUnique_lift_of_surjective_closedImmersion

L106 ↗

AlgebraicGeometry.FiniteEtale.existsUnique_lift_of_surjective_closedImmersion

Documentation

A map to a finite étale scheme lifts uniquely across a surjective closed immersion.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeThickening :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf

Lean source · statement

theorem existsUnique_lift_of_surjective_closedImmersion
    {X Y Z S : Scheme.{u}}
    (i : X ⟶ Y) [IsClosedImmersion i] [Surjective i]
    (p : Z ⟶ S) [IsFinite p] [Etale p]
    (g : Y ⟶ S) (s : X ⟶ Z) (hs : s ≫ p = i ≫ g) :
    ∃! t : Y ⟶ Z, t ≫ p = g ∧ i ≫ t = s

theorem

pullback_map_bijective_to_finiteEtale

L163 ↗

AlgebraicGeometry.FiniteEtale.pullback_map_bijective_to_finiteEtale

Documentation

Pullback across a thickening preserves all maps into a finite étale object, even when the source object is an arbitrary scheme over the base.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeThickening :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf

Lean source · statement

theorem pullback_map_bijective_to_finiteEtale
    {X Y : Scheme.{u}} (i : X ⟶ Y) [IsClosedImmersion i] [Surjective i]
    (T V : CategoryTheory.Over Y) [IsFinite V.hom] [Etale V.hom] :
    Function.Bijective ((CategoryTheory.Over.pullback i).map (X := T) (Y := V))

theorem

pullback_full_of_surjective_closedImmersion

L201 ↗

AlgebraicGeometry.FiniteEtale.pullback_full_of_surjective_closedImmersion

Documentation

Finite étale pullback along a surjective closed immersion is full.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeThickening :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf

Lean source · statement

theorem pullback_full_of_surjective_closedImmersion
    {X Y : Scheme.{u}} (i : X ⟶ Y) [IsClosedImmersion i] [Surjective i] :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ i).Full

theorem

pullback_faithful_of_surjective_closedImmersion

L215 ↗

AlgebraicGeometry.FiniteEtale.pullback_faithful_of_surjective_closedImmersion

Documentation

Finite étale pullback along a surjective closed immersion is faithful.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeThickening :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf

Lean source · statement

theorem pullback_faithful_of_surjective_closedImmersion
    {X Y : Scheme.{u}} (i : X ⟶ Y) [IsClosedImmersion i] [Surjective i] :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ i).Faithful

def

pullback_fullyFaithful_of_surjective_closedImmersion

L229 ↗

AlgebraicGeometry.FiniteEtale.pullback_fullyFaithful_of_surjective_closedImmersion

Documentation

The fully faithful structure on finite étale pullback along a thickening.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeThickening :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf

Lean source · statement

def pullback_fullyFaithful_of_surjective_closedImmersion
    {X Y : Scheme.{u}} (i : X ⟶ Y) [IsClosedImmersion i] [Surjective i] :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ i).FullyFaithful

Module documentation

Unique lifting to finite étale schemes across thickenings

Declarations

finiteEtaleInfStableUnderBaseChangeThickening

affine_existsUnique_lift

existsUnique_lift_of_surjective_closedImmersion

pullback_map_bijective_to_finiteEtale

pullback_full_of_surjective_closedImmersion

pullback_faithful_of_surjective_closedImmersion

pullback_fullyFaithful_of_surjective_closedImmersion