Module

AffineClosedLift.lean

Nyll.SchemeTheory.Etale.AffineClosedLift

1 declaration indexed from sourceView source ↗

Module documentation

Affine étale lifts across closed immersions

An affine étale scheme over a closed subscheme of an affine scheme lifts to an affine étale scheme over the ambient scheme. We apply the shared algebraic lifting theorem to the actual maps on global sections and use the spectrum of the tensor product to construct the base-change isomorphism over the closed subscheme. No nilpotence, noetherian, or field hypothesis is needed.

Imports7

Nyll.SchemeTheory.FiniteEtale.Algebra.EtaleQuotientLift
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Imported by2

theorem

exists_affine_lift_of_closedImmersion

L39 ↗

AlgebraicGeometry.Etale.exists_affine_lift_of_closedImmersion

Documentation

An affine étale scheme over an affine closed subscheme lifts to the ambient affine scheme, with an isomorphism over the closed subscheme after base change.

Source context 5 commands

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

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

Lean source · statement

theorem exists_affine_lift_of_closedImmersion
    {X Z W : Scheme.{u}} [IsAffine X] [IsAffine W]
    (i : Z ⟶ X) [IsClosedImmersion i] (f : W ⟶ Z) [Etale f] :
    ∃ (V : Scheme.{u}) (_ : IsAffine V) (g : V ⟶ X), Etale g ∧
      ∃ e : pullback i g ≅ W, e.hom ≫ f = pullback.fst i g

Module documentation

Affine étale lifts across closed immersions

Declarations

exists_affine_lift_of_closedImmersion