93.14 Deformations of… to 93.17 Smoothings

Section93.14 Deformations of henselizations#

Section 93.14 of the Stacks Project, Tag 0DZA. 3 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DZB, a lemma

Tag 0DZB in the Stacks Project.

Deformation.hasFlatAlgebraLift_henselization_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FlatAlgebraLiftHenselization.lean, line 381. The attribute's comment: “VACUOUS: h0DZ2 cannot be satisfied, so nothing below is evidence for the tag. That hypothesis is Deformation.FlatModuleLiftBaseChangeStatement - Stacks 0DZ2 with the source's hypotheses and M restricted to be finite over P - and it is refuted outright, at universe zero by Deformation.Examples.ArtinSchreier.not_flatModuleLiftBaseChangeStatement of StacksFrontier.Deformation.Examples.Linear.NodalCubicRefutation and at an arbitrary universe by Deformation.Examples.ArtinSchreier.not_flatModuleLiftBaseChangeStatement_ulift of StacksFrontier.Deformation.Examples.Linear.NodalCubicRefutationUniverse; the second covers the universe parameter u appearing below, so the vacuity here is unconditional. Read the module documentation of NodalCubicRefutation for the counterexample; it is stated there and nowhere else. A square-zero variant would not rescue 0DZB, whose hypothesis on A' -> A is nilpotence of the kernel. The open route for 0DZB is its own: Stacks 0DZD's henselization functor, which consumes this lemma, and where the module being lifted comes from a syntomic B_h whose higher Ext kills the obstruction - vanishing that 0DZ2 never assumes. Independently of all that, the henselization of the pair (B, b) is described here by the henselian-pair condition hhens together with its universal property huniv, as in Stacks 0DZC, rather than by a chosen model, and the syntomic hypothesis is the affine reading. See the implementation notes”.

Stacks 0DZB. For a surjection A' → A of Noetherian rings with nilpotent kernel and a finite type flat A-algebra B with A → B_h syntomic for every h in an ideal 𝔟, flat lifts of B to A' exist exactly when flat lifts of the henselization Bʰ of the pair (B, 𝔟) do.

