The standard-smooth lift of a presentation along a closed embedding #
The algebraic core of Kollár's Lemma 41 ([Kol07, Lemma 41]). Kollár writes Y near y as an open
of a hypersurface H ⊂ X × 𝔸^{d+1} after a general projection, extends the coefficients φ_I of
its equation to Φ_I on the ambient A_X and sets A_Y := (Σ Φ_I z^I = 0) ⊂ A_X × 𝔸^{d+1},
smooth over A_X at y. Here the general projection is replaced by Mathlib's local structure of
smooth algebras: S (the ring of Y near y) has a submersive presentation P over R (the
ring of X), S = R[ι]/(f_r) with an invertible Jacobian. Fix a surjective R' → R (the ring of
A_X onto the ring of X).
liftRelation,LiftedQuot: the relationsf_rlifted coefficientwise toF_r ∈ R'[ι](Kollár'sΦ_I), andT := R'[ι]/(F);liftedPre,liftedJac: the same variables give a pre-submersive presentation ofTwith JacobianΔliftingP's.Ambient := T[1/Δ],ambientPres,isStandardSmooth_ambient,isStandardSmoothOfRelativeDimension_ambient: the basic openD(Δ)(Kollár'sA⁰_Y, on which the projection is smooth) is standard smooth of relative dimensionP.dimensionoverR'(the localisation adds one variable and one relation;comp_jacobian_eq_jacobian_smul_jacobian).baseChangeEquiv : R ⊗[R'] T ≃ₐ[R] S,isPushout_liftedQuot: the base change ofTalongR' → RisS, the fibre square of the lemma at the level of rings, throughPresentation.baseChange(the base-changed relations areP's) andPresentation.quotientEquiv.baseChangeEquiv_one_tmul_liftedJac,ambientToS,ambientToS_surjective:Δmaps toP's Jacobian, a unit ofS, soT → Sextends toT[1/Δ] → S, surjective (asR' → Ris):Spec S ↪ D(Δ)is Kollár's closed embeddingj.
The scheme-level assembly (the charts, the Spec square, the shrinking to a surjective h_A) is
Hironaka/Scheme/Smooth/SmoothAmbientLift.lean. Compare [Wlo05, Lemma 4.9.1], the extension of an
étale morphism of embedded affine varieties to the ambient spaces.
A lift of the relation P.relation r ∈ R[ι] to R'[ι] along the coefficientwise surjection
MvPolynomial.map (algebraMap R' R) (Function.surjInv): the coefficients φ_I of the equations
of Y extended to Φ_I on A_X in the proof of [Kol07, Lemma 41].
Equations
- Algebra.StandardSmoothLift.liftRelation hφ P r = Function.surjInv ⋯ (P.relation r)
Instances For
The lifted relation maps back to P.relation r.
The lifted quotient T := R'[ι]/(F_r): Kollár's A_Y as an algebra over Γ(A_X), before
localising, with the standard-smooth equations in place of his single hypersurface equation
([Kol07, Lemma 41], the proof).
Equations
Instances For
The naive pre-submersive presentation of T with P's choice of variables
(PreSubmersivePresentation.naive); its Jacobian is the lift of P's.
Equations
Instances For
The lifted Jacobian determinant Δ ∈ T, which cuts out the smooth locus of A_Y → A_X.
Equations
Instances For
The lifted quotient localised at the lifted Jacobian, T[1/Δ], i.e. the basic open D(Δ) of
Spec T on which the Jacobian is a unit: Kollár's open A⁰_Y on which "the projection
A_Y → A_X is smooth" ([Kol07, Lemma 41], the proof).
Equations
Instances For
The pre-submersive presentation of the ambient over R': the localisation presentation (one
variable w, one relation w·Δ − 1) composed with the lifted one
(PreSubmersivePresentation.comp).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The composite presentation's Jacobian is the unit Δ · Δ of T[1/Δ].
The submersive presentation of the ambient over R'.
Equations
- Algebra.StandardSmoothLift.ambientPres hφ P = { toPreSubmersivePresentation := Algebra.StandardSmoothLift.ambientPre hφ P, jacobian_isUnit := ⋯ }
Instances For
The ambient T[1/Δ] is standard smooth over R': h_A is smooth.
The base change of the lifted quotient is S #
The base change of the lifted presentation along R' → R, a presentation of R ⊗[R'] T over
R.
Equations
Instances For
The base-changed relations are P's.
The base-changed presentation has P's kernel.
R ⊗[R'] R'[ι]/(F) ≃ R[ι]/(P.relation) ≃ S: the fibre square of [Kol07, Lemma 41] at the level
of rings, before localising.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The relative dimension and the image of the lifted Jacobian #
The ambient's presentation has P's dimension (the localisation adds one variable and one
relation): Kollár's relative dimension d.
The ambient is standard smooth of relative dimension P.dimension over R': the constant
relative dimension of h_A.
Under the base change, the class of a lifted polynomial q goes to q evaluated at P's
generators.
The lifted Jacobian maps to P's Jacobian under the base change, a unit of S, so Spec S
lies in D(Δ).
The pushout: S is the base change of the lifted quotient #
The algebra map T → S through the base change, t ↦ e (1 ⊗ t): Kollár's closed embedding
Y ⊂ A_Y at the level of rings, before localising.
Equations
Instances For
The defining formula of liftedToS.
liftedToS is a map of R'-algebras.
The pushout square in CommRingCat: S is the base change of the lifted quotient along
R' → R, so Spec S = Spec R ×_{Spec R'} Spec T (isPullback_SpecMap_of_isPushout).
The ambient localised at the Jacobian maps onto S #
T → S is surjective: every tensor r ⊗ t is 1 ⊗ r' • t since R' → R is surjective.
The lifted Jacobian is a unit in S.
The ring map T[1/Δ] → S extending liftedToS: the closed embedding j : Y⁰ ↪ A⁰_Y of
[Kol07, Lemma 41] at the level of rings.
Equations
Instances For
ambientToS extends liftedToS.
ambientToS on the image of T.
T[1/Δ] → S is surjective: j is a closed immersion.