public theorem hasFlatAlgebraLift_henselization_iff
    (h0DZ2 : FlatModuleLiftBaseChangeStatement.{u})
    (A' A B : Type u) [CommRing A'] [CommRing A] [CommRing B]
    [IsNoetherianRing A'] [IsNoetherianRing A] [Algebra A' A] [Algebra A B]
    (hsurjA : Function.Surjective (algebraMap A' A))
    (hnilA : IsNilpotent (RingHom.ker (algebraMap A' A)))
    [Algebra.FiniteType A B] [Module.Flat A B] (b : Ideal B)
    (hsyn : ∀ h ∈ b, Algebra.Syntomic A (Localization.Away h))
    (Bh : Type u) [CommRing Bh] [Algebra B Bh] [Algebra A Bh] [IsScalarTower A B Bh]
    (hhens : HenselianPair Bh (b.map (algebraMap B Bh)))
    (huniv : ∀ (D : Type u) (_ : CommRing D) (K : Ideal D), HenselianPair D K →
      ∀ f : B →+* D, b ≤ K.comap f →
        ∃! g : Bh →+* D, g.comp (algebraMap B Bh) = f ∧
          b.map (algebraMap B Bh) ≤ K.comap g) :
    HasFlatAlgebraLift A' A B ↔ HasFlatAlgebraLift A' A Bh

Deformation.hasFlatAlgebraLift_iff_hasFlatAlgebraLift_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FlatAlgebraLiftHenselizationNilpotent.lean, line 412. The attribute's comment: “The henselization of the pair (B, 𝔟) is described by the henselian-pair condition hhens together with its universal property huniv, as in Stacks 0DZC, rather than by a chosen model; the syntomic hypothesis is the affine reading: the complement of V(𝔟) is covered by the D(h), h ∈ 𝔟. Both published proofs rest on Stacks 0DZ2, which is false; the proof here approximates a flat lift over the henselized presentation by solutions over the polynomial presentation and corrects them one power of the kernel at a time (Artin-Rees plus Stacks 07M8 at every level). See the module docstring.”.

Stacks 0DZB. Let A' → A be a surjective map of Noetherian rings with nilpotent kernel, let A → B be a finite type flat ring map and let 𝔟 ⊆ B be an ideal such that Spec(B) → Spec(A) is syntomic on the complement of V(𝔟), that is A → B_h is syntomic for every h ∈ 𝔟. Let (Bʰ, 𝔟ʰ) be the henselization of the pair (B, 𝔟). Then B has a flat lift to A' if and only if Bʰ has a flat lift to A'.

The proof does not go through Stacks 0DZ2 (which is false); see the module documentation.

public theorem hasFlatAlgebraLift_iff_hasFlatAlgebraLift_henselization
    (A' A B : Type u) [CommRing A'] [CommRing A] [CommRing B]
    [IsNoetherianRing A'] [IsNoetherianRing A] [Algebra A' A] [Algebra A B]
    (hsurjA : Function.Surjective (algebraMap A' A))
    (hnilA : IsNilpotent (RingHom.ker (algebraMap A' A)))
    [Algebra.FiniteType A B] [Module.Flat A B] (b : Ideal B)
    (hsyn : ∀ h ∈ b, Algebra.Syntomic A (Localization.Away h))
    (Bh : Type u) [CommRing Bh] [Algebra B Bh] [Algebra A Bh] [IsScalarTower A B Bh]
    (hhens : HenselianPair Bh (b.map (algebraMap B Bh)))
    (huniv : ∀ (D : Type u) (_ : CommRing D) (K : Ideal D), HenselianPair D K →
      ∀ f : B →+* D, b ≤ K.comap f →
        ∃! g : Bh →+* D, g.comp (algebraMap B Bh) = f ∧
          b.map (algebraMap B Bh) ≤ K.comap g) :
    HasFlatAlgebraLift A' A B ↔ HasFlatAlgebraLift A' A Bh
Tag 0DZC, a lemma

Tag 0DZC in the Stacks Project.

Stacks.Deformation.exists_squareZeroAlgebraExtensionClassesHenselizationEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/HenselizationDeformation.lean, line 78.

Stacks 0DZC. Let k be a field, B a finite type k-algebra and J ⊆ B an ideal containing the non-smooth locus of B over k in its vanishing locus, and let (Bʰ, Jʰ) be the henselization of the pair (B, J). For a B-module N with Nʰ = Bʰ ⊗_B N there is a bijection between the isomorphism classes of square-zero extensions of B by N and those of Bʰ by Nʰ, namely the one inducing extension of scalars along B → Bʰ on the groups Ext¹_B(NL_{B/k}, N) and Ext¹_{Bʰ}(NL_{Bʰ/k}, Nʰ) that classify those classes.

public theorem exists_squareZeroAlgebraExtensionClassesHenselizationEquiv
    (k : Type uk) [Field k] (B : Type uB) [CommRing B] [Algebra k B]
    [Algebra.FiniteType k B]
    (J : Ideal B)
    (hsmooth : ∀ q : PrimeSpectrum B, ¬ Algebra.IsSmoothAt k q.asIdeal → J ≤ q.asIdeal)
    (N : Type uN) [AddCommGroup N] [Module B N]
    (Bh : Type uB) [CommRing Bh] [Algebra B Bh] [Algebra k Bh] [IsScalarTower k B Bh]
    (hhens : HenselianPair Bh (J.map (algebraMap B Bh)))
    (huniv : ∀ (C : Type uB) (_ : CommRing C) (JC : Ideal C), HenselianPair C JC →
      ∀ f : B →+* C, J ≤ JC.comap f →
        ∃! g : Bh →+* C, g.comp (algebraMap B Bh) = f ∧
          J.map (algebraMap B Bh) ≤ JC.comap g) :
    ∃ e : SquareZeroExtensionProblem.CompatibleExtension.IsomorphismClasses.{uk, uk, uB, uN,
          max uB uN} (algebraExtensionProblem k B N) ≃
        SquareZeroExtensionProblem.CompatibleExtension.IsomorphismClasses.{uk, uk, uB,
          max uB uN, max uB uN} (algebraExtensionProblem k Bh (Bh ⊗[B] N)),
      ∀ x, extOneCokernelHenselizationFlatBaseChangeEquiv.{uk, uB, uN} k B N Bh J hhens huniv
              (extCokernelIso k Bh (Bh ⊗[B] N)
                (squareZeroAlgebraExtensionClassesEquivExtOne k Bh (Bh ⊗[B] N) (e x)))
            = extCokernelIso k B N (squareZeroAlgebraExtensionClassesEquivExtOne k B N x)
                ⊗ₜ[B] (1 : Bh)
Tag 0DZD, a lemma

Tag 0DZD in the Stacks Project.

Deformation.Examples.bijective_differential_henselizationFunctorData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/HenselizationDifferential.lean, line 446. The attribute's comment: “the second conclusion, the tangent-space assertion, for the map INDUCED by the functor of Stacks 0DYT: Deformation.differential of that functor is bijective, the tangent spaces being those of Stacks 06IH carried by the two deformation categories. Under the tag's own hypotheses and no others: (1) is Algebra.FiniteType k P and (2) is hsm, smoothness of Spec(P) -> Spec(k) at every prime outside V(J). Stated for an arbitrary functor datum of Stacks 0DYT, with no extra hypothesis on the datum. The inputs are the classification of Stacks 0GPT through Stacks 0DY3, the comparison criterion of Stacks 0GPV, the coefficient half of Stacks 0DZC and injectivity of restriction along P -> P^h”.

Stacks 0DZD, the tangent-space conclusion, for the map induced by the functor. Let k be a field, P a finite type k-algebra and J ⊆ P an ideal such that Spec(P) → Spec(k) is smooth on the complement of V(J). The henselization functor 𝓓_P ⟶ 𝓓_{Pʰ} of Stacks 0DYT induces a bijection on tangent spaces.

The proof is the source's: the family of extension classes of Stacks 0DY3 is a bijection of each tangent space with a first Ext group of the naive cotangent complex, by Deformation.Examples.bijective_tangentExtClass; the functor is compatible with those classes through the two comparison maps of Stacks 0GPV, by Deformation.Examples.squareZeroFiberExtClass_henselization; the coefficient comparison is bijective by the henselization half of Stacks 0DZC, in the form Deformation.Examples.bijective_naiveCotangentExtOneMap_tensorCoefficientMap; and restriction along P → Pʰ is injective, by Stacks.Deformation.injective_naiveCotangentExtOneTowerMap_henselization.

public theorem bijective_differential_henselizationFunctorData [Algebra.FiniteType k P]
    (F : HenselizationFunctorData (Λ := Λ) (k := k) (P := P) J)
    (hsm : ∀ q : PrimeSpectrum P, ¬ J ≤ q.asIdeal → Algebra.IsSmoothAt k q.asIdeal) :
    Function.Bijective (differential (𝓕 := ringDeformationBasedCategory Λ k P)
      (𝓖 := ringDeformationBasedCategory Λ k (henselization P J : Type w))
      isCofiberedInGroupoids_ringDeformationProjection
      isCofiberedInGroupoids_ringDeformationProjection F.functor)

Deformation.Examples.bijective_differential_henselizationFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/HenselizationDifferential.lean, line 485. The attribute's comment: “the second conclusion, the tangent-space assertion for the map induced by the functor, at the canonical henselization functor Deformation.Examples.henselizationFunctor of Stacks 0DYT. Under the tag's own hypotheses and no others”.

Stacks 0DZD, the tangent-space conclusion, at the canonical henselization functor. This is Deformation.Examples.bijective_differential_henselizationFunctorData specialized to Deformation.Examples.henselizationFunctor, the functor datum built in the proof of Stacks 0DYT.

public theorem bijective_differential_henselizationFunctor [Algebra.FiniteType k P]
    (hsm : ∀ q : PrimeSpectrum P, ¬ J ≤ q.asIdeal → Algebra.IsSmoothAt k q.asIdeal) :
    Function.Bijective (differential (𝓕 := ringDeformationBasedCategory Λ k P)
      (𝓖 := ringDeformationBasedCategory Λ k (henselization P J : Type w))
      isCofiberedInGroupoids_ringDeformationProjection
      isCofiberedInGroupoids_ringDeformationProjection
      (henselizationFunctor (Λ := Λ) (k := k) J).functor)

Deformation.Examples.isSmooth_henselizationFunctorData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/HenselizationSmooth.lean, line 230. The attribute's comment: “the first conclusion, smoothness: the functor of Stacks 0DYT is smooth. Under the tag's own hypotheses and no others: (1) is Algebra.FiniteType k P and (2) is hsm, smoothness of Spec(P) -> Spec(k) at every prime outside V(J). Stated for an arbitrary functor datum of Stacks 0DYT, with no extra hypothesis on the datum. The criterion of Stacks 0DYP reduces it to surjectivity of the differential, which is Deformation.Examples.bijective_differential_henselizationFunctorData, and to the correspondence of liftability, which is proved here in Deformation.Examples.lifts_henselizationFunctorData -- that is Stacks 0DZB, which Stacks 0DYP needs only across small extensions, whose kernel is square-zero, so the form used is Deformation.hasFlatAlgebraLift_of_hasFlatAlgebraLift_henselization_of_sqZero and NO h0DZ2-style hypothesis is carried”.

Stacks 0DZD, the smoothness conclusion. Let k be a field, P a finite type k-algebra and J ⊆ P an ideal such that Spec(P) → Spec(k) is smooth on the complement of V(J). The henselization functor 𝓓_P ⟶ 𝓓_{Pʰ} of Stacks 0DYT is smooth.

public theorem isSmooth_henselizationFunctorData [Algebra.FiniteType k P]
    (F : HenselizationFunctorData (Λ := Λ) (k := k) (P := P) J)
    (hsm : ∀ q : PrimeSpectrum P, ¬ J ≤ q.asIdeal → Algebra.IsSmoothAt k q.asIdeal) :
    IsSmooth F.functor

Deformation.Examples.isSmooth_henselizationFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/HenselizationSmooth.lean, line 249. The attribute's comment: “the first conclusion, smoothness, at the canonical henselization functor Deformation.Examples.henselizationFunctor of Stacks 0DYT. Under the tag's own hypotheses and no others”.

Stacks 0DZD, the smoothness conclusion, at the canonical henselization functor. This is Deformation.Examples.isSmooth_henselizationFunctorData specialized to Deformation.Examples.henselizationFunctor, the functor datum built in the proof of Stacks 0DYT.

public theorem isSmooth_henselizationFunctor [Algebra.FiniteType k P]
    (hsm : ∀ q : PrimeSpectrum P, ¬ J ≤ q.asIdeal → Algebra.IsSmoothAt k q.asIdeal) :
    IsSmooth (henselizationFunctor (Λ := Λ) (k := k) J).functor

Stacks.Deformation.exists_squareZeroAlgebraExtensionClassesHenselizationTangentEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/HenselizationTangentSpace.lean, line 217. The attribute's comment: “ONLY the second conclusion, that the functor of Stacks 0DYT induces an isomorphism on tangent spaces -- and that in the form the source's own proof produces it, as the case N = B of Stacks 0DZC: the tangent spaces are the groups Ext¹_B(NL_{B/k}, B) and Ext¹_{Bʰ}(NL_{Bʰ/k}, Bʰ ⊗_B B) of Stacks 0DY3, which classify isomorphism classes of square-zero extensions by Stacks 0GPT, and it is those classes the bijection is between. That the bijection is the map INDUCED by the functor of Stacks 0DYT is not established: no naturality comparing Deformation.Examples.henselizationFunctor with the classification of Stacks 0GPT is formalized. No hypothesis the source does not have is carried: Stacks 0DZC is proved outright, base-change input and all -- Stacks 0D08, Stacks 0GPY and flat base change of the conormal cokernel for the comparison of the two Ext groups, and Stacks 00S1 for the J-power torsion of Ext¹_B(NL_{B/k}, N). The FIRST conclusion, that the functor is smooth, is NOT proved at all: it rests on Stacks 0DZ2 through Stacks 0DZB, and the nilpotent devissage needed for 0DZ2 is refuted under 0DZ2's own hypotheses -- it would need Ext¹ to be power torsion, whereas local liftability kills only the Ext² obstruction. See the implementation notes.”.

The case N = B of Stacks 0DZC, in the form this file's Ext comparison produces it. Let k be a field, B a finite type k-algebra and J ⊆ B an ideal containing the non-smooth locus of B over k in its vanishing locus, and let (Bʰ, Jʰ) be the henselization of the pair (B, J). Then the isomorphism classes of square-zero extensions of B by B are in bijection with those of Bʰ by Bʰ ⊗_B B, compatibly with extension of scalars along B → Bʰ on the groups Ext¹_B(NL_{B/k}, B) and Ext¹_{Bʰ}(NL_{Bʰ/k}, Bʰ ⊗_B B) that classify them.

By Stacks 0DY3 those two groups are the tangent spaces of the deformation categories Def_B and Def_{Bʰ}. The tangent-space conclusion of Stacks 0DZD itself is registered on Deformation.Examples.bijective_differential_henselizationFunctorData, for the map the functor of Stacks 0DYT induces; see the section note above for why the attribute is not here.

public theorem exists_squareZeroAlgebraExtensionClassesHenselizationTangentEquiv
    (J : Ideal B)
    (hsmooth : ∀ q : PrimeSpectrum B, ¬ Algebra.IsSmoothAt k q.asIdeal → J ≤ q.asIdeal)
    (Bh : Type uB) [CommRing Bh] [Algebra B Bh] [Algebra k Bh] [IsScalarTower k B Bh]
    (hhens : HenselianPair Bh (J.map (algebraMap B Bh)))
    (huniv : ∀ (C : Type uB) (_ : CommRing C) (JC : Ideal C), HenselianPair C JC →
      ∀ f : B →+* C, J ≤ JC.comap f →
        ∃! g : Bh →+* C, g.comp (algebraMap B Bh) = f ∧
          J.map (algebraMap B Bh) ≤ JC.comap g) :
    ∃ e : SquareZeroExtensionProblem.CompatibleExtension.IsomorphismClasses.{uk, uk, uB, uB,
          uB} (algebraExtensionProblem k B B) ≃
        SquareZeroExtensionProblem.CompatibleExtension.IsomorphismClasses.{uk, uk, uB, uB,
          uB} (algebraExtensionProblem k Bh (Bh ⊗[B] B)),
      ∀ x, extOneCokernelHenselizationFlatBaseChangeEquiv.{uk, uB, uB} k B B Bh J hhens huniv
              (extCokernelIso k Bh (Bh ⊗[B] B)
                (squareZeroAlgebraExtensionClassesEquivExtOne k Bh (Bh ⊗[B] B) (e x)))
            = extCokernelIso k B B (squareZeroAlgebraExtensionClassesEquivExtOne k B B x)
                ⊗ₜ[B] (1 : Bh)
Sources
LeanDeformation.hasFlatAlgebraLift_henselization_iff · Deformation.hasFlatAlgebraLift_iff_hasFlatAlgebraLift_henselization · Stacks.Deformation.exists_squareZeroAlgebraExtensionClassesHenselizationEquiv · Deformation.Examples.bijective_differential_henselizationFunctorData · Deformation.Examples.bijective_differential_henselizationFunctor · Deformation.Examples.isSmooth_henselizationFunctorData · Deformation.Examples.isSmooth_henselizationFunctor · Stacks.Deformation.exists_squareZeroAlgebraExtensionClassesHenselizationTangentEquiv

Section93.15 Application to isolated singularities#

Section 93.15 of the Stacks Project, Tag 0DZE. 1 tag here is carried by 13 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DZF, a lemma

Tag 0DZF in the Stacks Project.

Deformation.Examples.bijective_adicCompletionMap_henselizedLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/IsolatedSingularities.lean, line 157. The attribute's comment: “the identification of the last term of the chain: the completion of the henselization of the local ring is the completion of the local ring, which the source records as the parenthetical the completion of the henselization is the completion. Stated with no hypothesis at all beyond a commutative ring and a prime of it, so in particular without the tag's finite type and smooth-away-from-the-maximal-ideals hypotheses, which this step of the proof does not use”.

Stacks 0DZF. The completion of the local ring P_𝔪 is the completion of its henselization P^h_𝔪: the canonical map induced by P_𝔪 → P^h_𝔪 on adic completions is bijective.

This is the identification of the final term ∏ Def_{P^∧_{𝔪 i}} of the chain of Stacks 0DZF, whose functor out of ∏ Def_{P^h_{𝔪 i}} is completion of the henselization; the source records it as the parenthetical remark that "the completion of the henselization is the completion".

public theorem bijective_adicCompletionMap_henselizedLocalRing
    {P : Type w} [CommRing P] (q : PrimeSpectrum P) :
    Function.Bijective
      (adicCompletionMap (algebraMap (localRingAt q) (henselizedLocalRingAt q))
        (IsLocalRing.maximalIdeal (localRingAt q)) (henselizedMaximalIdealAt q) le_rfl)

Deformation.Examples.bijective_adicCompletion_iInf_to_pi_completedLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/IsolatedSingularities.lean, line 201. The attribute's comment: “the decomposition of the completion used by the proof: the completion of P along the intersection of the maximal ideals 𝔪 1, ..., 𝔪 n is the product of the completions of the local rings P_{𝔪 i}, which the source states as P^ = ∏ P_{𝔪 i}^. Under the tag's own hypotheses on the family: the 𝔪 i are maximal and distinct. Finite type of P and smoothness away from the 𝔪 i are not used by this step and are not assumed”. References: EGA IV (18.6.7), “more general”.

Stacks 0DZF. The completion of P along J = 𝔪 1 ∩ … ∩ 𝔪 n is the product of the completions of the local rings P_{𝔪 i}. This is the step the source states as "P^∧ is ∏ P^∧_{𝔪 i}", and it is what carries the completion leg of the chain from the finite type algebra P to the family of its local rings.

The map is the product of the canonical maps P^∧_J → (P_{𝔪 i})^∧; the proof is the Chinese remainder theorem on the levels P / Jⁿ ≅ ∏ P / 𝔪 iⁿ, by Stacks.AdicCompletion.bijective_adicCompletion_iInf_to_pi, followed by the identification of each 𝔪 i-adic completion of P with the completion of P_{𝔪 i}, by Stacks.AdicCompletion.bijective_adicCompletionMap_localization_atPrime.

public theorem bijective_adicCompletion_iInf_to_pi_completedLocalRing
    {P : Type w} [CommRing P] {ι : Type uι} [Finite ι] (m : ι → PrimeSpectrum P)
    (hmax : ∀ i, (m i).asIdeal.IsMaximal) (hinj : Function.Injective m) :
    Function.Bijective (RingHom.pi fun i =>
      adicCompletionMap (algebraMap P (localRingAt (m i))) (⨅ j, (m j).asIdeal)
        (IsLocalRing.maximalIdeal (localRingAt (m i)))
        ((Ideal.map_mono (iInf_le (fun j => (m j).asIdeal) i)).trans_eq
          (IsLocalization.AtPrime.map_eq_maximalIdeal (m i).asIdeal (localRingAt (m i)))))

Deformation.Examples.exists_ringEquiv_henselization_iInf_pi_henselizedLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/IsolatedSingularities.lean, line 264. The attribute's comment: “the decomposition of the henselization used by the proof: the henselization of the pair (P, J) for J the intersection of the maximal ideals 𝔪 1, ..., 𝔪 n is the product of the henselizations P^h_{𝔪 i} of the local rings, which the source states as P^h = ∏ P^h_{𝔪 i}. Under the tag's own hypotheses on the family: the 𝔪 i are maximal and distinct. Finite type of P and smoothness away from the 𝔪 i are not used by this step and are not assumed”.

Stacks 0DZF. The henselization of the pair (P, J) for J = 𝔪 1 ∩ … ∩ 𝔪 n is the product of the henselizations P^h_{𝔪 i} of the local rings. This is the step the source states as "P^h = ∏ P^h_{𝔪 i}", proved there by looking at idempotents together with More on Algebra, Lemma 15.11.6; it is what carries the henselization leg of the chain from the finite type algebra P to the family of its local rings.

public theorem exists_ringEquiv_henselization_iInf_pi_henselizedLocalRing
    {P : Type w} [CommRing P] {ι : Type uι} [Finite ι] (m : ι → PrimeSpectrum P)
    (hmax : ∀ i, (m i).asIdeal.IsMaximal) (hinj : Function.Injective m) :
    ∃ e : (henselization P (⨅ i, (m i).asIdeal) : Type w) ≃+*
        (∀ i, henselizedLocalRingAt (m i)),
      ∀ (r : P) (i : ι),
        e (algebraMap P (henselization P (⨅ j, (m j).asIdeal) : Type w) r) i =
          algebraMap (localRingAt (m i)) (henselizedLocalRingAt (m i))
            (algebraMap P (localRingAt (m i)) r)

Deformation.Examples.isSmooth_piCompletedLocalRingFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/IsolatedSingularities.lean, line 421. The attribute's comment: “the smoothness half of the source's second step: the composite Def_P -> ∏ Def_{P^∧_{𝔪 i}} of all three maps of the chain is smooth, which the source obtains from Stacks 0DZ5 at P with J = 𝔪 1 ∩ ... ∩ 𝔪 n followed by the decomposition P^∧ = ∏ P^∧_{𝔪 i}. The product of deformation categories is read here as the deformation category of the product ring ∏ P^∧_{𝔪 i}; the identification of that with the product of the deformation categories of the factors is Deformation.Examples.piDeformationFunctor_full and Deformation.Examples.piDeformationFunctor_faithful, and the clause of the tag for the third map of the chain itself is Deformation.Examples.isSmooth_completedLocalRingFunctors. Hypotheses: the tag's own, namely P of finite type over k, the 𝔪 i maximal and distinct, and hsm, smoothness away from V(J) -- which the tag's smooth except at 𝔪 1, ..., 𝔪 n supplies, since every prime not containing J is none of the 𝔪 i”.

Stacks 0DZF, smoothness of the composite of the chain. The map 𝓓_P → ∏ 𝓓_{P^∧_{𝔪 i}} is smooth.

This is the source's second step, in its own order: Stacks 0DZ5 applied to P itself with J = 𝔪 1 ∩ … ∩ 𝔪 n — for which P really is of finite type over k — gives smoothness of 𝓓_P → 𝓓_{P^∧_J}, and the transport of Deformation.Examples.isSmooth_ringDeformationTransport along Deformation.Examples.adicCompletionIInfPiEquiv carries it to the decomposed target.

public theorem isSmooth_piCompletedLocalRingFunctor [Algebra.FiniteType k P]
    (hsm : ∀ q : PrimeSpectrum P, ¬ (⨅ j, (m j).asIdeal) ≤ q.asIdeal →
      Algebra.IsSmoothAt k q.asIdeal) :
    IsSmooth (piCompletedLocalRingFunctor (Λ := Λ) (k := k) m hmax hinj)

Deformation.Examples.bijective_differential_piCompletedLocalRingFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/IsolatedSingularities.lean, line 445. The attribute's comment: “the tangent-space half of the source's second step: the composite Def_P -> ∏ Def_{P^∧_{𝔪 i}} of all three maps of the chain induces an isomorphism on tangent spaces, which the source obtains from Stacks 0DZ5 at P with J = 𝔪 1 ∩ ... ∩ 𝔪 n followed by the decomposition P^∧ = ∏ P^∧_{𝔪 i}. As for smoothness, the product of deformation categories is read as the deformation category of the product ring, the identification of the two being Deformation.Examples.piDeformationFunctor_full and Deformation.Examples.piDeformationFunctor_faithful; the clause of the tag for the third map of the chain itself is Deformation.Examples.bijective_differential_completedLocalRingFunctors. Hypotheses: the tag's own”.

Stacks 0DZF, the tangent-space conclusion for the composite of the chain. The map 𝓓_P → ∏ 𝓓_{P^∧_{𝔪 i}} induces an isomorphism on tangent spaces.

Same route as Deformation.Examples.isSmooth_piCompletedLocalRingFunctor: the tangent-space half of Stacks 0DZ5 at (P, J), carried along the decomposition by Deformation.Examples.bijective_differential_ringDeformationTransport.

public theorem bijective_differential_piCompletedLocalRingFunctor [Algebra.FiniteType k P]
    (hsm : ∀ q : PrimeSpectrum P, ¬ (⨅ j, (m j).asIdeal) ≤ q.asIdeal →
      Algebra.IsSmoothAt k q.asIdeal) :
    Function.Bijective (differential
      (isCofiberedInGroupoids_ringDeformationProjection (Λ := Λ) (k := k) (P := P))
      (isCofiberedInGroupoids_ringDeformationProjection (Λ := Λ) (k := k)
        (P := ∀ i, AdicCompletion (IsLocalRing.maximalIdeal (localRingAt (m i)))
          (localRingAt (m i))))
      (piCompletedLocalRingFunctor (Λ := Λ) (k := k) m hmax hinj))

Deformation.Examples.bijective_differential_localizationFunctors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/IsolatedSingularitiesChain.lean, line 1235. The attribute's comment: “clause 2 of seven: the first map of the chain, Def_P -> ∏ Def_{P_{𝔪 i}}, induces an isomorphism on tangent spaces. Under the tag's own hypotheses and no others: P of finite type over k, the 𝔪 i maximal and pairwise distinct, and every prime at which P is not smooth one of the 𝔪 i. The product of deformation categories is the product over 𝒞_Λ, which is the reading the proof of Stacks 0DZN records. The index type is required to live in the universe of P; any finite family can be reindexed into it”.

Stacks 0DZF, clause 2. The first map Def_P → ∏ Def_{P_{𝔪 i}} of the chain induces an isomorphism on tangent spaces.

public theorem bijective_differential_localizationFunctors [Algebra.FiniteType k P] :
    Function.Bijective (differential
      (isCofiberedInGroupoids_ringDeformationProjection (Λ := Λ) (k := k) (P := P))
      (isCofiberedInGroupoids_pi_ringDeformation (Λ := Λ) (k := k) fun i => localRingAt (m i))
      (localizationFunctors (Λ := Λ) (k := k) m))

Deformation.Examples.isSmooth_localizationFunctors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/IsolatedSingularitiesChain.lean, line 1253. The attribute's comment: “clause 1 of seven: the first map of the chain, Def_P -> ∏ Def_{P_{𝔪 i}}, is smooth. Under the tag's own hypotheses and no others. Obtained from the criterion of Stacks 0DYP: its differential is surjective by clause 2, and a deformation of P lifts along a small extension whenever its image under the composite of the first two maps does, which is smoothness of that composite”.

Stacks 0DZF, clause 1. The first map Def_P → ∏ Def_{P_{𝔪 i}} of the chain is smooth.

public theorem isSmooth_localizationFunctors [Algebra.FiniteType k P] :
    IsSmooth (localizationFunctors (Λ := Λ) (k := k) m)

Deformation.Examples.isSmooth_henselizationFunctors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/IsolatedSingularitiesChain.lean, line 1268. The attribute's comment: “clause 3 of seven: the second map of the chain, ∏ Def_{P_{𝔪 i}} -> ∏ Def_{P^h_{𝔪 i}}, is smooth. Under the tag's own hypotheses and no others. Obtained by cancelling the first map out of the composite of the first two: the first map is smooth by clause 1, hence essentially surjective”.

Stacks 0DZF, clause 3. The second map ∏ Def_{P_{𝔪 i}} → ∏ Def_{P^h_{𝔪 i}} of the chain is smooth.

public theorem isSmooth_henselizationFunctors [Algebra.FiniteType k P] :
    IsSmooth (henselizationFunctors (Λ := Λ) (k := k) m)

Deformation.Examples.bijective_differential_henselizationFunctors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/IsolatedSingularitiesChain.lean, line 1281. The attribute's comment: “clause 4 of seven: the second map of the chain, ∏ Def_{P_{𝔪 i}} -> ∏ Def_{P^h_{𝔪 i}}, induces an isomorphism on tangent spaces. Under the tag's own hypotheses and no others. Obtained by cancelling the first map, which is bijective on tangent spaces by clause 2, out of the composite of the first two”.

Stacks 0DZF, clause 4. The second map ∏ Def_{P_{𝔪 i}} → ∏ Def_{P^h_{𝔪 i}} of the chain induces an isomorphism on tangent spaces.

public theorem bijective_differential_henselizationFunctors [Algebra.FiniteType k P] :
    Function.Bijective (differential
      (isCofiberedInGroupoids_pi_ringDeformation (Λ := Λ) (k := k) fun i => localRingAt (m i))
      (isCofiberedInGroupoids_pi_ringDeformation (Λ := Λ) (k := k)
        fun i => henselizedLocalRingAt (m i))
      (henselizationFunctors (Λ := Λ) (k := k) m))

Deformation.Examples.isSmooth_completedLocalRingFunctors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/IsolatedSingularitiesChain.lean, line 1305. The attribute's comment: “clause 5 of seven: the third map of the chain, ∏ Def_{P^h_{𝔪 i}} -> ∏ Def_{P^∧_{𝔪 i}}, is smooth, with the target the tag's own -- the completions of the local rings, not of the henselizations, the two being identified by Deformation.Examples.bijective_adicCompletionMap_henselizedLocalRing, which is the source's parenthetical the completion of the henselization is the completion. Under the tag's own hypotheses and no others. Obtained by cancelling the composite of the first two maps, which is smooth, out of the composite of all three”.

Stacks 0DZF, clause 5. The third map ∏ Def_{P^h_{𝔪 i}} → ∏ Def_{P^∧_{𝔪 i}} of the chain is smooth. The target is the tag's own: the deformation categories of the completions of the local rings, which the completions of the henselizations are by Deformation.Examples.bijective_adicCompletionMap_henselizedLocalRing.

public theorem isSmooth_completedLocalRingFunctors [Algebra.FiniteType k P] :
    IsSmooth (completedLocalRingFunctors (Λ := Λ) (k := k) m)

Deformation.Examples.bijective_differential_completedLocalRingFunctors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/IsolatedSingularitiesChain.lean, line 1319. The attribute's comment: “clause 6 of seven: the third map of the chain, ∏ Def_{P^h_{𝔪 i}} -> ∏ Def_{P^∧_{𝔪 i}}, induces an isomorphism on tangent spaces, with the target the tag's own -- the completions of the local rings. Under the tag's own hypotheses and no others. Obtained by cancelling the composite of the first two maps out of the composite of all three”.

Stacks 0DZF, clause 6. The third map ∏ Def_{P^h_{𝔪 i}} → ∏ Def_{P^∧_{𝔪 i}} of the chain induces an isomorphism on tangent spaces.

public theorem bijective_differential_completedLocalRingFunctors [Algebra.FiniteType k P] :
    Function.Bijective (differential
      (isCofiberedInGroupoids_pi_ringDeformation (Λ := Λ) (k := k)
        fun i => henselizedLocalRingAt (m i))
      (isCofiberedInGroupoids_pi_ringDeformation (Λ := Λ) (k := k) fun i =>
        AdicCompletion (IsLocalRing.maximalIdeal (localRingAt (m i))) (localRingAt (m i)))
      (completedLocalRingFunctors (Λ := Λ) (k := k) m))

Deformation.Examples.finiteDimensional_artinianTangentSpace_chain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/IsolatedSingularitiesChain.lean, line 1343. The attribute's comment: “clause 7 of seven: the tangent spaces of all four terms of the chain are finite dimensional over k, which is the tag's finite dimensional tangent spaces. Under the tag's own hypotheses and no others -- in particular the finiteness of the non-smooth locus that Stacks 0DY4 wants is derived here from the tag's smooth except at 𝔪 1, ..., 𝔪 n. The source's tangent space is Ext¹_P(NL_{P/k}, P) by Stacks 0DY3; the other three are carried along by clauses 2, 4 and 6, each differential being k-linear by Stacks 06IJ”.

Stacks 0DZF, clause 7. All four tangent spaces along the chain are finite dimensional over k. The source's is Ext¹_P(NL_{P/k}, P) by Stacks 0DY3 and is finite dimensional by Stacks 0DY4(2); the other three are carried along by the tangent-space isomorphisms of clauses 2, 4 and 6, each of which is k-linear by Stacks 06IJ.

public theorem finiteDimensional_artinianTangentSpace_chain
    {ι : Type w} [Finite ι] (m : ι → PrimeSpectrum P) [Algebra.FiniteType k P]
    (hmax : ∀ i, (m i).asIdeal.IsMaximal) (hinj : Function.Injective m)
    (hsm : ∀ q : PrimeSpectrum P, ¬ Algebra.IsSmoothAt k q.asIdeal → ∃ i, m i = q) :
    letI : Fact (IsPredeformationCategory (ringDeformationBasedCategory Λ k P).p) :=
      ⟨(ringDeformationCategory_isDeformationCategory P).predeformation⟩
    letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
      (isomorphismClasses (ringDeformationBasedCategory Λ k P)
        isCofiberedInGroupoids_ringDeformationProjection))) :=
      ⟨schlessingerConditionS2_ringDeformation Λ k P⟩
    letI : Fact (IsPredeformationCategory
        (piBasedCategory fun i => ringDeformationBasedCategory Λ k (localRingAt (m i))).p) :=
      ⟨(isDeformationCategory_pi_ringDeformation (Λ := Λ) (k := k)
        fun i => localRingAt (m i)).predeformation⟩
    letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
      (isomorphismClasses (piBasedCategory fun i =>
          ringDeformationBasedCategory Λ k (localRingAt (m i)))
        (isCofiberedInGroupoids_pi_ringDeformation fun i => localRingAt (m i))))) :=
      ⟨schlessingerConditionS2_pi_ringDeformation (Λ := Λ) (k := k) fun i => localRingAt (m i)⟩
    letI : Fact (IsPredeformationCategory
        (piBasedCategory fun i =>
          ringDeformationBasedCategory Λ k (henselizedLocalRingAt (m i))).p) :=
      ⟨(isDeformationCategory_pi_ringDeformation (Λ := Λ) (k := k)
        fun i => henselizedLocalRingAt (m i)).predeformation⟩
    letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
      (isomorphismClasses (piBasedCategory fun i =>
          ringDeformationBasedCategory Λ k (henselizedLocalRingAt (m i)))
        (isCofiberedInGroupoids_pi_ringDeformation fun i => henselizedLocalRingAt (m i))))) :=
      ⟨schlessingerConditionS2_pi_ringDeformation (Λ := Λ) (k := k)
        fun i => henselizedLocalRingAt (m i)⟩
    letI : Fact (IsPredeformationCategory
        (piBasedCategory fun i => ringDeformationBasedCategory Λ k
          (AdicCompletion (IsLocalRing.maximalIdeal (localRingAt (m i)))
            (localRingAt (m i)))).p) :=
      ⟨(isDeformationCategory_pi_ringDeformation (Λ := Λ) (k := k) fun i =>
        AdicCompletion (IsLocalRing.maximalIdeal (localRingAt (m i)))
          (localRingAt (m i))).predeformation⟩
    letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
      (isomorphismClasses (piBasedCategory fun i => ringDeformationBasedCategory Λ k
          (AdicCompletion (IsLocalRing.maximalIdeal (localRingAt (m i))) (localRingAt (m i))))
        (isCofiberedInGroupoids_pi_ringDeformation fun i =>
          AdicCompletion (IsLocalRing.maximalIdeal (localRingAt (m i)))
            (localRingAt (m i)))))) :=
      ⟨schlessingerConditionS2_pi_ringDeformation (Λ := Λ) (k := k) fun i =>
        AdicCompletion (IsLocalRing.maximalIdeal (localRingAt (m i))) (localRingAt (m i))⟩
    FiniteDimensional k (artinianTangentSpace Λ k
        (isomorphismClasses (ringDeformationBasedCategory Λ k P)
          isCofiberedInGroupoids_ringDeformationProjection)) ∧
      FiniteDimensional k (artinianTangentSpace Λ k
        (isomorphismClasses (piBasedCategory fun i =>
            ringDeformationBasedCategory Λ k (localRingAt (m i)))
          (isCofiberedInGroupoids_pi_ringDeformation fun i => localRingAt (m i)))) ∧
      FiniteDimensional k (artinianTangentSpace Λ k
        (isomorphismClasses (piBasedCategory fun i =>
            ringDeformationBasedCategory Λ k (henselizedLocalRingAt (m i)))
          (isCofiberedInGroupoids_pi_ringDeformation fun i => henselizedLocalRingAt (m i)))) ∧
      FiniteDimensional k (artinianTangentSpace Λ k
        (isomorphismClasses (piBasedCategory fun i => ringDeformationBasedCategory Λ k
            (AdicCompletion (IsLocalRing.maximalIdeal (localRingAt (m i))) (localRingAt (m i))))
          (isCofiberedInGroupoids_pi_ringDeformation fun i =>
            AdicCompletion (IsLocalRing.maximalIdeal (localRingAt (m i)))
              (localRingAt (m i)))))

Deformation.Examples.nonempty_basedIso_adicCompletionFunctor_completionFunctors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/IsolatedSingularitiesCompletionComparison.lean, line 666. The attribute's comment: “the identification the source's proof makes when, after applying Stacks 0DZ5 to P itself with J = 𝔪 1 ∩ ... ∩ 𝔪 n, it says P^ = ∏ P^_{𝔪 i}: completing a deformation along J and transporting along a ring isomorphism P^∧_J ≅ ∏ (P^h_{𝔪 i})^∧ is isomorphic, over 𝒞_Λ, to localizing at each 𝔪 i, henselizing, completing, and reading the family as a deformation of the product ring. Hypotheses: the tag's own on the family -- the 𝔪 i maximal and distinct -- plus P of finite type over k, and the ring isomorphism together with its description on elements of P, which are inputs rather than existentials”.

The comparison of Stacks 0DZF for the completion leg. Completing a deformation of P along J = 𝔪 1 ∩ … ∩ 𝔪 n and then transporting along a ring isomorphism P^∧_J ≅ ∏ (P^h_{𝔪 i})^∧ gives the same functor over 𝒞_Λ as localizing at each 𝔪 i, henselizing, completing each henselized local ring, and reading the resulting family as a deformation of the product ring.

This is the step the source of Stacks 0DZF makes when, having applied Stacks 0DZ5 to P itself — where the finite type hypothesis genuinely holds — it says "P^∧ = ∏ P^∧_{𝔪 i}". The ring isomorphism and its description on elements coming from P are hypotheses, so a caller may supply the one it already has; Deformation.Examples.adicCompletionPiHenselizedEquiv, Deformation.Examples.algebraMap_adicCompletionPiHenselizedEquiv and Deformation.Examples.apply_algebraMap_adicCompletionPiHenselizedEquiv are such a triple.

public theorem nonempty_basedIso_adicCompletionFunctor_completionFunctors
    {ι : Type w} [Finite ι] [Algebra.FiniteType k P] [IsNoetherianRing P]
    (m : ι → PrimeSpectrum P) (hmax : ∀ i, (m i).asIdeal.IsMaximal)
    (hinj : Function.Injective m)
    (e : AdicCompletion (⨅ j, (m j).asIdeal) P ≃+*
      (∀ i, AdicCompletion (henselizedMaximalIdealAt (m i)) (henselizedLocalRingAt (m i))))
    (he : ∀ a : k, e (algebraMap k (AdicCompletion (⨅ j, (m j).asIdeal) P) a) =
      algebraMap k (∀ i, AdicCompletion (henselizedMaximalIdealAt (m i))
        (henselizedLocalRingAt (m i))) a)
    (hchar : ∀ (x : P) (i : ι),
      e (algebraMap P (AdicCompletion (⨅ j, (m j).asIdeal) P) x) i =
        algebraMap (henselizedLocalRingAt (m i))
          (AdicCompletion (henselizedMaximalIdealAt (m i)) (henselizedLocalRingAt (m i)))
          (algebraMap (localRingAt (m i)) (henselizedLocalRingAt (m i))
            (algebraMap P (localRingAt (m i)) x))) :
    Nonempty (BasedFunctor.comp
        (adicCompletionFunctor (Λ := Λ) (k := k) P (⨅ j, (m j).asIdeal)).functor
        (ringDeformationTransport e he) ≅
      BasedFunctor.comp (localizationFunctors (Λ := Λ) (k := k) m)
        (BasedFunctor.comp (henselizationFunctors (Λ := Λ) (k := k) m)
          (BasedFunctor.comp (completionFunctors (Λ := Λ) (k := k) m)
            (piDeformationFunctor (Λ := Λ) (k := k) fun i =>
              AdicCompletion (henselizedMaximalIdealAt (m i))
                (henselizedLocalRingAt (m i))))))

Declarations registered for the tag:

  • finiteDimensional_naiveCotangentExtOne registered with add_to_stacks in StacksFrontier/Deformation/Examples/Geometric/IsolatedSingularities.lean, line 469 (StacksFrontier): “the finite-dimensionality of the tangent space of the source Def_P of the chain, which the source's proof obtains from Stacks 0DY4 and which this declaration carries. The tangent space is the group Ext¹_P(NL_{P/k}, P) of Stacks 0DY3. No extra hypothesis: hfinite asks only that the non-smooth locus be finite, which 0DZF's own hypothesis -- smooth except at the maximal ideals 𝔪 1, ..., 𝔪 n -- gives. Finite-dimensionality for all four terms of the chain, which is the tag's own finite dimensional tangent spaces, is Deformation.Examples.finiteDimensional_artinianTangentSpace_chain”.
Sources
LeanDeformation.Examples.bijective_adicCompletionMap_henselizedLocalRing · Deformation.Examples.bijective_adicCompletion_iInf_to_pi_completedLocalRing · Deformation.Examples.exists_ringEquiv_henselization_iInf_pi_henselizedLocalRing · Deformation.Examples.isSmooth_piCompletedLocalRingFunctor · Deformation.Examples.bijective_differential_piCompletedLocalRingFunctor · Deformation.Examples.bijective_differential_localizationFunctors · Deformation.Examples.isSmooth_localizationFunctors · Deformation.Examples.isSmooth_henselizationFunctors

Section93.16 Unobstructed deformation problems#

Section 93.16 of the Stacks Project, Tag 0DZG. 4 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DZH, a lemma

Tag 0DZH in the Stacks Project.

Deformation.Examples.ringDeformationCategory_isSmooth_of_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/RingsUnobstructed.lean, line 282.

Stacks 0DZH. In the setting of Stacks 0DY1, the deformation category of a local complete intersection P over a field k is unobstructed: the structure functor of Deformation.Examples.ringDeformationCategory P to the category of Artinian local Λ-algebras with residue field k is smooth.

public theorem ringDeformationCategory_isSmooth_of_isLocalCompleteIntersection
    {Λ : Type u} {k P : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    [CommRing P] [Algebra k P]
    (hP : IsLocalCompleteIntersection k P) :
    IsSmooth
      (baseProjection
        (Over.forget (residueFieldAlgebra (Λ := Λ) (k := k) P) ⋙
          FlatAlgebraCategory.projection (Λ := Λ) (k := k)))
Tag 0DZN, a lemma

Tag 0DZN in the Stacks Project.

Deformation.Examples.GluingSituation.isSmooth_toChartProductOfCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesTwoOpenCoverSmooth.lean, line 384. The attribute's comment: “clause 1: Def_X ⟶ Def_{P_1} × Def_{P_2} is smooth when U_12 is smooth over k; unconditional, the hypothesis on P_12 being the source's own”.

Stacks Project, Tag 0DZN, first clause. In Situation 0DYY, if U₁₂ → Spec(k) is smooth then Def_X ⟶ Def_{U₁} × Def_{U₂} = Def_{P₁} × Def_{P₂} is smooth.

theorem isSmooth_toChartProductOfCover (hU₁₂ : Algebra.Smooth k S.P₁₂) :
    IsSmooth (toChartProductOfCover S)

Deformation.Examples.GluingSituation.isSmooth_toChartProductOfCover_comp_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesTwoOpenCoverSmooth.lean, line 407. The attribute's comment: “clause 2: Def_X ⟶ Def_{P_2} is smooth when U_12 is smooth over k and U_1 is a local complete intersection over k; unconditional, the hypotheses on P_12 and P_1 being the source's own”.

Stacks Project, Tag 0DZN, second clause. In Situation 0DYY, if U₁₂ → Spec(k) is smooth and U₁ is in addition a local complete intersection over k, then Def_X ⟶ Def_{U₂} = Def_{P₂} is smooth.

theorem isSmooth_toChartProductOfCover_comp_snd (hU₁₂ : Algebra.Smooth k S.P₁₂)
    (hU₁ : IsLocalCompleteIntersection k S.P₁) :
    IsSmooth (BasedFunctor.comp (toChartProductOfCover S)
      (cofiberedProductSnd (ringDeformationCategoryOver Λ k S.P₁)
        (ringDeformationCategoryOver Λ k S.P₂)))
Tag 0DZP, a lemma

Tag 0DZP in the Stacks Project.

Deformation.Examples.isSmooth_localRingFunctors_and_chain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/CurveIsolatedSingularities.lean, line 131.

Let X be a separated scheme of finite type over k with dim X ≤ 1, and let p_i be finitely many distinct closed points of X outside of which X → Spec k is smooth. In the chain of deformation categories Def_X ⟶ ∏ Def_{𝒪_{X, p_i}} ⟶ ∏ Def_{𝒪^h_{X, p_i}} ⟶ ∏ Def_{𝒪^∧_{X, p_i}} the first map is smooth, and the second and third maps are smooth and induce isomorphisms (bijections of k-vector spaces, by Stacks 06IJ) on tangent spaces.

theorem isSmooth_localRingFunctors_and_chain [IsSeparated X.hom] [LocallyOfFiniteType X.hom]
    [QuasiCompact X.hom] (hdim : topologicalKrullDim (X.left : Type u) ≤ 1) [Finite ι]
    (hinj : Function.Injective p) (hclosed : ∀ i, IsClosed ({p i} : Set X.left))
    (hsm : ∀ x : X.left, x ∉ Set.range p → x ∈ X.hom.smoothLocus) :
    letI : ∀ i, Algebra k (X.left.presheaf.stalk (p i)) := fun i => stalkAlgebraOver X (p i)
    haveI : IsLocallyNoetherian X.left := LocallyOfFiniteType.isLocallyNoetherian X.hom
    IsSmooth (localRingFunctors (Λ := Λ) X p) ∧
      IsSmooth (stalkHenselizationFunctors (Λ := Λ) X p) ∧
      Function.Bijective (differential
        (isCofiberedInGroupoids_pi_ringDeformation (Λ := Λ) (k := k)
          fun i => X.left.presheaf.stalk (p i))
        (isCofiberedInGroupoids_pi_ringDeformation (Λ := Λ) (k := k)
          fun i => (henselization (X.left.presheaf.stalk (p i))
            (IsLocalRing.maximalIdeal (X.left.presheaf.stalk (p i))) : Type u))
        (stalkHenselizationFunctors (Λ := Λ) X p)) ∧
      IsSmooth (stalkCompletionFunctors (Λ := Λ) X p) ∧
      Function.Bijective (differential
        (isCofiberedInGroupoids_pi_ringDeformation (Λ := Λ) (k := k)
          fun i => (henselization (X.left.presheaf.stalk (p i))
            (IsLocalRing.maximalIdeal (X.left.presheaf.stalk (p i))) : Type u))
        (isCofiberedInGroupoids_pi_ringDeformation (Λ := Λ) (k := k)
          fun i => AdicCompletion (IsLocalRing.maximalIdeal (X.left.presheaf.stalk (p i)))
            (X.left.presheaf.stalk (p i)))
        (stalkCompletionFunctors (Λ := Λ) X p))
Tag 0DZQ, a lemma

Tag 0DZQ in the Stacks Project.

Deformation.Examples.isSmooth_baseProjection_schemeDeformationCategoryProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesUnobstructed.lean, line 412. The attribute's comment: “carrying four hypotheses this repository cannot discharge, and no others: h09NZ, the existence of an ample invertible sheaf on a Noetherian separated scheme of dimension at most one (Tag 09NZ), which is what Tag 0A25 carries; hΛ, the Rim–Schlessinger condition for 𝒞_Λ over itself, which is what Tag 0DZN carries; h0DYZ, Tag 0DYZ in the form Tag 0DZN consumes it, namely the existence of restriction morphisms Def_{P_i} ⟶ Def_{P_12} and of a smooth comparison morphism Def_X ⟶ Def_{P_1} ×_{Def_{P_12}} Def_{P_2} for every gluing situation — this absorbs the identification Def_{U_i} = Def_{P_i} of Tag 0DYX, as Tag 0DZN does; and hsmooth, the affine-local reading of smoothness over a field, which translates smoothness of U_12 ⟶ Spec k into Algebra.Smooth k Γ(X, U_12) as Tag 0DZN asks. The three hypotheses (1), (2), (3) of the source are present in full, scheme-level form; the affine-local reading of (2) is proved here from Tag 01UD and is not carried”.

[Stacks, Tag 0DZQ]. Let X be a scheme over a field k which is separated and of finite type over k, of dimension at most one, a local complete intersection over k, and smooth over k outside a finite set of points. Then the deformation category Def_X of Example 0DY7 is unobstructed: its structure morphism over 𝒞_Λ is smooth.

The proof is the source's. The two-chart cover is Deformation.Examples.exists_affineOpen_cover_avoiding_of_topologicalKrullDim_le_one, applied to the complement of the smooth locus; it produces affine opens U₁, U₂ covering X with U₁ inside the smooth locus, hence with U₁ and U₁₂ smooth over k. Tag 0DZN, clause 2, then makes Def_X ⟶ Def_{P₂} smooth, and Tag 0DZH makes Def_{P₂} ⟶ 𝒞_Λ smooth, P₂ = Γ(X, U₂) being a local complete intersection over k by hypothesis (2); the composite is the structure morphism of Def_X by Deformation.comp_baseProjection.

See the module documentation for a full account of the four carried hypotheses.

theorem isSmooth_baseProjection_schemeDeformationCategoryProjection {Λ k : Type u} [CommRing Λ]
    [Field k] [Algebra Λ k]
    (h09NZ : Stacks.HQuasiProjectiveDimensionOne.AmpleOfNoetherianSeparatedDimLEOne.{u})
    (hΛ : IsDeformationCategory.{u, u, u} (𝟭 (ArtinianLocalAlgCat.{u, u, u} Λ k)))
    (h0DYZ : GluingComparisonSmooth Λ k) (hsmooth : SmoothSectionsOfSmoothAffineOpen.{u} k)
    (X : Over (Spec (CommRingCat.of k))) [IsSeparated X.hom] [LocallyOfFiniteType X.hom]
    [QuasiCompact X.hom] (hdim : topologicalKrullDim (X.left : Type u) ≤ 1)
    (hlci : IsLocalCompleteIntersectionOverField X.hom)
    (hfinite : ((X.hom.smoothLocus : Set X.left)ᶜ).Finite) :
    IsSmooth (baseProjection (schemeDeformationCategoryProjection (Λ := Λ) (k := k) X))

Deformation.Examples.isSmooth_baseProjection_schemeDeformationCategoryProjection_of_lci, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesUnobstructedUnconditional.lean, line 92. References: SGA 7 VI (4.10), “(a)”; SGA 7 VI (4.13), “(b), special case”.

[Stacks, Tag 0DZQ]. Let X be a scheme over a field k which is separated and of finite type over k, of dimension at most one, a local complete intersection over k, and smooth over k outside a finite set of points. Then the deformation category Def_X of Example 0DY7 is unobstructed: its structure morphism over 𝒞_Λ is smooth.

theorem isSmooth_baseProjection_schemeDeformationCategoryProjection_of_lci {Λ k : Type u}
    [CommRing Λ] [Field k] [Algebra Λ k]
    (X : Over (Spec (CommRingCat.of k))) [IsSeparated X.hom] [LocallyOfFiniteType X.hom]
    [QuasiCompact X.hom] (hdim : topologicalKrullDim (X.left : Type u) ≤ 1)
    (hlci : IsLocalCompleteIntersectionOverField X.hom)
    (hfinite : ((X.hom.smoothLocus : Set X.left)ᶜ).Finite) :
    IsSmooth (baseProjection (schemeDeformationCategoryProjection (Λ := Λ) (k := k) X))
Sources
LeanDeformation.Examples.ringDeformationCategory_isSmooth_of_isLocalCompleteIntersection · Deformation.Examples.GluingSituation.isSmooth_toChartProductOfCover · Deformation.Examples.GluingSituation.isSmooth_toChartProductOfCover_comp_snd · Deformation.Examples.isSmooth_localRingFunctors_and_chain · Deformation.Examples.isSmooth_baseProjection_schemeDeformationCategoryProjection · Deformation.Examples.isSmooth_baseProjection_schemeDeformationCategoryProjection_of_lci

Section93.17 Smoothings#

Section 93.17 of the Stacks Project, Tag 0E7S. 7 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0E7T, a lemma

Tag 0E7T in the Stacks Project.

Deformation.Examples.SmoothingCriterion.smooth_genericFibre_of_pow_mem_fittingIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SmoothingCriterion.lean, line 540.

Let k be a field, S = Spec k⟦t⟧ and Sₙ = Spec (k⟦t⟧/(t^n)). Let f : Y ⟶ S be proper and flat with Cohen–Macaulay special fibre, equidimensional of dimension d, and let Xₙ = Y ×_S Sₙ with projections pr and gₙ. If for some n ≥ 1 the d-th Fitting ideal of Ω_{Xₙ/Sₙ} contains t ^ (n - 1), then the generic fibre of f, taken over the residue field of the generic point of S, is smooth.

public theorem smooth_genericFibre_of_pow_mem_fittingIdeal (k : Type u) [Field k]
    {Y : Scheme.{u}} (f : Y ⟶ Spec (.of (PowerSeries k))) [IsProper f] [Flat f]
    (d n : ℕ) (hn : 1 ≤ n)
    (hCM : IsCohenMacaulay (f.fiber (IsLocalRing.closedPoint (PowerSeries k))))
    (hequi : TopologicalSpace.Equidimensional
      (f.fiber (IsLocalRing.closedPoint (PowerSeries k))))
    (hdim : topologicalKrullDim (f.fiber (IsLocalRing.closedPoint (PowerSeries k))) =
      (d : WithBot ℕ∞))
    {Xₙ : Scheme.{u}} {pr : Xₙ ⟶ Y}
    {gₙ : Xₙ ⟶ Spec (.of (PowerSeries k ⧸ Ideal.span
      {(PowerSeries.X : PowerSeries k) ^ n}))}
    (hcart : IsPullback pr gₙ f (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk
      (Ideal.span {(PowerSeries.X : PowerSeries k) ^ n})))))
    (hfit : ∀ U : Xₙ.affineOpens,
      (pr ≫ f).appLE ⊤ U.1 (le_preimage_top (pr ≫ f) U.1)
          ((Scheme.ΓSpecIso (.of (PowerSeries k))).inv (PowerSeries.X ^ (n - 1))) ∈
        (fittingIdeal (Scheme.Hom.relativeDifferentials gₙ) (d : ℤ)).ideal U) :
    Smooth (f.fiberToSpecResidueField
      (⟨⊥, inferInstance⟩ : PrimeSpectrum (PowerSeries k)))
Tag 0E7U, a lemma

Tag 0E7U in the Stacks Project.

Deformation.Examples.Smoothing.exists_nonempty_open_smooth_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Smoothing/GenericSmoothness.lean, line 472.

The generic affine-linear deformation is smooth over some nonempty open in the affine space of its coefficients.

public theorem exists_nonempty_open_smooth_projection
    (k : Type u) [Field k] (n c : ℕ) (hc : 1 ≤ c) (hcn : c ≤ n)
    (f : Fin c → MvPolynomial (Fin n) k) :
    let R := parameterRing k n c
    let A := deformedCoordinateRing k n c f
    let π : Spec (.of A) ⟶ Spec (.of R) :=
      Spec.map (CommRingCat.ofHom (algebraMap R A))
    ∃ U : (Spec (.of R)).Opens,
      U ≠ ⊥ ∧ Smooth (π.resLE U (π ⁻¹ᵁ U) le_rfl)
Tag 0E7V, a lemma

Tag 0E7V in the Stacks Project.

Deformation.Examples.Smoothing.exists_flat_powerSeries_specialFiber_smooth_genericFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Smoothing/GlobalCompleteIntersection.lean, line 661. The attribute's comment: “the smoothing of a global complete intersection”.

Stacks 0E7V. A global complete intersection A over a field k is the special fibre B/XB of a flat finite type k⟦X⟧-algebra B whose generic fibre k⸨X⸩ ⊗[k⟦X⟧] B is smooth over k⸨X⸩, and B carries a relative global complete intersection presentation whose number of variables minus number of relations is the Krull dimension of A when A is nonzero.

public theorem exists_flat_powerSeries_specialFiber_smooth_genericFiber
    (k : Type u) [Field k] (A : Type v) [CommRing A] [Algebra k A]
    (hA : IsGlobalCompleteIntersection k A) :
    ∃ (B : Type u) (_ : CommRing B) (_ : Algebra (PowerSeries k) B)
      (_ : Algebra k B) (_ : IsScalarTower k (PowerSeries k) B)
      (_ : Module.Flat (PowerSeries k) B) (_ : Algebra.FiniteType (PowerSeries k) B),
      Nonempty
          ((B ⧸ Ideal.span ({algebraMap (PowerSeries k) B PowerSeries.X} : Set B)) ≃ₐ[k] A) ∧
        Algebra.Smooth (LaurentSeries k)
          (TensorProduct (PowerSeries k) (LaurentSeries k) B) ∧
        ∃ (n c : ℕ) (P : Algebra.Presentation (PowerSeries k) B (Fin n) (Fin c)),
          P.IsRelativeGlobalCompleteIntersection ∧
            (Nontrivial A → ringKrullDim A = ((n - c : ℕ) : WithBot ℕ∞))
Tag 0E7W, a lemma

Tag 0E7W in the Stacks Project.

Deformation.Examples.Smoothing.exists_finite_powerSeries_specialFiber_etale_genericFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Smoothing/FiniteLocalCompleteIntersection.lean, line 378. The attribute's comment: “the smoothing of a finite local complete intersection”.

Stacks 0E7W. A finite-dimensional local complete intersection A over a field k is the special fibre B/XB of a finite flat k⟦X⟧-algebra B whose generic fibre k⸨X⸩ ⊗[k⟦X⟧] B is étale over k⸨X⸩.

public theorem exists_finite_powerSeries_specialFiber_etale_genericFiber
    (k : Type u) [Field k] (A : Type v) [CommRing A] [Algebra k A]
    [FiniteDimensional k A] (hA : IsLocalCompleteIntersection k A) :
    ∃ (B : Type (max u v)) (_ : CommRing B) (_ : Algebra (PowerSeries k) B)
      (_ : Algebra k B) (_ : IsScalarTower k (PowerSeries k) B),
      Module.Finite (PowerSeries k) B ∧ Module.Flat (PowerSeries k) B ∧
        Nonempty
          ((B ⧸ Ideal.span ({algebraMap (PowerSeries k) B PowerSeries.X} : Set B)) ≃ₐ[k] A) ∧
      Algebra.Etale (LaurentSeries k)
          (TensorProduct (PowerSeries k) (LaurentSeries k) B)
Tag 0E7X, a lemma

Tag 0E7X in the Stacks Project.

Deformation.Examples.Smoothing.exists_flat_essFiniteType_specialFiber_pow_mem_fittingIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SmoothingEssFiniteType.lean, line 692.

Stacks 0E7X. Let k be a field and let A be a local k-algebra, essentially of finite type over k and a complete intersection over k. Then A is the special fibre B/tB of a flat k⟦t⟧-algebra B essentially of finite type over k⟦t⟧, and for some n the element t^n lies in the d-th Fitting ideal of Ω_{B/k⟦t⟧}, where d = dim(A) + trdeg_k(κ) for κ the residue field of A.

public theorem exists_flat_essFiniteType_specialFiber_pow_mem_fittingIdeal
    (k : Type u) [Field k] (A : Type v) [CommRing A] [Algebra k A]
    [IsLocalRing A] [Algebra.EssFiniteType k A]
    (hA : IsCompleteIntersectionLocalRing k A) :
    ∃ (dimA trdegResidue n : ℕ),
      ringKrullDim A = (dimA : WithBot ℕ∞) ∧
      Algebra.trdeg k (IsLocalRing.ResidueField A) = trdegResidue ∧
      ∃ (B : Type (max u v)) (_ : CommRing B) (_ : Algebra (PowerSeries k) B)
        (_ : Algebra.EssFiniteType (PowerSeries k) B) (_ : Module.Flat (PowerSeries k) B)
        (_ : Algebra k B) (_ : IsScalarTower k (PowerSeries k) B),
        Nonempty
          ((B ⧸ Ideal.span {algebraMap (PowerSeries k) B PowerSeries.X}) ≃ₐ[k] A) ∧
          algebraMap (PowerSeries k) B (PowerSeries.X ^ n) ∈
            fittingIdeal (M := KaehlerDifferential (PowerSeries k) B)
              ((dimA + trdegResidue : ℕ) : ℤ)
Tag 0E7Y, a lemma

Tag 0E7Y in the Stacks Project.

Deformation.Examples.Smoothing.exists_flat_isProjective_smoothing_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SmoothingProperCurve.lean, line 104.

[Stacks, Tag 0E7Y]. Let X be a scheme over a field k. Assume (1) X is proper over k, (2) X is a local complete intersection over k, (3) X has dimension ≤ 1, and (4) X → Spec(k) is smooth except at finitely many points. Then there exists a flat projective morphism Y → Spec(k[[t]]) whose generic fibre is smooth and whose special fibre is isomorphic to X.

The generic fibre is the fibre over the zero ideal of k⟦t⟧, smooth over its residue field. The special fibre is the base change along Spec k ⟶ Spec k⟦t⟧ given by the constant coefficient, and the isomorphism with X is one of schemes over Spec k. Projectivity is AlgebraicGeometry.IsProjective, [Stacks, Tag 01W8].

theorem exists_flat_isProjective_smoothing_of_isProper {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [IsProper f] (hf : IsLocalCompleteIntersectionOverField f) (hdim : topologicalKrullDim X ≤ 1)
    (hfin : (f.smoothLocus : Set X)ᶜ.Finite) :
    ∃ (Y : Scheme.{u}) (g : Y ⟶ Spec (.of (PowerSeries k))),
      Flat g ∧ AlgebraicGeometry.IsProjective g ∧
      Smooth (g.fiberToSpecResidueField
        (⟨⊥, inferInstance⟩ : PrimeSpectrum (PowerSeries k))) ∧
      ∃ e : X ≅ pullback g
          (Spec.map (CommRingCat.ofHom (PowerSeries.constantCoeff (R := k)))),
        e.hom ≫ pullback.snd g
            (Spec.map (CommRingCat.ofHom (PowerSeries.constantCoeff (R := k)))) = f
Tag 0E7Z, a lemma

Tag 0E7Z in the Stacks Project.

Deformation.Examples.Smoothing.exists_flat_separated_finiteType_smoothing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SmoothingSeparated.lean, line 149.

[Stacks, Tag 0E7Z]. Let k be a field and let X be a scheme over k. Assume (1) X is separated, finite type over k and dim(X) ≤ 1, (2) X is a local complete intersection over k, and (3) X → Spec(k) is smooth except at finitely many points. Then there exists a flat, separated, finite type morphism Y → Spec(k[[t]]) whose generic fibre is smooth and whose special fibre is isomorphic to X.

Finite type is LocallyOfFiniteType together with QuasiCompact. The generic fibre is the fibre over the zero ideal of k⟦t⟧, smooth over its residue field. The special fibre is the base change along Spec k ⟶ Spec k⟦t⟧ given by the constant coefficient, and the isomorphism with X is one of schemes over Spec k.

theorem exists_flat_separated_finiteType_smoothing {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
    (hdim : topologicalKrullDim X ≤ 1) (hlci : IsLocalCompleteIntersectionOverField f)
    (hfin : ((f.smoothLocus : Set X)ᶜ).Finite) :
    ∃ (Y : Scheme.{u}) (g : Y ⟶ Spec (.of (PowerSeries k))),
      Flat g ∧ IsSeparated g ∧ LocallyOfFiniteType g ∧ QuasiCompact g ∧
        Smooth (g.fiberToSpecResidueField
          (⟨⊥, Ideal.isPrime_bot⟩ : PrimeSpectrum (PowerSeries k))) ∧
        ∃ e : X ≅
            pullback g (Spec.map (CommRingCat.ofHom (PowerSeries.constantCoeff (R := k)))),
          e.hom ≫ pullback.snd g
              (Spec.map (CommRingCat.ofHom (PowerSeries.constantCoeff (R := k)))) = f
Sources
LeanDeformation.Examples.SmoothingCriterion.smooth_genericFibre_of_pow_mem_fittingIdeal · Deformation.Examples.Smoothing.exists_nonempty_open_smooth_projection · Deformation.Examples.Smoothing.exists_flat_powerSeries_specialFiber_smooth_genericFiber · Deformation.Examples.Smoothing.exists_finite_powerSeries_specialFiber_etale_genericFiber · Deformation.Examples.Smoothing.exists_flat_essFiniteType_specialFiber_pow_mem_fittingIdeal · Deformation.Examples.Smoothing.exists_flat_isProjective_smoothing_of_isProper · Deformation.Examples.Smoothing.exists_flat_separated_finiteType_smoothing

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.