29.23 Constructible sets to 29.35 Smooth morphisms
Section29.23 Constructible sets#
Section 29.23 of the Stacks Project, Tag 054H. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 054I, a lemma
Tag 054I in the Stacks Project.
AlgebraicGeometry.isLocallyConstructible_preimage, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FinitePresentation/Constructible.lean, line 63. The attribute's comment: “locally constructible case”. References: EGA IV (1.8.2), “locally constructible”; EGA IV (9.2.2), “Forward implication only”.
Stacks Project, Tag 054I. The inverse image of a locally constructible subset under a morphism of schemes is locally constructible.
public lemma isLocallyConstructible_preimage {X Y : Scheme.{u}} (f : X ⟶ Y)
{s : Set Y} (hs : IsLocallyConstructible s) :
IsLocallyConstructible (f ⁻¹' s)
Tag 05LW, a lemma
Tag 05LW in the Stacks Project.
AlgebraicGeometry.mem_nhds_of_isLocallyConstructible_of_specializes_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FinitePresentation/Constructible.lean, line 85. References: EGA 0 (9.2.5), “sufficiency”; SGA 3 XV (3.3), “partial”.
Stacks Project, Tag 05LW. A locally constructible subset of a scheme that contains every generalization of
xcontains an open neighbourhood ofx.
public theorem mem_nhds_of_isLocallyConstructible_of_specializes_subset
{X : Scheme.{u}} {E : Set X} {x : X} (hE : IsLocallyConstructible E)
(h : {x' : X | x' ⤳ x} ⊆ E) :
E ∈ 𝓝 x
Sources
Section29.24 Open morphisms#
Section 29.24 of the Stacks Project, Tag 01TZ. 6 tags here are carried by 6 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 01U0, a definition
Tag 01U0 in the Stacks Project.
Declarations registered for the tag:
IsOpenMapregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 308 (StacksFrontier): “(1), open:IsOpenMap f.base, which Mathlib writestopologically @IsOpenMap f”. References: EGA I (2.2.6); EGA IV (1.10.4); SGA 1 IV (6.6).AlgebraicGeometry.UniversallyOpenregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 311 (StacksFrontier): “(2), universally open”. References: EGA III (4.3.11); EGA IV (14.3.1); EGA IV (14.4.9); EGA IV (2.4.2).
Tag 01U1, a lemma
Tag 01U1 in the Stacks Project.
AlgebraicGeometry.isOpenMap_of_liftsGeneralizations, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Open/LiftsGeneralizations.lean, line 50. The attribute's comment: “part (1): locally of finite presentation and generalizations lift implies open”. References: EGA IV (1.10.4), “b) ⇒ a)”; EGA IV (14.1.6), “partial”.
Stacks Project, Tag 01U1, part (1). A morphism of schemes which is locally of finite presentation and along which generalizations lift is open.
public lemma isOpenMap_of_liftsGeneralizations {X S : Scheme.{u}} (f : X ⟶ S)
[LocallyOfFinitePresentation f] (hf : LiftsGeneralizations f) : IsOpenMap f
AlgebraicGeometry.universallyOpen_of_universally_liftsGeneralizations, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Open/LiftsGeneralizations.lean, line 58. The attribute's comment: “part (2): lfp and generalizations lift along every base change implies univ. open”. References: EGA IV (1.10.4), “b) ⇒ a), special case”.
Stacks Project, Tag 01U1, part (2). A morphism of schemes which is locally of finite presentation and along every base change of which generalizations lift is universally open.
public lemma universallyOpen_of_universally_liftsGeneralizations {X S : Scheme.{u}} (f : X ⟶ S)
[LocallyOfFinitePresentation f]
(hf : universally (topologically @LiftsGeneralizations) f) : UniversallyOpen f
Tag 02V2, a lemma
Tag 02V2 in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.UniversallyOpen.instIsStableUnderCompositionSchemeTopologicallyIsOpenMapregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 184 (StacksFrontier): “composition of open morphisms”. References: EGA I (2.2.7).AlgebraicGeometry.UniversallyOpen.instIsStableUnderCompositionSchemeregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 186 (StacksFrontier): “composition of universally open morphisms”. References: EGA IV (14.3.4), “(i), special case”; EGA IV (2.4.3), “(ii), universally open”.
Tag 0383, a lemma
Tag 0383 in the Stacks Project.
AlgebraicGeometry.universallyOpen_of_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Open/OverField.lean, line 41.
Let
kbe a field and letXbe a scheme overk. The structure morphismX ⟶ Spec kis universally open.
public theorem universallyOpen_of_field (k : Type u) [Field k] {X : Scheme.{u}}
(f : X ⟶ Spec (.of k)) : UniversallyOpen f
Tag 040F, a lemma
Tag 040F in the Stacks Project.
AlgebraicGeometry.liftsGeneralizations_of_isOpenMap, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Open/Generizing.lean, line 48. The attribute's comment: “open morphisms”. References: EGA IV (1.10.3), “a) ⇒ b)”; EGA IV (2.3.5), “partial”.
An open morphism of schemes lifts generalizations of points.
public lemma liftsGeneralizations_of_isOpenMap {X Y : Scheme.{u}} (f : X ⟶ Y)
(hf : IsOpenMap f) : LiftsGeneralizations f
AlgebraicGeometry.universally_liftsGeneralizations_of_universallyOpen, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Open/Generizing.lean, line 77. The attribute's comment: “universally open morphisms”. References: EGA IV (2.3.5), “special case”.
A universally open morphism of schemes lifts generalizations after every base change.
public lemma universally_liftsGeneralizations_of_universallyOpen {X Y : Scheme.{u}} (f : X ⟶ Y)
[UniversallyOpen f] : universally (topologically @LiftsGeneralizations) f
Tag 04ZE, a lemma
Tag 04ZE in the Stacks Project.
AlgebraicGeometry.quasiCompact_of_isOpenMap_surjective_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Surjective/QuasiCompact.lean, line 52.
Quasi-compactness of a morphism of schemes descends along an open, surjective morphism of target schemes.
public theorem quasiCompact_of_isOpenMap_surjective_baseChange
{X Y Y' : Scheme.{u}} (f : X ⟶ Y) (g : Y' ⟶ Y)
(hopen : IsOpenMap g.base) [Surjective g]
[QuasiCompact (pullback.snd f g)] : QuasiCompact f
Sources
Section29.25 Submersive morphisms#
Section 29.25 of the Stacks Project, Tag 040G. 2 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 040H, a definition
Tag 040H in the Stacks Project.
AlgebraicGeometry.Submersive, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Submersive.lean, line 63. The attribute's comment: “part (1): submersive”. References: EGA IV (15.7.8); SGA 1 IX (2.1), “submersive”.
Stacks 040H, part (1). A morphism of schemes is submersive when the continuous map of underlying topological spaces is a quotient map, that is submersive in the sense of Stacks 0406, part (2). This is unrelated to the notion of a submersion of differentiable manifolds.
def Submersive : MorphismProperty Scheme.{u}
AlgebraicGeometry.UniversallySubmersive, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Submersive.lean, line 71. The attribute's comment: “part (2): universally submersive”. References: EGA IV (15.7.8); SGA 1 IX (2.1), “univ. submersive”.
Stacks 040H, part (2). A morphism of schemes
f : X ⟶ Yis universally submersive when the base changeY' ×_Y X ⟶ Y'offalong every morphism of schemesY' ⟶ Yis submersive.
def UniversallySubmersive : MorphismProperty Scheme.{u}
Tag 0CET, a lemma
Tag 0CET in the Stacks Project.
AlgebraicGeometry.Submersive.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Submersive.lean, line 95. The attribute's comment: “submersive”.
Stacks 0CET, submersive morphisms. The composition of a pair of submersive morphisms of schemes is submersive.
theorem Submersive.comp {X Y Z : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z}
(hf : Submersive f) (hg : Submersive g) : Submersive (f ≫ g)
AlgebraicGeometry.UniversallySubmersive.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Submersive.lean, line 108. The attribute's comment: “universally submersive”.
Stacks 0CET, universally submersive morphisms. The composition of a pair of universally submersive morphisms of schemes is universally submersive.
theorem UniversallySubmersive.comp {X Y Z : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z}
(hf : UniversallySubmersive f) (hg : UniversallySubmersive g) :
UniversallySubmersive (f ≫ g)
Sources
Section29.26 Flat morphisms#
Section 29.26 of the Stacks Project, Tag 01U2. 15 tags here are carried by 18 declarations of the repository (all in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 01U3, a definition
Tag 01U3 in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.IsFlatAt, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/FlatPoint.lean, line 33 (StacksFrontier): “part (1)”.AlgebraicGeometry.IsFlatOverAt, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/FlatPoint.lean, line 34 (StacksFrontier): “part (2)”.AlgebraicGeometry.Flatregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/FlatPoint.lean, line 35 (StacksFrontier): “part (3)”. References: EGA 0 (6.7.1); EGA IV (2.1.1); SGA 3 III (2.0), “partial”; SGA 7 VII (1.3.8), “flatness of p”.AlgebraicGeometry.IsFlatOver, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/FlatPoint.lean, line 40 (StacksFrontier): “part (4)”.
Tag 01U4, a lemma
Tag 01U4 in the Stacks Project.
AlgebraicGeometry.isFlatOver_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/QuasicoherentCriteria.lean, line 586. The attribute's comment: “flatness characterization”.
For a morphism of schemes
f : X ⟶ Sand a quasi-coherent moduleFonX, the following are equivalent: 1.Fis flat overS; 2. for all affine opensUofXandVofSwithU ≤ f ⁻¹ᵁ V, the sectionsΓ(F, U)are flat overΓ(S, V); 3. there is an open coverVofSand, for eachj, an open coverUoff ⁻¹ᵁ V jsuch that each restriction ofFtoU iis flat overV j; 4. there is an affine open coverVofSand, for eachj, an affine open coverUoff ⁻¹ᵁ V jsuch that eachΓ(F, U i)is flat overΓ(S, V j).
public theorem isFlatOver_tfae {X S : Scheme.{u}} (f : X ⟶ S)
(F : X.Modules) [F.IsQuasicoherent] :
List.TFAE [
IsFlatOver f.toLRSHom.toShHom F,
∀ (U : X.Opens) (_ : IsAffineOpen U) (V : S.Opens) (_ : IsAffineOpen V)
(hUV : U ≤ f ⁻¹ᵁ V),
let : Module Γ(S, V) Γ(F, U) :=
Module.compHom Γ(F, U) (f.appLE V U hUV).hom
Module.Flat Γ(S, V) Γ(F, U),
∃ (J : Type u) (V : J → S.Opens),
IsOpenCover V ∧
∀ j, ∃ (I : Type u) (U : I → X.Opens)
(hU : (⨆ i, U i) = f ⁻¹ᵁ V j),
∀ i, IsFlatOver
(f.resLE (V j) (U i) ((le_iSup U i).trans hU.le)).toLRSHom.toShHom
(F.restrict (U i).ι),
∃ (J : Type u) (V : J → S.Opens),
IsOpenCover V ∧
(∀ j, IsAffineOpen (V j)) ∧
∀ j, ∃ (I : Type u) (U : I → X.Opens)
(hU : (⨆ i, U i) = f ⁻¹ᵁ V j),
(∀ i, IsAffineOpen (U i)) ∧
∀ i,
let hUV : U i ≤ f ⁻¹ᵁ V j := (le_iSup U i).trans hU.le
let : Module Γ(S, V j) Γ(F, U i) :=
Module.compHom Γ(F, U i) (f.appLE (V j) (U i) hUV).hom
Module.Flat Γ(S, V j) Γ(F, U i)]
AlgebraicGeometry.isFlatOver_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/QuasicoherentCriteria.lean, line 696. The attribute's comment: “restriction to open subschemes”.
A module flat over the target remains flat over any compatible open subscheme of the target after restriction to an open of the source.
public theorem isFlatOver_resLE {X S : Scheme.{u}} {f : X ⟶ S}
(F : X.Modules) (hF : IsFlatOver f.toLRSHom.toShHom F)
(U : X.Opens) (V : S.Opens) (hUV : U ≤ f ⁻¹ᵁ V) :
IsFlatOver (f.resLE V U hUV).toLRSHom.toShHom
(F.restrict U.ι)
Tag 01U5, a lemma
Tag 01U5 in the Stacks Project.
AlgebraicGeometry.flat_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/Flat.lean, line 64. The attribute's comment: “moreover: restriction to open subschemes”.
If
fis flat then so is its restrictionU → Vto any opensU ⊆ X,V ⊆ Swithf(U) ⊆ V.
theorem flat_resLE {f : X ⟶ S} (hf : Flat f) (V : S.Opens) (U : X.Opens)
(e : U ≤ f ⁻¹ᵁ V) : Flat (f.resLE V U e)
AlgebraicGeometry.flat_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/Flat.lean, line 76. The attribute's comment: “equivalence of (1), (2), (3) and (4)”.
Flatness of a morphism of schemes can be checked on all pairs of affine opens, on open coverings of target and preimages, or on affine such coverings.
The source defines flatness of
fby flatness of the local ring maps𝒪_{S, f(x)} → 𝒪_{X, x}; this agrees withAlgebraicGeometry.FlatbyAlgebraicGeometry.Flat.iff_flat_stalkMap.
theorem flat_tfae (f : X ⟶ S) :
List.TFAE [
Flat f,
∀ (V : S.affineOpens) (U : X.affineOpens) (e : U.1 ≤ f ⁻¹ᵁ V.1),
(f.appLE V U e).hom.Flat,
∃ 𝒱 : Set S.Opens, sSup 𝒱 = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.Opens, sSup 𝒰 = f ⁻¹ᵁ V ∧
∀ U ∈ 𝒰, ∃ e : U ≤ f ⁻¹ᵁ V, Flat (f.resLE V U e),
∃ 𝒱 : Set S.affineOpens, (⨆ V ∈ 𝒱, V.1) = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.affineOpens,
(⨆ U ∈ 𝒰, U.1) = f ⁻¹ᵁ V.1 ∧ ∀ U ∈ 𝒰, ∃ e : U.1 ≤ f ⁻¹ᵁ V.1,
(f.appLE V U e).hom.Flat]
AlgebraicGeometry.flat_tfae_and_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/Flat.lean, line 96.
The whole statement: the four characterizations of flatness agree, and flatness passes to restrictions to open subschemes.
The source defines flatness of
fby flatness of the local ring maps𝒪_{S, f(x)} → 𝒪_{X, x}; this agrees withAlgebraicGeometry.FlatbyAlgebraicGeometry.Flat.iff_flat_stalkMap.
theorem flat_tfae_and_resLE (f : X ⟶ S) :
List.TFAE [
Flat f,
∀ (V : S.affineOpens) (U : X.affineOpens) (e : U.1 ≤ f ⁻¹ᵁ V.1),
(f.appLE V U e).hom.Flat,
∃ 𝒱 : Set S.Opens, sSup 𝒱 = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.Opens, sSup 𝒰 = f ⁻¹ᵁ V ∧
∀ U ∈ 𝒰, ∃ e : U ≤ f ⁻¹ᵁ V, Flat (f.resLE V U e),
∃ 𝒱 : Set S.affineOpens, (⨆ V ∈ 𝒱, V.1) = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.affineOpens,
(⨆ U ∈ 𝒰, U.1) = f ⁻¹ᵁ V.1 ∧ ∀ U ∈ 𝒰, ∃ e : U.1 ≤ f ⁻¹ᵁ V.1,
(f.appLE V U e).hom.Flat] ∧
(Flat f → ∀ (U : X.Opens) (V : S.Opens) (e : U ≤ f ⁻¹ᵁ V), Flat (f.resLE V U e))
Tag 0FLM, a lemma
Tag 0FLM in the Stacks Project.
AlgebraicGeometry.isFlatOver_pushforward_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/AffinePushforward.lean, line 71.
Stacks Project, Tag 0FLM. A quasi-coherent module on the source of an affine morphism is flat over a base scheme if and only if its direct image is.
public theorem isFlatOver_pushforward_iff {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
[IsAffineHom f] (F : X.Modules) [F.IsQuasicoherent] :
IsFlatOver (f ≫ g).toLRSHom.toShHom F ↔
IsFlatOver g.toLRSHom.toShHom ((Scheme.Modules.pushforward f).obj F)
Tag 01U6, a lemma
Tag 01U6 in the Stacks Project.
AlgebraicGeometry.IsFlatOverAt.comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/Module.lean, line 43.
Flatness of a module over a ringed space at a point is transitive along a flat morphism of target ringed spaces.
public lemma comp {X Y Z : RingedSpace.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
(F : SheafOfModules.{u}
((sheafCompose (Opens.grothendieckTopology X)
(forget₂ CommRingCat.{u} RingCat.{u})).obj X.sheaf)) (x : X)
(hF : AlgebraicGeometry.IsFlatOverAt f F x)
(hY : AlgebraicGeometry.IsFlatAt g (f.hom.base x)) :
AlgebraicGeometry.IsFlatOverAt (f ≫ g) F x
Tag 01U7, a lemma
Tag 01U7 in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.Flat.compregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 314 (StacksFrontier). References: EGA 0 (6.7.5), “Schemes (EGA preschemes)”; EGA IV (2.1.5), “global case Y' = Y”; EGA IV (2.1.6); EGA IV (2.2.11), “(iii), special case”; EGA IV (2.2.13), “(iii)”; EGA IV (6.6.1), “(i): flatness of h = g∘f”; EGA IV (7.3.5), “partial”; SGA 3 VIIB (1.3.3), “(i), special case”.
Tag 01U8, a lemma
Tag 01U8 in the Stacks Project.
AlgebraicGeometry.modulePullback_isFlatOverAt, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/BaseChange.lean, line 167. The attribute's comment: “flatness at a point”. References: EGA IV (2.1.4), “pointwise statement”; SGA 3 V (7.4), “(i) base change”.
The pullback of a quasi-coherent module which is flat over the base at the image of a point is flat over the new base at that point.
public lemma modulePullback_isFlatOverAt
{X S S' X' : Scheme.{u}} {f : X ⟶ S} {g : S' ⟶ S}
{g' : X' ⟶ X} {f' : X' ⟶ S'} (h : IsPullback g' f' f g)
(F : SheafOfModules.{u} (structureSheafRing X.toRingedSpace)) [F.IsQuasicoherent]
(x' : X') (hF : AlgebraicGeometry.IsFlatOverAt f.toLRSHom.toShHom F (g' x')) :
AlgebraicGeometry.IsFlatOverAt f'.toLRSHom.toShHom
((modulePullback g'.toLRSHom.toShHom).obj F) x'
AlgebraicGeometry.modulePullback_isFlatOver, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/BaseChange.lean, line 207. The attribute's comment: “global flatness”. References: EGA IV (2.1.4), “global module case”.
The pullback of a quasi-coherent module flat over the base is flat over the new base.
public lemma modulePullback_isFlatOver
{X S S' X' : Scheme.{u}} {f : X ⟶ S} {g : S' ⟶ S}
{g' : X' ⟶ X} {f' : X' ⟶ S'} (h : IsPullback g' f' f g)
(F : SheafOfModules.{u} (structureSheafRing X.toRingedSpace)) [F.IsQuasicoherent]
(hF : AlgebraicGeometry.IsFlatOver f.toLRSHom.toShHom F) :
AlgebraicGeometry.IsFlatOver f'.toLRSHom.toShHom
((modulePullback g'.toLRSHom.toShHom).obj F)
Tag 01U9, a lemma
Tag 01U9 in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.Flat.isStableUnderBaseChangeregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 317 (StacksFrontier). References: EGA III (7.7.2), “special case”; EGA III (7.9.7), “special case”; EGA IV (11.5.4), “necessity”; EGA IV (2.1.4); EGA IV (2.2.13), “(i)”; EGA IV (2.5.1), “special case”; EGA IV (20.6.9), “flatness of X' over S'”; EGA IV (21.15.9), “partial”; EGA IV (7.3.5), “partial”; SGA 3 III (0.13), “partial”; SGA 3 VIB (10.1), “partial”; SGA 3 VIB (11.1); SGA 3 VIB (2.1.2), “partial”; SGA 3 VIB (3.11), “fiber-flatness”; SGA 3 VIIB (1.3.3), “(iii), special case”; SGA 3 XIX (2.1); SGA 4 Vbis (3.3), “special case”; SGA 6 0 (2.9), “special case”; SGA 6 XII (2.3), “(a)”; SGA 6 XII (4.1), “(1)”; SGA 7 VII (1.3.8), “partial”.
Tag 03HV, a lemma
Tag 03HV in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.Flat.generalizingMapregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 115 (StacksFrontier). References: EGA IV (2.3.4), “(i), special case”; EGA IV (2.3.5), “special case”.
Tag 01UA, a lemma
Tag 01UA in the Stacks Project.
AlgebraicGeometry.universallyOpen_of_flat_of_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/UniversallyOpen.lean, line 144. References: EGA IV (15.2.1); EGA IV (2.4.6); SGA 3 VIB (4.3); SGA 3 XVI (2.1), “more general”; SGA 6 VIII (1.3), “more general”.
Stacks Project, Tag 01UA. A flat morphism of schemes which is locally of finite presentation is universally open.
public theorem universallyOpen_of_flat_of_locallyOfFinitePresentation {X Y : Scheme.{u}}
(f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] : UniversallyOpen f
Tag 0CVT, a lemma
Tag 0CVT in the Stacks Project.
AlgebraicGeometry.universallyOpen_of_isFlatOver_of_supp_eq_univ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/UniversallyOpen.lean, line 114. References: EGA IV (11.3.1), “f|U open”; EGA IV (2.4.6).
Stacks Project, Tag 0CVT. A morphism of schemes locally of finite presentation admitting a finite type quasi-coherent module of full support which is flat over the target is universally open.
public theorem universallyOpen_of_isFlatOver_of_supp_eq_univ {X Y : Scheme.{u}} (f : X ⟶ Y)
[LocallyOfFinitePresentation f] (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
(hsupp : SheafOfModules.supp F = Set.univ)
(hflat : IsFlatOver f.toLRSHom.toShHom F) : UniversallyOpen f
Tag 02JY, a lemma
Tag 02JY in the Stacks Project.
AlgebraicGeometry.Flat.isOpen_iff_isOpen_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/Submersive.lean, line 38. The attribute's comment: “the open half: T is open if and only if f ⁻¹' T is open”.
A subset of the target of a quasi-compact, surjective, flat morphism of schemes is open if and only if its preimage is open.
public theorem Flat.isOpen_iff_isOpen_preimage {T : Set Y} : IsOpen T ↔ IsOpen (f ⁻¹' T)
AlgebraicGeometry.Flat.isClosed_iff_isClosed_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/Submersive.lean, line 44. The attribute's comment: “the closed half: T is closed if and only if f ⁻¹' T is closed”.
A subset of the target of a quasi-compact, surjective, flat morphism of schemes is closed if and only if its preimage is closed.
public theorem Flat.isClosed_iff_isClosed_preimage {T : Set Y} :
IsClosed T ↔ IsClosed (f ⁻¹' T)
Tag 02JZ, a lemma
Tag 02JZ in the Stacks Project.
AlgebraicGeometry.flat_of_comp_of_surjective_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/Descent.lean, line 38. The attribute's comment: “descent of scheme flatness”.
Stacks Project, Tag 02JZ (second global consequence). If
f : X ⟶ Yis surjective and flat andXis flat overS, thenYis flat overS.
public theorem flat_of_comp_of_surjective_flat
{X Y S : Scheme.{u}} (f : X ⟶ Y) (q : Y ⟶ S)
[Surjective f] [Flat f] [Flat (f ≫ q)] : Flat q
AlgebraicGeometry.isFlatOverAt_iff_modulePullback_isFlatOverAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/PullbackFlatness.lean, line 53. The attribute's comment: “pointwise equivalence”.
Stacks Project, Tag 02JZ (pointwise assertion). If
f : X ⟶ Yis flat atx, then a moduleGonYis flat overSatf(x)if and only if its pullback toXis flat overSatx.
public theorem isFlatOverAt_iff_modulePullback_isFlatOverAt
{X Y S : Scheme.{u}} (f : X ⟶ Y) (q : Y ⟶ S)
(G : SheafOfModules.{u} (structureSheafRing Y.toRingedSpace))
(x : X) (hf : AlgebraicGeometry.IsFlatAt f.toLRSHom.toShHom x) :
AlgebraicGeometry.IsFlatOverAt q.toLRSHom.toShHom G (f.base x) ↔
AlgebraicGeometry.IsFlatOverAt (f ≫ q).toLRSHom.toShHom
((modulePullback f.toLRSHom.toShHom).obj G) x
AlgebraicGeometry.isFlatOver_iff_modulePullback_isFlatOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/PullbackFlatness.lean, line 98. The attribute's comment: “global equivalence”.
Stacks Project, Tag 02JZ (first global consequence). Pullback along a surjective flat morphism detects whether a module is flat over the base.
public theorem isFlatOver_iff_modulePullback_isFlatOver
{X Y S : Scheme.{u}} (f : X ⟶ Y) (q : Y ⟶ S)
(G : SheafOfModules.{u} (structureSheafRing Y.toRingedSpace))
[Surjective f] [Flat f] :
AlgebraicGeometry.IsFlatOver q.toLRSHom.toShHom G ↔
AlgebraicGeometry.IsFlatOver (f ≫ q).toLRSHom.toShHom
((modulePullback f.toLRSHom.toShHom).obj G)
Tag 07T9, a lemma
Tag 07T9 in the Stacks Project.
AlgebraicGeometry.Scheme.Modules.schemeTheoreticSupport_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Support/SchemeTheoreticFlatPullback.lean, line 70.
The scheme-theoretic inverse image of the scheme-theoretic support of a finite type quasi-coherent module along a flat morphism is the scheme-theoretic support of its pullback.
theorem schemeTheoreticSupport_pullback {X Y : Scheme.{u}} (f : Y ⟶ X) [Flat f]
(F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] :
schemeTheoreticSupport ((Scheme.Modules.pullback f).obj F) =
(schemeTheoreticSupport F).comap f
Tag 081I, a lemma
Tag 081I in the Stacks Project.
AlgebraicGeometry.ker_pullback_snd_eq_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/SchemeTheoreticImage.lean, line 50. References: EGA IV (2.3.2).
Stacks Project, Tag 081I. The defining ideal sheaf of the scheme-theoretic image of a quasi-compact morphism after flat base change is the inverse image of its defining ideal sheaf.
public theorem ker_pullback_snd_eq_comap {X Y V : Scheme.{u}}
(f : X ⟶ Y) (g : V ⟶ Y) [Flat f] [QuasiCompact g] :
(pullback.snd g f).ker = g.ker.comap f
Sources
Section29.27 Flat closed immersions#
Section 29.27 of the Stacks Project, Tag 04PV. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 04PW, a lemma
Tag 04PW in the Stacks Project.
AlgebraicGeometry.support_bijOn_flat_closedImmersions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/ClosedSubscheme.lean, line 254. The attribute's comment: “bijection”.
Taking the support is a bijection from the flat closed subschemes of a scheme to the closed subsets stable under generalization.
public theorem support_bijOn_flat_closedImmersions (X : Scheme.{u}) :
Set.BijOn (fun I : X.IdealSheafData => I.support)
{I : X.IdealSheafData | Flat I.subschemeι}
{Z : Closeds X | StableUnderGeneralization (Z : Set X)}
AlgebraicGeometry.existsUnique_lift_of_flat_closedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/ClosedSubscheme.lean, line 272. The attribute's comment: “factorization”. References: EGA I (4.1.8), “special case”.
A morphism whose set-theoretic image lies in a flat closed subscheme factors uniquely through it.
public theorem existsUnique_lift_of_flat_closedImmersion {X Y : Scheme.{u}}
(I : X.IdealSheafData) [Flat I.subschemeι] (g : Y ⟶ X)
(hg : Set.range g ⊆ (I.support : Set X)) :
∃! h : Y ⟶ I.subscheme, h ≫ I.subschemeι = g
Tag 0819, a lemma
Tag 0819 in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.IsOpenImmersion.of_flat_of_monoregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 328 (StacksFrontier): “only: f is an open immersion; Mathlib's form assumes flat, locally of finite presentation and mono (a closed immersion is mono). That its image is open and closed is not stated separately”. References: EGA IV (17.9.1), “(b) ⇒ (a)”; EGA IV (17.9.2), “partial”; SGA 1 I (5.1), “special case”; SGA 3 X (3.7), “partial”; SGA 3 XXII (5.4.10), “more general”.
Tag 04PX, a definition
Tag 04PX in the Stacks Project.
AlgebraicGeometry.connectedComponentIdealSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/ClosedSubscheme.lean, line 292.
The canonical closed subscheme structure on the connected component of a point
xof a schemeX: the closed subscheme cut out byconnectedComponent x, which is closed and stable under generalization. It is the unique closed subscheme structure on that component whose closed immersion intoXis flat.
public noncomputable def connectedComponentIdealSheaf {X : Scheme.{u}} (x : X) :
X.IdealSheafData
Tag 053N, a lemma
Tag 053N in the Stacks Project.
AlgebraicGeometry.Scheme.Modules.forall_isFiniteLocallyFree_iff_forall_isOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FiniteFlatLocallyFree.lean, line 193.
Stacks Project, Tag 053N. For a scheme
Xthe following are equivalent: every quasi-coherent𝒪_X-module of finite type which is flat is finite locally free; every closed subset ofXstable under generalization is open.
theorem forall_isFiniteLocallyFree_iff_forall_isOpen (X : Scheme.{u}) :
(∀ F : X.Modules, _root_.SheafOfModules.IsFiniteType.{u, u, u} F → F.IsQuasicoherent →
AlgebraicGeometry.SheafOfModules.IsFlat
(C := TopologicalSpace.Opens X.toTopCat)
(J := Opens.grothendieckTopology X.toTopCat) (O := X.sheaf) F →
AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u}
(R := X.ringCatSheaf) F) ↔
∀ Z : Set X, IsClosed Z → StableUnderGeneralization Z → IsOpen Z
Sources
Section29.28 Generic flatness#
Section 29.28 of the Stacks Project, Tag 0529. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 052A, a proposition
Tag 052A in the Stacks Project.
AlgebraicGeometry.exists_dense_open_flat_finitePresentation_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/GenericFlatnessIntegralBase.lean, line 52. The attribute's comment: “Deduced from the reduced-base Proposition 052B, which the Stacks Project notes supersedes this one, using that an integral scheme is reduced (01ON).”. References: EGA IV (8.9.4), “more general”; EGA IV (6.9.1), “more general”.
Stacks 052A. For a finite type morphism
f : X ⟶ Sto an integral scheme and a finite type quasi-coherent moduleFonX, there is a dense openU ⊆ Ssuch thatX_U → Uis flat and of finite presentation andF|_{X_U}is flat overUand of finite presentation over𝒪_{X_U}. An integral scheme is reduced, so this is a case of generic flatness over a reduced base.
public theorem exists_dense_open_flat_finitePresentation_of_isIntegral
{X S : Scheme.{u}} (f : X ⟶ S) [IsIntegral S]
[LocallyOfFiniteType f] [QuasiCompact f]
(F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] :
∃ U : S.Opens,
Dense (U : Set S) ∧
Flat (f.resLE U (f ⁻¹ᵁ U) le_rfl) ∧
AlgebraicGeometry.FinitePresentation (f.resLE U (f ⁻¹ᵁ U) le_rfl) ∧
AlgebraicGeometry.IsFlatOver
(f.resLE U (f ⁻¹ᵁ U) le_rfl).toLRSHom.toShHom
(F.restrict (f ⁻¹ᵁ U).ι) ∧
(F.restrict (f ⁻¹ᵁ U).ι).IsFinitePresentation
Tag 052B, a proposition
Tag 052B in the Stacks Project.
AlgebraicGeometry.exists_dense_open_flat_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/GenericFlatness.lean, line 1269. References: EGA IV (8.9.4), “more general”.
Stacks Project, Tag 052B. A finite type morphism and a finite type quasi-coherent module become flat and finitely presented over a common dense open of a reduced base.
public theorem exists_dense_open_flat_finitePresentation
{X S : Scheme.{u}} (f : X ⟶ S) [IsReduced S]
[LocallyOfFiniteType f] [QuasiCompact f]
(F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] :
∃ U : S.Opens,
Dense (U : Set S) ∧
Flat (f.resLE U (f ⁻¹ᵁ U) le_rfl) ∧
AlgebraicGeometry.FinitePresentation (f.resLE U (f ⁻¹ᵁ U) le_rfl) ∧
AlgebraicGeometry.IsFlatOver
(f.resLE U (f ⁻¹ᵁ U) le_rfl).toLRSHom.toShHom
(F.restrict (f ⁻¹ᵁ U).ι) ∧
(F.restrict (f ⁻¹ᵁ U).ι).IsFinitePresentation
Sources
Section29.29 Morphisms and dimensions of fibres#
Section 29.29 of the Stacks Project, Tag 02FW. 7 tags here are carried by 17 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02FX, a lemma
Tag 02FX in the Stacks Project.
AlgebraicGeometry.topologicalKrullDimAt_fiber_eq_krullDimOfRing_stalk_add_trdeg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/F6Rank128/FiberDimension.lean, line 50.
Stacks Project, Tag 02FX. For a morphism locally of finite type, the dimension of the fibre at a point is the dimension of the local ring of the fibre there plus the transcendence degree of the residue-field extension.
theorem topologicalKrullDimAt_fiber_eq_krullDimOfRing_stalk_add_trdeg
(f : X ⟶ S) [LocallyOfFiniteType f] (x : X) :
letI := (f.residueFieldMap x).hom.toAlgebra
topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) =
ringKrullDim ((f.fiber (f x)).presheaf.stalk (f.asFiber x)) +
(Cardinal.toENat (Algebra.trdeg (S.residueField (f x)) (X.residueField x)) :
WithBot ℕ∞)
AlgebraicGeometry.topologicalKrullDimAt_fiber_eq_ringKrullDim_stalk_add_trdeg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FiniteOverSmoothInputs/FibreDimensionFormula.lean, line 97. References: EGA IV (17.15.8), “more general”; SGA 1 II (5.8), “n = p + trdeg_k κ(x)”.
For a morphism locally of finite type, the dimension of the fibre at a point is the Krull dimension of the local ring of the fibre there plus the transcendence degree of the residue field extension.
theorem topologicalKrullDimAt_fiber_eq_ringKrullDim_stalk_add_trdeg
{X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] (x : X) :
letI := (f.residueFieldMap x).hom.toAlgebra
topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) =
ringKrullDim ((f.fiber (f x)).presheaf.stalk (f.asFiber x)) +
(Cardinal.toENat (Algebra.trdeg (S.residueField (f x)) (X.residueField x)) :
WithBot ℕ∞)
Tag 02JS, a lemma
Tag 02JS in the Stacks Project.
AlgebraicGeometry.topologicalKrullDimAt_fiber_comp_le_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FibreDimensionBaseChange/Composite.lean, line 153. The attribute's comment: “the inequality”.
For two morphisms locally of finite type, the dimension at a point of a fibre of their composition is at most the sum of the dimensions, at the corresponding points, of the two successive fibres.
theorem topologicalKrullDimAt_fiber_comp_le_add (f : X ⟶ Y) (g : Y ⟶ S)
[LocallyOfFiniteType f] [LocallyOfFiniteType g] (x : X) :
topologicalKrullDimAt ((f ≫ g).fiber ((f ≫ g) x)) ((f ≫ g).asFiber x) ≤
topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) +
topologicalKrullDimAt (g.fiber (g (f x))) (g.asFiber (f x))
AlgebraicGeometry.topologicalKrullDimAt_fiber_comp_eq_add_of_isFlatAt_fiberMapOfComp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FibreDimensionBaseChange/Composite.lean, line 256. The attribute's comment: “equality for a flat morphism of fibres”.
The dimension inequality for a composition is an equality as soon as the induced morphism between the fibres is flat at the point.
theorem topologicalKrullDimAt_fiber_comp_eq_add_of_isFlatAt_fiberMapOfComp (f : X ⟶ Y)
(g : Y ⟶ S) [LocallyOfFiniteType f] [LocallyOfFiniteType g] (x : X)
(hflat : IsFlatAt (fiberMapOfComp f g ((f ≫ g) x)).toLRSHom.toShHom
((f ≫ g).asFiber x)) :
topologicalKrullDimAt ((f ≫ g).fiber ((f ≫ g) x)) ((f ≫ g).asFiber x) =
topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) +
topologicalKrullDimAt (g.fiber (g (f x))) (g.asFiber (f x))
AlgebraicGeometry.topologicalKrullDimAt_fiber_comp_eq_add_of_isFlatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FibreDimensionBaseChange/Composite.lean, line 310. The attribute's comment: “equality when the first morphism is flat”.
The dimension inequality for a composition is an equality as soon as the first morphism is flat at the point.
theorem topologicalKrullDimAt_fiber_comp_eq_add_of_isFlatAt (f : X ⟶ Y) (g : Y ⟶ S)
[LocallyOfFiniteType f] [LocallyOfFiniteType g] (x : X)
(hflat : IsFlatAt f.toLRSHom.toShHom x) :
topologicalKrullDimAt ((f ≫ g).fiber ((f ≫ g) x)) ((f ≫ g).asFiber x) =
topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) +
topologicalKrullDimAt (g.fiber (g (f x))) (g.asFiber (f x))
Tag 02FY, a lemma
Tag 02FY in the Stacks Project.
AlgebraicGeometry.topologicalKrullDimAt_fiber_eq_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FibreDimensionBaseChange/Basic.lean, line 235. The attribute's comment: “part (1)”.
Stacks Project, Tag 02FY part (1). In a fibre product diagram with
flocally of finite type, the fibre of the base changef'has the same dimension atx'as the fibre offhas at the image ofx'.
public theorem topologicalKrullDimAt_fiber_eq_of_isPullback {X' X S' S : Scheme.{u}}
{g' : X' ⟶ X} {f' : X' ⟶ S'} {f : X ⟶ S} {g : S' ⟶ S}
(hsq : IsPullback g' f' f g) [LocallyOfFiniteType f] (x' : X') :
topologicalKrullDimAt ↥(f'.fiber (f' x')) (f'.asFiber x') =
topologicalKrullDimAt ↥(f.fiber (f (g' x'))) (f.asFiber (g' x'))
AlgebraicGeometry.fiberMap_ringKrullDim_stalk_add_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FibreDimensionBaseChange/LocalRing.lean, line 208. The attribute's comment: “local_ring_differences”.
Stacks Project, Tag 02FY part (2). In a fibre product diagram with
flocally of finite type, the dimension of the local ring atx'of the fibre of the induced morphism of fibres, plus the dimension of the local ring ofX_satx = g' x', is the dimension of the local ring ofX'_{s'}atx'.
public theorem fiberMap_ringKrullDim_stalk_add_eq (hsq : IsPullback g' f' f g)
[LocallyOfFiniteType f] (x' : X') :
ringKrullDim (((fiberMap f' g' g f hsq.w (f' x')).fiber
(fiberMap f' g' g f hsq.w (f' x') (f'.asFiber x'))).presheaf.stalk
((fiberMap f' g' g f hsq.w (f' x')).asFiber (f'.asFiber x'))) +
ringKrullDim ((f.fiber (g (f' x'))).presheaf.stalk
(fiberMap f' g' g f hsq.w (f' x') (f'.asFiber x'))) =
ringKrullDim ((f'.fiber (f' x')).presheaf.stalk (f'.asFiber x'))
AlgebraicGeometry.fiberMap_ringKrullDim_stalk_add_trdeg_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FibreDimensionBaseChange/LocalRing.lean, line 229. The attribute's comment: “local_ring_differences”.
Stacks Project, Tag 02FY part (2). The same dimension is the loss of residue-field transcendence degree: the dimension of the local ring at
x'of the fibre of the induced morphism of fibres, plustrdeg_{κ(s')} κ(x'), istrdeg_{κ(s)} κ(x).
public theorem fiberMap_ringKrullDim_stalk_add_trdeg_eq (hsq : IsPullback g' f' f g)
[LocallyOfFiniteType f] (x' : X') :
letI := (f.residueFieldMap (g' x')).hom.toAlgebra
letI := (f'.residueFieldMap x').hom.toAlgebra
ringKrullDim (((fiberMap f' g' g f hsq.w (f' x')).fiber
(fiberMap f' g' g f hsq.w (f' x') (f'.asFiber x'))).presheaf.stalk
((fiberMap f' g' g f hsq.w (f' x')).asFiber (f'.asFiber x'))) +
(Cardinal.toENat (Algebra.trdeg ↥(S'.residueField (f' x')) ↥(X'.residueField x')) :
WithBot ℕ∞) =
(Cardinal.toENat (Algebra.trdeg ↥(S.residueField (f (g' x'))) ↥(X.residueField (g' x'))) :
WithBot ℕ∞)
AlgebraicGeometry.ringKrullDim_stalk_fiber_le_of_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FibreDimensionBaseChange/LocalRing.lean, line 267. The attribute's comment: “local_ring_differences”.
Stacks Project, Tag 02FY part (2). The dimension of the local ring of a fibre cannot drop under base change.
public theorem ringKrullDim_stalk_fiber_le_of_baseChange (hsq : IsPullback g' f' f g)
[LocallyOfFiniteType f] (x' : X') :
ringKrullDim ((f.fiber (g (f' x'))).presheaf.stalk
(fiberMap f' g' g f hsq.w (f' x') (f'.asFiber x'))) ≤
ringKrullDim ((f'.fiber (f' x')).presheaf.stalk (f'.asFiber x'))
AlgebraicGeometry.trdeg_residueField_le_of_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FibreDimensionBaseChange/LocalRing.lean, line 278. The attribute's comment: “local_ring_differences”.
Stacks Project, Tag 02FY part (2). The transcendence degree of the residue-field extension cannot grow under base change.
public theorem trdeg_residueField_le_of_baseChange (hsq : IsPullback g' f' f g)
[LocallyOfFiniteType f] (x' : X') :
letI := (f.residueFieldMap (g' x')).hom.toAlgebra
letI := (f'.residueFieldMap x').hom.toAlgebra
Algebra.trdeg ↥(S'.residueField (f' x')) ↥(X'.residueField x') ≤
Algebra.trdeg ↥(S.residueField (f (g' x'))) ↥(X.residueField (g' x'))
AlgebraicGeometry.exists_pullback_point_preserving_fibre_dimension_and_trdeg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FibreDimensionBaseChange/LocalRing.lean, line 358. The attribute's comment: “zero_difference_lift”.
Stacks Project, Tag 02FY part (3). In a fibre product diagram with
flocally of finite type, lets'be a point ofS'andxa point ofXwith the same imagesinS. Then there is a common liftx'ofxands'toX'at which neither the dimension of the local ring of the fibre nor the transcendence degree of the residue-field extension changes.
public theorem exists_pullback_point_preserving_fibre_dimension_and_trdeg
(hpb : IsPullback g' f' f g) [LocallyOfFiniteType f] (s' : S') (x : X) (h : f x = g s') :
∃ (x' : X') (_hx : g' x' = x) (hs' : f' x' = s'),
ringKrullDim ((f'.fiber s').presheaf.stalk ((f'.fiberHomeo s').symm ⟨x', hs'⟩)) =
ringKrullDim ((f.fiber (g s')).presheaf.stalk
((f.fiberHomeo (g s')).symm ⟨x, h⟩)) ∧
(letI := ((S.residueFieldCongr h).inv ≫ f.residueFieldMap x).hom.toAlgebra
letI := ((S'.residueFieldCongr hs').inv ≫ f'.residueFieldMap x').hom.toAlgebra
Algebra.trdeg ↥(S.residueField (g s')) ↥(X.residueField x) =
Algebra.trdeg ↥(S'.residueField s') ↥(X'.residueField x'))
Tag 02FZ, a lemma
Tag 02FZ in the Stacks Project.
AlgebraicGeometry.isOpen_setOf_fiberDimensionAt_le, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/Openness.lean, line 78. References: EGA IV (13.1.3).
Stacks Project, Tag 02FZ. For a locally finite type morphism of schemes, the locus where the local dimension of the fibre is at most
nis open.
public lemma isOpen_setOf_fiberDimensionAt_le {X S : Scheme.{u}} (f : X ⟶ S)
[LocallyOfFiniteType f] (n : ℕ) :
IsOpen {x : X |
topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) ≤ (n : WithBot ℕ∞)}
Tag 0A3V, a lemma
Tag 0A3V in the Stacks Project.
AlgebraicGeometry.exists_topologicalKrullDim_fiber_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/Bounded.lean, line 78.
Stacks Project, Tag 0A3V. The dimensions of the fibres of a finite-type morphism to a quasi-compact scheme are bounded by a single natural number.
public theorem exists_topologicalKrullDim_fiber_le
{X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [QuasiCompact f]
[CompactSpace Y] :
∃ n : ℕ, ∀ y : Y, topologicalKrullDim (f.fiber y) ≤ n
Tag 02G0, a lemma
Tag 02G0 in the Stacks Project.
AlgebraicGeometry.isRetrocompact_setOf_fiberDimensionAt_le, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/Openness.lean, line 160.
Stacks Project, Tag 02G0. For a morphism of schemes locally of finite presentation, the locus where the local dimension of the fibre is at most
nis retrocompact.
public lemma isRetrocompact_setOf_fiberDimensionAt_le {X S : Scheme.{u}} (f : X ⟶ S)
[LocallyOfFinitePresentation f] (n : ℕ) :
IsRetrocompact {x : X |
topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) ≤ (n : WithBot ℕ∞)}
Tag 06RU, a lemma
Tag 06RU in the Stacks Project.
AlgebraicGeometry.topologicalKrullDimAt_fiber_le_of_specialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/Specialization.lean, line 49. The attribute's comment: “fiber_dimension_monotone”.
Local dimension in a fibre is monotone along a specialization of points with a common image in the base.
public theorem topologicalKrullDimAt_fiber_le_of_specialization {X S : Scheme.{u}}
(f : X ⟶ S) {x x' : X} (hxx' : x ⤳ x') {s : S}
(hx : f x = s) (hx' : f x' = s) :
topologicalKrullDimAt (f.fiber s) ((f.fiberHomeo s).symm ⟨x, hx⟩) ≤
topologicalKrullDimAt (f.fiber s) ((f.fiberHomeo s).symm ⟨x', hx'⟩)
AlgebraicGeometry.ringKrullDim_fiber_stalk_lt_of_specialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/Specialization.lean, line 61. The attribute's comment: “fiber_local_dimension_strict”.
A strict specialization inside a fibre of a locally finite type morphism strictly increases the dimension of the fibre's local ring.
public theorem ringKrullDim_fiber_stalk_lt_of_specialization
{X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
{x x' : X} (hxx' : x ⤳ x') (hne : x ≠ x')
{s : S} (hx : f x = s) (hx' : f x' = s) :
ringKrullDim ((f.fiber s).presheaf.stalk ((f.fiberHomeo s).symm ⟨x, hx⟩)) <
ringKrullDim ((f.fiber s).presheaf.stalk ((f.fiberHomeo s).symm ⟨x', hx'⟩))
AlgebraicGeometry.trdeg_residueField_fiber_lt_of_specialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/SpecializationTrdeg.lean, line 172. The attribute's comment: “part (3): the strict inequality of transcendence degrees trdeg_{κ(s)} κ(x) > trdeg_{κ(s)} κ(x') along a nontrivial specialization x ⤳ x' inside a fibre, for f locally of finite type. Each residue field is a κ(s)-algebra through AlgebraicGeometry.Scheme.Hom.residueFieldMap, and the comparison is between Mathlib's cardinal-valued Algebra.trdeg. Parts (1) and (2) are AlgebraicGeometry.topologicalKrullDimAt_fiber_le_of_specialization and AlgebraicGeometry.ringKrullDim_fiber_stalk_lt_of_specialization.”.
Stacks 06RU, part (3). Let
f : X ⟶ Sbe locally of finite type and letx ⤳ x'be a nontrivial specialization of points ofXlying over the same pointsofS. Then the transcendence degree ofκ(x)overκ(s)is strictly larger than that ofκ(x').
public theorem trdeg_residueField_fiber_lt_of_specialization (f : X ⟶ S)
[LocallyOfFiniteType f] {x x' : X} (hxx' : x ⤳ x') (hne : x ≠ x')
{s : S} (hx : f x = s) (hx' : f x' = s) :
letI : Algebra (S.residueField s) (X.residueField x) :=
((S.residueFieldCongr hx).inv ≫ f.residueFieldMap x).hom.toAlgebra
letI : Algebra (S.residueField s) (X.residueField x') :=
((S.residueFieldCongr hx').inv ≫ f.residueFieldMap x').hom.toAlgebra
Algebra.trdeg (S.residueField s) (X.residueField x') <
Algebra.trdeg (S.residueField s) (X.residueField x)
Sources
Section29.30 Morphisms of given relative dimension#
Section 29.30 of the Stacks Project, Tag 02NI. 6 tags here are carried by 21 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02NJ, a definition
Tag 02NJ in the Stacks Project.
AlgebraicGeometry.RelativeDimensionLEAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/RelativeDimension.lean, line 55. The attribute's comment: “part (1)”.
A locally finite type morphism
f : X ⟶ Shas relative dimension at mostdatx : Xif the local Krull dimension of the fibre overf xat its point corresponding toxis at mostd.
public def RelativeDimensionLEAt {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
(d : ℕ) (x : X) : Prop
AlgebraicGeometry.RelativeDimensionLE, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/RelativeDimension.lean, line 62. The attribute's comment: “part (2)”.
A locally finite type morphism has relative dimension at most
dif it does so at every point of its source.
public abbrev RelativeDimensionLE {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
(d : ℕ) : Prop
AlgebraicGeometry.RelativeDimension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/RelativeDimension.lean, line 69. The attribute's comment: “part (3)”.
A locally finite type morphism has relative dimension
dif every nonempty fibre is equidimensional and has topological Krull dimensiond.
public def RelativeDimension {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
(d : ℕ) : Prop
AlgebraicGeometry.equidimensional_and_topologicalKrullDim_of_relativeDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Correspondences/GraphCodimension.lean, line 88. The attribute's comment: “over a field”.
Over a field, constant fibre dimension
dis equidimensionality of dimensiond. The spectrum of a field has a single point whose residue field is the field itself, so the only nonempty fibre is the scheme itself.
theorem equidimensional_and_topologicalKrullDim_of_relativeDimension (k : Type u) [Field k]
{T : Scheme.{u}} (q : T ⟶ Spec (.of k)) [LocallyOfFiniteType q] [Nonempty T] (d : ℕ)
(h : AlgebraicGeometry.RelativeDimension q d) :
TopologicalSpace.Equidimensional T ∧ topologicalKrullDim T = (d : WithBot ℕ∞)
Tag 02NK, a lemma
Tag 02NK in the Stacks Project.
AlgebraicGeometry.RelativeDimension.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/BaseChange.lean, line 74. The attribute's comment: “relative dimension d”.
Stacks Project, Tag 02NK. Relative dimension
din the sense of Tag 02NJ is preserved by an arbitrary base change: every nonempty fibre of the base change has local dimensiondat each of its points, hence is equidimensional of dimensiond.
public theorem RelativeDimension.of_isPullback {X' X S' S : Scheme.{u}} {g' : X' ⟶ X}
{f' : X' ⟶ S'} {f : X ⟶ S} {g : S' ⟶ S} (hsq : IsPullback g' f' f g)
[LocallyOfFiniteType f] {d : ℕ} (hf : RelativeDimension f d) :
letI : LocallyOfFiniteType f' := MorphismProperty.of_isPullback hsq inferInstance
RelativeDimension f' d
AlgebraicGeometry.RelativeDimensionLE.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/BaseChange.lean, line 98. The attribute's comment: “relative dimension at most d”.
Stacks Project, Tag 02NK. A bound
≤ don the relative dimension in the sense of Tag 02NJ is preserved by an arbitrary base change, because the local dimension of a fibre is unchanged along the square.
public theorem RelativeDimensionLE.of_isPullback {X' X S' S : Scheme.{u}} {g' : X' ⟶ X}
{f' : X' ⟶ S'} {f : X ⟶ S} {g : S' ⟶ S} (hsq : IsPullback g' f' f g)
[LocallyOfFiniteType f] {d : ℕ} (hf : RelativeDimensionLE f d) :
letI : LocallyOfFiniteType f' := MorphismProperty.of_isPullback hsq inferInstance
RelativeDimensionLE f' d
Tag 02NL, a lemma
Tag 02NL in the Stacks Project.
AlgebraicGeometry.RelativeDimensionLE.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/Composition.lean, line 66. The attribute's comment: “the inequality”.
Stacks Project, Tag 02NL. If
fhas relative dimension at mostdandghas relative dimension at moste, thenf ≫ ghas relative dimension at mostd + e.
public theorem RelativeDimensionLE.comp (f : X ⟶ Y) (g : Y ⟶ S) [LocallyOfFiniteType f]
[LocallyOfFiniteType g] {d e : ℕ} (hf : RelativeDimensionLE f d)
(hg : RelativeDimensionLE g e) : RelativeDimensionLE (f ≫ g) (d + e)
AlgebraicGeometry.RelativeDimension.comp_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/Composition.lean, line 79. The attribute's comment: “the exact relative dimension of a flat composition”.
Stacks Project, Tag 02NL. If
fhas relative dimensiond,ghas relative dimensioneandfis flat, thenf ≫ ghas relative dimensiond + e.
public theorem RelativeDimension.comp_of_flat (f : X ⟶ Y) (g : Y ⟶ S) [LocallyOfFiniteType f]
[LocallyOfFiniteType g] [Flat f] {d e : ℕ} (hf : RelativeDimension f d)
(hg : RelativeDimension g e) : RelativeDimension (f ≫ g) (d + e)
Tag 02NM, a lemma
Tag 02NM in the Stacks Project.
AlgebraicGeometry.relativeDimensionFunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/CohenMacaulayRelativeDimension.lean, line 370. The attribute's comment: “relative dimension function”.
The locally constant function giving the relative dimension of a flat, locally finitely presented morphism with Cohen–Macaulay fibres.
public noncomputable def relativeDimensionFunction
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f]
(hCM : ∀ s : S, IsCohenMacaulay (f.fiber s)) : LocallyConstant X ℕ
AlgebraicGeometry.relativeDimensionFunction_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/CohenMacaulayRelativeDimension.lean, line 462. The attribute's comment: “pointwise relative dimension”.
At a point, the relative dimension function is the local Krull dimension of its fibre.
public theorem relativeDimensionFunction_apply
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f]
(hCM : ∀ s : S, IsCohenMacaulay (f.fiber s)) (x : X) :
topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) =
((relativeDimensionFunction f hCM x : ℕ) : WithBot ℕ∞)
AlgebraicGeometry.relativeDimensionOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/CohenMacaulayRelativeDimension.lean, line 474. The attribute's comment: “canonical dimension pieces”.
The canonical open subscheme where the relative dimension is
d.
public def relativeDimensionOpen
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f]
(hCM : ∀ s : S, IsCohenMacaulay (f.fiber s)) (d : ℕ) : X.Opens
AlgebraicGeometry.relativeDimensionOpen_isClopen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/CohenMacaulayRelativeDimension.lean, line 482. The attribute's comment: “canonical pieces are clopen”.
Every canonical relative-dimension piece is open and closed.
public theorem relativeDimensionOpen_isClopen
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f]
(hCM : ∀ s : S, IsCohenMacaulay (f.fiber s)) (d : ℕ) :
IsClopen (relativeDimensionOpen f hCM d : Set X)
AlgebraicGeometry.iSup_relativeDimensionOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/CohenMacaulayRelativeDimension.lean, line 502. The attribute's comment: “canonical pieces cover”.
The canonical relative-dimension pieces cover the source.
public theorem iSup_relativeDimensionOpen
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f]
(hCM : ∀ s : S, IsCohenMacaulay (f.fiber s)) :
⨆ d : ℕ, relativeDimensionOpen f hCM d = ⊤
AlgebraicGeometry.pairwise_disjoint_relativeDimensionOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/CohenMacaulayRelativeDimension.lean, line 517. The attribute's comment: “canonical pieces are disjoint”.
Distinct canonical relative-dimension pieces are disjoint.
public theorem pairwise_disjoint_relativeDimensionOpen
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f]
(hCM : ∀ s : S, IsCohenMacaulay (f.fiber s)) :
Pairwise (Disjoint on relativeDimensionOpen f hCM)
AlgebraicGeometry.relativeDimensionOpen_relativeDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/CohenMacaulayRelativeDimension.lean, line 532. The attribute's comment: “canonical pieces have pure relative dimension”.
The restriction of the morphism to its
d-dimensional locus has relative dimensiond.
public theorem relativeDimensionOpen_relativeDimension
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f]
(hCM : ∀ s : S, IsCohenMacaulay (f.fiber s)) (d : ℕ) :
RelativeDimension ((relativeDimensionOpen f hCM d).ι ≫ f) d
AlgebraicGeometry.exists_clopen_relativeDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/CohenMacaulayRelativeDimension.lean, line 581.
Stacks Project, Tag 02NM. A flat morphism locally of finite presentation with Cohen–Macaulay fibres is the disjoint union of clopen subschemes of pure relative dimension.
public theorem exists_clopen_relativeDimension
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f]
(hCM : ∀ s : S, IsCohenMacaulay (f.fiber s)) :
∃ U : ℕ → X.Opens,
(∀ d : ℕ, IsClopen (U d : Set X)) ∧
(iSup U = ⊤) ∧
Pairwise (Disjoint on U) ∧
(∀ d : ℕ, RelativeDimension ((U d).ι ≫ f) d)
Tag 0397, a lemma
Tag 0397 in the Stacks Project.
AlgebraicGeometry.quasiFiniteAt_of_fiberDimensionAt_le_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/MaxSliceQuasiFinite.lean, line 63. The attribute's comment: “a zero-dimensional fibre point is a quasi-finite point”.
A morphism locally of finite type is quasi-finite at a point whose fibre has local dimension at most zero there: local dimensions are nonnegative, so the bound makes the dimension zero.
public theorem quasiFiniteAt_of_fiberDimensionAt_le_zero {X S : Scheme.{u}}
(f : X ⟶ S) [LocallyOfFiniteType f] (x : X)
(hx : topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) ≤ 0) :
f.QuasiFiniteAt x
AlgebraicGeometry.locallyQuasiFinite_of_relativeDimensionLE_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/MaxSliceQuasiFinite.lean, line 73. The attribute's comment: “relative dimension at most zero implies locally quasi-finite”.
A morphism locally of finite type of relative dimension at most zero is locally quasi-finite.
public theorem locallyQuasiFinite_of_relativeDimensionLE_zero {X S : Scheme.{u}}
(f : X ⟶ S) [LocallyOfFiniteType f] (hf : RelativeDimensionLE f 0) :
LocallyQuasiFinite f
AlgebraicGeometry.quasiFiniteAt_iff_fiberDimensionAt_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/QuasiFinite.lean, line 65. The attribute's comment: “pointwise characterization”.
A morphism locally of finite type is quasi-finite at a point if and only if the local dimension of its fibre at that point is zero.
public theorem quasiFiniteAt_iff_fiberDimensionAt_eq_zero
{X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] (x : X) :
quasiFiniteAt f x ↔
topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) = 0
AlgebraicGeometry.locallyQuasiFinite_iff_relativeDimension_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/QuasiFinite.lean, line 76. The attribute's comment: “global characterization”.
A morphism locally of finite type is locally quasi-finite if and only if it has relative dimension zero.
public theorem locallyQuasiFinite_iff_relativeDimension_zero
{X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] :
LocallyQuasiFinite f ↔ RelativeDimension f 0
Tag 0AFE, a lemma
Tag 0AFE in the Stacks Project.
AlgebraicGeometry.topologicalKrullDimAt_eq_add_of_relativeDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/CohenMacaulayDimensionFormula.lean, line 187.
Stacks Project, Tag 0AFE. A flat morphism locally of finite type of relative dimension
dbetween locally Noetherian schemes raises the local dimension byd:dim_x(X) = dim_{f x}(Y) + d.This is also the input to the dimension formula for a Cohen-Macaulay morphism.
public theorem topologicalKrullDimAt_eq_add_of_relativeDimension {X Y : Scheme.{u}}
[IsLocallyNoetherian X] [IsLocallyNoetherian Y] (f : X ⟶ Y) [Flat f] [LocallyOfFiniteType f]
{d : ℕ} (hf : RelativeDimension f d) (x : X) :
topologicalKrullDimAt X x = topologicalKrullDimAt Y (f x) + (d : WithBot ℕ∞)
Sources
Section29.31 Syntomic morphisms#
Section 29.31 of the Stacks Project, Tag 01UB. 16 tags here are carried by 20 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 01UC, a definition
Tag 01UC in the Stacks Project.
AlgebraicGeometry.SyntomicAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/Defs.lean, line 51. The attribute's comment: “syntomic_at_point”.
A morphism of schemes
f : X ⟶ Sis syntomic atx : Xif there are affine open neighbourhoodsUofxandVoff(x), withf(U) ⊆ V, for which the induced mapΓ(S, V) → Γ(X, U)is syntomic.
def SyntomicAt {X S : Scheme.{u}} (f : X ⟶ S) (x : X) : Prop
AlgebraicGeometry.Syntomic, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/Defs.lean, line 65. The attribute's comment: “syntomic_morphism”.
A morphism of schemes is syntomic if it is syntomic at every point of its source.
abbrev Syntomic {X S : Scheme.{u}} (f : X ⟶ S) : Prop
AlgebraicGeometry.IsStandardSyntomic, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/Defs.lean, line 73. The attribute's comment: “standard_syntomic_morphism”.
A morphism
f : X ⟶ Sof affine schemes is standard syntomic if the induced ring mapΓ(S, ⊤) → Γ(X, ⊤)is a relative global complete intersection. Via the canonical isomorphisms of affine schemes with the spectra of their global sections, this says precisely thatfis isomorphic to the spectrum of a relative global complete intersection.
abbrev IsStandardSyntomic {X S : Scheme.{u}} [IsAffine X] [IsAffine S]
(f : X ⟶ S) : Prop
AlgebraicGeometry.IsLocalCompleteIntersectionOverField, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/Defs.lean, line 100. The attribute's comment: “local_complete_intersection_over_field”.
A scheme over a field is a local complete intersection over the field if its structure morphism to the spectrum of the field is syntomic.
abbrev IsLocalCompleteIntersectionOverField {k : Type u} [Field k] {X : Scheme.{u}}
(f : X ⟶ Spec (.of k)) : Prop
Tag 01UD, a lemma
Tag 01UD in the Stacks Project.
AlgebraicGeometry.syntomic_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/Basic.lean, line 59. The attribute's comment: “syntomic characterization”.
The four characterizations of a syntomic morphism: the global condition, the condition on every compatible pair of affine opens, an open-covering criterion, and an affine-open-covering criterion on rings of sections.
theorem syntomic_tfae {X S : Scheme.{u}} (f : X ⟶ S) :
List.TFAE [
Syntomic f,
∀ (U : X.Opens) (_ : IsAffineOpen U) (V : S.Opens) (_ : IsAffineOpen V)
(hUV : U ≤ f ⁻¹ᵁ V),
letI : Algebra Γ(S, V) Γ(X, U) := (f.appLE V U hUV).hom.toAlgebra
Algebra.Syntomic Γ(S, V) Γ(X, U),
∃ (J : Type u) (V : J → S.Opens),
IsOpenCover V ∧
∀ j, ∃ (I : Type u) (U : I → X.Opens)
(hU : (⨆ i, U i) = f ⁻¹ᵁ V j),
∀ i, Syntomic (f.resLE (V j) (U i) ((le_iSup U i).trans hU.le)),
∃ (J : Type u) (V : J → S.Opens),
IsOpenCover V ∧
(∀ j, IsAffineOpen (V j)) ∧
∀ j, ∃ (I : Type u) (U : I → X.Opens)
(hU : (⨆ i, U i) = f ⁻¹ᵁ V j),
(∀ i, IsAffineOpen (U i)) ∧
∀ i,
let hUV : U i ≤ f ⁻¹ᵁ V j := (le_iSup U i).trans hU.le
letI : Algebra Γ(S, V j) Γ(X, U i) := (f.appLE (V j) (U i) hUV).hom.toAlgebra
Algebra.Syntomic Γ(S, V j) Γ(X, U i)]
AlgebraicGeometry.syntomic_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/Basic.lean, line 123. The attribute's comment: “restriction of a syntomic morphism”.
Restricting a syntomic morphism to compatible open subschemes of its source and target is syntomic.
theorem syntomic_resLE {X S : Scheme.{u}} {f : X ⟶ S}
(hf : Syntomic f) (U : X.Opens) (V : S.Opens) (hUV : U ≤ f ⁻¹ᵁ V) :
Syntomic (f.resLE V U hUV)
Tag 01UH, a lemma
Tag 01UH in the Stacks Project.
AlgebraicGeometry.syntomic_isStableUnderComposition, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/Comp.lean, line 63.
Stacks Project, Tag 01UH. Syntomic morphisms of schemes are stable under composition.
instance syntomic_isStableUnderComposition :
MorphismProperty.IsStableUnderComposition (@Syntomic.{u})
Tag 01UI, a lemma
Tag 01UI in the Stacks Project.
AlgebraicGeometry.syntomic_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/BaseChange.lean, line 39.
Stacks Project, Tag 01UI. A base change of a syntomic morphism is syntomic.
instance syntomic_isStableUnderBaseChange :
MorphismProperty.IsStableUnderBaseChange (@Syntomic : MorphismProperty Scheme.{u})
Tag 01UJ, a lemma
Tag 01UJ in the Stacks Project.
AlgebraicGeometry.syntomic_of_isOpenImmersion, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/OpenImmersion.lean, line 29.
Every open immersion of schemes is syntomic.
lemma syntomic_of_isOpenImmersion {X S : Scheme.{u}} (f : X ⟶ S)
[IsOpenImmersion f] : Syntomic f
Tag 01UK, a lemma
Tag 01UK in the Stacks Project.
AlgebraicGeometry.locallyOfFinitePresentation, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/Properties.lean, line 44.
A syntomic morphism of schemes is locally of finite presentation.
lemma locallyOfFinitePresentation {X S : Scheme.{u}} {f : X ⟶ S}
(hf : Syntomic f) : LocallyOfFinitePresentation f
Tag 01UL, a lemma
Tag 01UL in the Stacks Project.
AlgebraicGeometry.flat, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/Properties.lean, line 58.
A syntomic morphism of schemes is flat.
lemma flat {X S : Scheme.{u}} {f : X ⟶ S} (hf : Syntomic f) : Flat f
Tag 056F, a lemma
Tag 056F in the Stacks Project.
AlgebraicGeometry.universallyOpen_of_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/Properties.lean, line 70.
A syntomic morphism of schemes is universally open.
theorem universallyOpen_of_syntomic {X S : Scheme.{u}} {f : X ⟶ S}
(hf : Syntomic f) : UniversallyOpen f
Tag 01UG, a lemma
Tag 01UG in the Stacks Project.
AlgebraicGeometry.localCompleteIntersection_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/LocalCompleteIntersection.lean, line 194.
Stacks Project, Tag 01UG. For a scheme locally of finite type over a field, being a local complete intersection is equivalent to the existence of affine neighbourhoods with global-complete-intersection coordinate rings, and to all local rings being complete intersections over the field.
theorem localCompleteIntersection_tfae (k : Type u) [Field k]
(X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f] :
let globalCI := fun U : X.Opens ↦
letI : Algebra k Γ(X, U) :=
((Scheme.ΓSpecIso (.of k)).inv ≫ f.appLE ⊤ U (by simp)).hom.toAlgebra
IsGlobalCompleteIntersection k Γ(X, U)
let localCI := fun x : X ↦
letI : Algebra k (X.presheaf.stalk x) :=
((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫
X.presheaf.germ ⊤ x (by simp)).hom.toAlgebra
IsCompleteIntersection k (X.presheaf.stalk x)
List.TFAE [
IsLocalCompleteIntersectionOverField f,
∀ x : X, ∃ U : X.affineOpens, x ∈ U.1 ∧ globalCI U.1,
∀ x : X, localCI x]
Tag 01UE, a lemma
Tag 01UE in the Stacks Project.
AlgebraicGeometry.syntomicAt_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/Local.lean, line 482.
Let
x : Xmap tos : S, and letVbe an affine open neighbourhood ofs. Then the following are equivalent:
fis syntomic atx;- some affine open neighbourhood
Uofx, mapping intoV, makes the restricted morphismU ⟶ Vstandard syntomic;fis of finite presentation atx, its map on local rings is flat, and its local fibre ring atxis a complete intersection overκ(s).
theorem syntomicAt_tfae {X S : Scheme.{u}} (f : X ⟶ S) (x : X)
(V : S.affineOpens) (_hxV : f x ∈ V.1) :
List.TFAE [
SyntomicAt f x,
∃ (U : X.affineOpens) (_ : x ∈ U.1) (hUV : U.1 ≤ f ⁻¹ᵁ V.1),
IsStandardSyntomic (f.resLE V.1 U.1 hUV),
AlgebraicGeometry.FinitePresentationAt f x ∧
(f.stalkMap x).hom.Flat ∧
(let A := S.presheaf.stalk (f x)
let B := X.presheaf.stalk x
letI : Algebra A B := (f.stalkMap x).hom.toAlgebra
IsCompleteIntersection (IsLocalRing.ResidueField A)
(IsLocalRing.ResidueField A ⊗[A] B))]
Tag 01UF, a lemma
Tag 01UF in the Stacks Project.
AlgebraicGeometry.syntomic_of_lci_fibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/FiberCriterion.lean, line 58.
Stacks Project, Tag 01UF. A flat morphism of schemes which is locally of finite presentation and whose every fibre is a local complete intersection over the residue field of its base point is syntomic.
theorem syntomic_of_lci_fibers {X S : Scheme.{u}} (f : X ⟶ S) [Flat f]
[LocallyOfFinitePresentation f]
(hlci : ∀ s : S, IsLocalCompleteIntersectionOverField (f.fiberToSpecResidueField s)) :
Syntomic f
Tag 02V3, a lemma
Tag 02V3 in the Stacks Project.
AlgebraicGeometry.syntomicLocus_eq_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SyntomicBaseChange/Basic.lean, line 129. The attribute's comment: “syntomic locus”.
Stacks Project, Tag 02V3. For a flat morphism locally of finite presentation, the syntomic locus commutes with arbitrary base change: if the square
g',f',f,gis cartesian then the set of points wheref'is syntomic is theg'-preimage of the set of points wherefis syntomic.
theorem syntomicLocus_eq_preimage
(g' : X' ⟶ X) (f' : X' ⟶ S') (f : X ⟶ S) (g : S' ⟶ S) (hpb : IsPullback g' f' f g)
[Flat f] [LocallyOfFinitePresentation f] :
{x' : X' | IsSyntomicAt f' x'} = g' ⁻¹' {x : X | IsSyntomicAt f x}
Declarations registered for the tag:
Stacks.Tag02V3FibreStalk.completeIntersectionFibreStalkLocus_eq_preimage, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/FibreStalk/Basic.lean, line 266 (StacksFrontier): “complete-intersection fibre locus”. References: EGA IV (19.3.4).
Tag 02K0, a lemma
Tag 02K0 in the Stacks Project.
AlgebraicGeometry.fiberDimensionAt_eq_card_sub_card, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/FiberDimension.lean, line 115.
Stacks 02K0. For a presentation
S = R[x₁, …, xₙ]/(f₁, …, fᶜ)which is a relative global complete intersection, the dimension at every point of the fibre ofSpec S → Spec Risn - c.
lemma fiberDimensionAt_eq_card_sub_card
{R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
{ι σ : Type*} [Finite ι] [Finite σ] (P : Algebra.Presentation R S ι σ)
[P.IsRelativeGlobalCompleteIntersection] (x : Spec (.of S)) :
let f : Spec (.of S) ⟶ Spec (.of R) := Spec.map (CommRingCat.ofHom (algebraMap R S))
topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) =
((Nat.card ι - Nat.card σ : ℕ) : WithBot ℕ∞)
Tag 02K1, a lemma
Tag 02K1 in the Stacks Project.
AlgebraicGeometry.isLocallyConstant_fiberDimensionAt, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/FiberDimension.lean, line 177.
The local dimension of the fibre of a syntomic morphism is locally constant on its source.
lemma isLocallyConstant_fiberDimensionAt {X S : Scheme.{u}} (f : X ⟶ S) (hf : Syntomic f) :
IsLocallyConstant (fun x : X => topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x))
Tag 02K2, a definition
Tag 02K2 in the Stacks Project.
AlgebraicGeometry.SyntomicOfRelativeDimension, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/FiberDimension.lean, line 202.
A syntomic morphism whose fibres have local dimension
dat every point.
abbrev SyntomicOfRelativeDimension (d : ℕ) {X S : Scheme.{u}} (f : X ⟶ S) : Prop
Tag 02K3, a lemma
Tag 02K3 in the Stacks Project.
Stacks.Syntomic.syntomic_of_comp_of_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SyntomicLciDescent.lean, line 325.
Stacks Project, Tag 02K3. Let
X ⟶ Y ⟶ Sbe morphisms of schemes withX ⟶ Ysurjective and syntomic and the compositeX ⟶ Ssyntomic. IfY ⟶ Sis locally of finite presentation, thenY ⟶ Sis syntomic.
theorem syntomic_of_comp_of_locallyOfFinitePresentation (f : X ⟶ Y) (q : Y ⟶ S) [Surjective f]
(hf : Syntomic f) (hcomp : Syntomic (f ≫ q)) [LocallyOfFinitePresentation q] :
Syntomic q
Sources
Section29.32 Conormal sheaf of an immersion#
Section 29.32 of the Stacks Project, Tag 01R1. 5 tags here are carried by 28 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 01R2, a definition
Tag 01R2 in the Stacks Project.
Stacks.Conormal.conormalSheaf_isQuasicoherent, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalAlgebra/Sheaf.lean, line 57. The attribute's comment: “quasi-coherence”.
Stacks Project, Tag 01R2. The conormal sheaf of an immersion is quasi-coherent.
instance conormalSheaf_isQuasicoherent {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i] :
(conormalSheaf i).IsQuasicoherent
Stacks.Conormal.conormalSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalComparison/IdealSheafComparison.lean, line 141. The attribute's comment: “construction”.
[Stacks, Tag 01R2]. The conormal sheaf of an immersion: the module pullback, along the canonical closed immersion
i.liftCoborderinto the coborder neighbourhood of the image, of the ideal sheaf of that closed immersion.Keeping it an abbreviation is deliberate: [Stacks, Tag 01R3]'s normalization clause compares an isomorphism of this object with
Iso.refl, which requires the two sides to have the same type without a transport.Quasi-coherence, the other half of the assertion of [Stacks, Tag 01R2], is
Stacks.Conormal.conormalSheaf_isQuasicoherent.
noncomputable abbrev conormalSheaf {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i] :
SheafOfModules.{u} (structureSheafRing Z.toLocallyRingedSpace.toRingedSpace)
Stacks.Thickenings.immersionConormalSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UniversalConormalSheaf.lean, line 126. The attribute's comment: “construction”. References: SGA 3 I (6.8.5); SGA 3 III (4.5.0); SGA 6 VII (1.6).
Stacks Project, Tag 01R2. The conormal sheaf
𝒞_{Z/X} = I/I²of an immersioni : Z ⟶ Xof schemes: the pullback along the closed immersionAlgebraicGeometry.Scheme.Hom.liftCoborderofiinto the canonical open neighbourhoodAlgebraicGeometry.Scheme.Hom.coborderRangeof its image of the defining ideal sheaf of that closed immersion.By [Stacks Project, Tag 01R3] part (1) this pullback is the conormal sheaf: its pushforward along the closed immersion is
I/I². Only the construction is provided; the quasi-coherence asserted by [Stacks Project, Tag 01R2] is not proved here.This is the same construction as
Stacks.Conormal.conormalSheaf, and is defined as that declaration:schemeConormalSheaf i.liftCoborderunfolds, by two abbreviations, to its body.
noncomputable abbrev immersionConormalSheaf {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i] :
SheafOfModules.{u} (structureSheafRing Z.toLocallyRingedSpace.toRingedSpace)
Tag 01R3, a lemma
Tag 01R3 in the Stacks Project.
Stacks.Conormal.affineConormalIsoCotangent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalAlgebra/AffineIdentification.lean, line 475. The attribute's comment: “part (2): affine conormal sections”.
The affine computation of the conormal sheaf. Let
i : Z ⟶ Xbe an immersion andU ⊆ Xan affine open withZ ∩ U = Spec (Γ(X, U) ⧸ I)overU. Then the sections of the conormal sheaf ofioverZ ∩ Uare canonicallyI/I², which is the assertion of [Stacks, Tag 01R3] (2).The conormal sheaf is [Stacks, Tag 01R2]'s, written out: the pullback along
i.liftCoborder : Z ⟶ i.coborderRangeof the ideal sheaf of that closed immersion. Its sections overZ ∩ Uare presented as the sections overUof its pushforward alongi, so that the module is one ofΓ(X, U)-modules, asI.Cotangentis.
def affineConormalIsoCotangent {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i]
(U : X.Opens) (hU : IsAffineOpen U) (I : Ideal Γ(X, U))
(e : pullback i U.ι ≅ Spec (.of (Γ(X, U) ⧸ I)))
(he : pullback.snd i U.ι ≫ hU.isoSpec.hom =
e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) :
((modulePushforward i.toLRSHom.toShHom).obj
((modulePullback i.liftCoborder.toLRSHom.toShHom).obj
(Stacks.ClosedImmersion.idealSheaf i.liftCoborder.toLRSHom.toShHom))).val.obj (op U)
≅ ModuleCat.of Γ(X, U) I.Cotangent
Stacks.Conormal.pushforwardConormalIsoCotangent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalAlgebra/Factorization.lean, line 157. The attribute's comment: “part (1): pushforward is the ideal modulo its square”.
[Stacks, Tag 01R3] (1), the affine form of
i'_* 𝒞_{Z/X} = ℐ/ℐ². Leti : Z ⟶ Xbe an immersion factored as a closed immersioni' : Z ⟶ Uinto an open subscheme, letV ⊆ Ube an affine open, and supposeZ ∩ V = Spec (Γ(U, V) ⧸ I)overV. Then the sections overVof the direct image alongi'of the conormal sheaf are canonicallyI/I².Part (1) identifies the conormal sheaf with
(i')^* ℐ, after which this isStacks.Conormal.affineIdealPullbackIsoCotangentfor the closed immersioni'— the ring-theoretic contentI ⊗_R R/I = I/I²— with the kernel of the map on sections identified withIby the affine model.
noncomputable def pushforwardConormalIsoCotangent {Z X : Scheme.{u}} (i : Z ⟶ X)
[IsImmersion i] (U : X.Opens) (i' : Z ⟶ U.toScheme) [IsClosedImmersion i']
(hfac : i' ≫ U.ι = i) (V : U.toScheme.Opens) (hV : IsAffineOpen V)
(I : Ideal Γ(U.toScheme, V))
(e : CategoryTheory.Limits.pullback i' V.ι ≅ Spec (.of (Γ(U.toScheme, V) ⧸ I)))
(he : CategoryTheory.Limits.pullback.snd i' V.ι ≫ hV.isoSpec.hom =
e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) :
((modulePushforward i'.toLRSHom.toShHom).obj (conormalSheaf i)).val.obj (op V) ≅
ModuleCat.of Γ(U.toScheme, V) I.Cotangent
Stacks.Conormal.pushforwardConormalIsoCotangent_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalAlgebra/Factorization.lean, line 178. The attribute's comment: “part (1): canonical affine quotient formula”.
[Stacks, Tag 01R3] (1), the normalization of the affine form of
i'_* 𝒞_{Z/X} = ℐ/ℐ². The isomorphism sends the canonical quotient of a section of the ideal sheaf to the class of that section moduloI². SinceIdeal.toCotangentis surjective this determines the isomorphism, so it is the canonical one and not merely some isomorphism of the right type.
theorem pushforwardConormalIsoCotangent_apply {Z X : Scheme.{u}} (i : Z ⟶ X)
[IsImmersion i] (U : X.Opens) (i' : Z ⟶ U.toScheme) [IsClosedImmersion i']
(hfac : i' ≫ U.ι = i) (V : U.toScheme.Opens) (hV : IsAffineOpen V)
(I : Ideal Γ(U.toScheme, V))
(e : CategoryTheory.Limits.pullback i' V.ι ≅ Spec (.of (Γ(U.toScheme, V) ⧸ I)))
(he : CategoryTheory.Limits.pullback.snd i' V.ι ≫ hV.isoSpec.hom =
e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
(x : (Stacks.ClosedImmersion.idealSheaf i'.toLRSHom.toShHom).val.obj (op V))
(hx : (kernel.ι (SheafOfModules.unitToPushforwardObjUnit
(structureSheafHom i'.toLRSHom.toShHom))).val.app (op V) x ∈ I) :
(pushforwardConormalIsoCotangent i U i' hfac V hV I e he).hom.hom
((conormalQuotientMap i U i' hfac).val.app (op V) x) =
I.toCotangent ⟨(kernel.ι (SheafOfModules.unitToPushforwardObjUnit
(structureSheafHom i'.toLRSHom.toShHom))).val.app (op V) x, hx⟩
Stacks.Conormal.conormalSheafIsoPullbackIdealSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalComparison/IdealSheafComparison.lean, line 187. The attribute's comment: “part (1): pullback of the ideal sheaf”.
[Stacks, Tag 01R3], part (1). The conormal sheaf of an immersion
i : Z ⟶ Xis the module pullback of the ideal sheaf of any factorization ofias a closed immersion into an open subscheme followed by the inclusion of that open subscheme.The given open
Uis contained ini.coborderRangebyStacks.Conormal.le_coborderRange_of_comp_eq, and the factorizing morphism followed by the induced open immersion isi.liftCoborderbyStacks.Conormal.comp_homOfLE_eq_liftCoborder. So this ispullbackIdealSheafIsoOfCompEqfor that open immersion.
noncomputable def conormalSheafIsoPullbackIdealSheaf {Z X : Scheme.{u}} (i : Z ⟶ X)
[IsImmersion i] (U : X.Opens) (i' : Z ⟶ U.toScheme) [IsClosedImmersion i']
(hfac : i' ≫ U.ι = i) :
conormalSheaf i ≅
(modulePullback i'.toLRSHom.toShHom).obj
(Stacks.ClosedImmersion.idealSheaf i'.toLRSHom.toShHom)
Stacks.Conormal.conormalSheafIsoPullbackIdealSheaf_liftCoborder, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalComparison/Normalization.lean, line 272. The attribute's comment: “part (1): canonical normalization”.
[Stacks, Tag 01R3], part (1): canonical normalization.
theorem conormalSheafIsoPullbackIdealSheaf_liftCoborder {Z X : Scheme.{u}} (i : Z ⟶ X)
[IsImmersion i] :
conormalSheafIsoPullbackIdealSheaf i i.coborderRange i.liftCoborder i.liftCoborder_ι =
Iso.refl (conormalSheaf i)
Stacks.Conormal.OpenFactorizations.conormalQuotientMap_restrict_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalOpenFactorizations/Compatibility.lean, line 296. The attribute's comment: “part (1): compatibility of open factorizations”.
[Stacks, Tag 01R3], part (1): compatibility of open factorizations. The quotient identifications from two open factorizations agree on common conormal sections: images of the same ambient ideal generator agree after restriction to any common source open.
This is
generator_eq_of_two_factorizationsatr = (a : Γ(X, V)). The presentation datahV,I,e,heis carried because the tagged statement carries it; the proof does not use it, and the statement proved is the stronger one witha : Ireplaced by an arbitraryr : Γ(X, V)and the presentation dropped altogether.
theorem conormalQuotientMap_restrict_factorization {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i]
(V : X.Opens) (hV : IsAffineOpen V)
(I : Ideal Γ(X, V))
(e : Limits.pullback i V.ι ≅ Spec (.of (Γ(X, V) ⧸ I)))
(he : Limits.pullback.snd i V.ι ≫ hV.isoSpec.hom =
e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
(U₁ U₂ : X.Opens)
(i₁ : Z ⟶ U₁.toScheme) [IsClosedImmersion i₁]
(i₂ : Z ⟶ U₂.toScheme) [IsClosedImmersion i₂]
(hfac₁ : i₁ ≫ U₁.ι = i) (hfac₂ : i₂ ≫ U₂.ι = i)
(W₁ : U₁.toScheme.Opens) (hW₁ : W₁ ≤ U₁.ι ⁻¹ᵁ V)
(W₂ : U₂.toScheme.Opens) (hW₂ : W₂ ≤ U₂.ι ⁻¹ᵁ V)
(a : I)
(x₁ : (Stacks.ClosedImmersion.idealSheaf i₁.toLRSHom.toShHom).val.obj (.op W₁))
(x₂ : (Stacks.ClosedImmersion.idealSheaf i₂.toLRSHom.toShHom).val.obj (.op W₂))
(hx₁ : (U₁.ι.appLE V W₁ hW₁).hom (a : Γ(X, V)) =
(kernel.ι (SheafOfModules.unitToPushforwardObjUnit
(structureSheafHom i₁.toLRSHom.toShHom))).val.app (.op W₁) x₁)
(hx₂ : (U₂.ι.appLE V W₂ hW₂).hom (a : Γ(X, V)) =
(kernel.ι (SheafOfModules.unitToPushforwardObjUnit
(structureSheafHom i₂.toLRSHom.toShHom))).val.app (.op W₂) x₂)
(T : Z.Opens) (hT₁ : T ≤ i₁ ⁻¹ᵁ W₁) (hT₂ : T ≤ i₂ ⁻¹ᵁ W₂) :
(conormalSheaf i).val.map (homOfLE hT₁).op
((conormalQuotientMap i U₁ i₁ hfac₁).val.app (.op W₁) x₁) =
(conormalSheaf i).val.map (homOfLE hT₂).op
((conormalQuotientMap i U₂ i₂ hfac₂).val.app (.op W₂) x₂)
Stacks.Conormal.Tag01R3Generators.conormalQuotientMap_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Generators/Epi.lean, line 138. The attribute's comment: “part (1): sheaf quotient map is epimorphic”.
[Stacks, Tag 01R3], part (1): the ideal sheaf surjects onto the pushforward conormal sheaf. For an immersion
i : Z ⟶ Xand any closed-immersion factorizationi' : Z ⟶ U,Stacks.Conormal.conormalQuotientMapis an epimorphism of sheaves of modules.
Stacks.SheafOfModules.EpiMono.epi_of_isLocallySurjectiveatisLocallySurjective_conormalQuotientMap. No affineness, Noetherian or finiteness hypothesis is used, andStacks.Conormal.epi_conormalQuotientMap_iff's named blocker — epimorphy of the adjunction unit — is bypassed rather than proved; see the module docstring.
theorem conormalQuotientMap_epi {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i]
(U : X.Opens) (i' : Z ⟶ U.toScheme) [IsClosedImmersion i'] (hfac : i' ≫ U.ι = i) :
Epi (Stacks.Conormal.conormalQuotientMap i U i' hfac)
Stacks.Conormal.Tag01R3Generators.conormalQuotientMap_kernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Generators/Kernel.lean, line 132. The attribute's comment: “part (1): quotient by the ideal square”.
[Stacks, Tag 01R3], part (1): the quotient is by the square of the ideal. On an affine open
Vof a closed-immersion factorizationi' : Z ⟶ Uof an immersioni : Z ⟶ X, a sectionxof the ideal sheaf ofi'overVis killed byStacks.Conormal.conormalQuotientMapexactly when its image in the structure sheaf lies in(i'.ker.ideal ⟨V, hV⟩) ^ 2.The statement involves no presentation data; one is produced inside the proof by
Stacks.DiagonalPresentation.exists_presentationand its ideal identified withi'.ker.ideal ⟨V, hV⟩bypresentationIdeal_eq_ker_app. The vanishing is then transported acrossStacks.Conormal.pushforwardConormalIsoCotangentbyStacks.Conormal.pushforwardConormalIsoCotangent_applyand read off byIdeal.toCotangent_eq_zero.
theorem conormalQuotientMap_kernel {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i]
(U : X.Opens) (i' : Z ⟶ U.toScheme) [IsClosedImmersion i'] (hfac : i' ≫ U.ι = i)
(V : U.toScheme.Opens) (hV : IsAffineOpen V)
(x : (Stacks.ClosedImmersion.idealSheaf i'.toLRSHom.toShHom).val.obj (.op V)) :
(Stacks.Conormal.conormalQuotientMap i U i' hfac).val.app (.op V) x = 0 ↔
(kernel.ι (SheafOfModules.unitToPushforwardObjUnit
(structureSheafHom i'.toLRSHom.toShHom))).val.app (.op V) x ∈
(i'.ker.ideal ⟨V, hV⟩) ^ 2
Stacks.Tag01R3PartTwo.affineConormalIsoCotangent_inv_toCotangent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PartTwo/Generators.lean, line 92. The attribute's comment: “part (2): canonical affine generators”.
[Stacks, Tag 01R3], part (2): canonical affine generators. The inverse affine identification sends the class of an ideal section to its canonical conormal quotient, on every open of every closed-immersion factorization, after restricting the ambient section.
The formula is proved at the coborder factorization by
conormalAffineSectionsIsoCotangent_toCotangentand moved to(U, i')by the compatibilityStacks.Conormal.OpenFactorizations.generator_eq_of_two_factorizations, at the common source openi' ⁻¹ᵁ W. The section of the coborder ideal sheaf that the comparison needs is produced byexists_coborderSectionfrom the presentation alone.
theorem affineConormalIsoCotangent_inv_toCotangent {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i]
(V : X.Opens) (hV : IsAffineOpen V) (I : Ideal Γ(X, V))
(e : Limits.pullback i V.ι ≅ Spec (.of (Γ(X, V) ⧸ I)))
(he : Limits.pullback.snd i V.ι ≫ hV.isoSpec.hom =
e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
(U : X.Opens) (i' : Z ⟶ U.toScheme) [IsClosedImmersion i']
(hfac : i' ≫ U.ι = i)
(W : U.toScheme.Opens) (hW : W ≤ U.ι ⁻¹ᵁ V)
(a : I)
(x : (Stacks.ClosedImmersion.idealSheaf i'.toLRSHom.toShHom).val.obj (.op W))
(hx : (U.ι.appLE V W hW).hom (a : Γ(X, V)) =
(kernel.ι (SheafOfModules.unitToPushforwardObjUnit
(structureSheafHom i'.toLRSHom.toShHom))).val.app (.op W) x) :
(Stacks.Conormal.conormalSheaf i).val.map
(homOfLE (show i' ⁻¹ᵁ W ≤ i ⁻¹ᵁ V from by
rw [← hfac]; exact i'.preimage_mono hW)).op
((Stacks.Conormal.affineConormalIsoCotangent i V hV I e he).inv.hom
(I.toCotangent a)) =
(Stacks.Conormal.conormalQuotientMap i U i' hfac).val.app (.op W) x
Stacks.Tag01R3PartTwo.affineConormalIsoCotangentWithQuotient, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PartTwo/Generators.lean, line 137. The attribute's comment: “part (2): affine identification with canonical quotient generators”.
[Stacks, Tag 01R3], part (2): the affine identification with canonical quotient generators. The sections over an affine open
Vof the ambient scheme of the direct image of the conormal sheaf areI.Cotangent, together with the formula on ideal generators for every closed-immersion factorization and every open of it.The isomorphism is
Stacks.Conormal.affineConormalIsoCotangentand the second component isaffineConormalIsoCotangent_inv_toCotangent.
noncomputable def affineConormalIsoCotangentWithQuotient {Z X : Scheme.{u}} (i : Z ⟶ X)
[IsImmersion i] (V : X.Opens) (hV : IsAffineOpen V) (I : Ideal Γ(X, V))
(e : Limits.pullback i V.ι ≅ Spec (.of (Γ(X, V) ⧸ I)))
(he : Limits.pullback.snd i V.ι ≫ hV.isoSpec.hom =
e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) :
{ c : ((modulePushforward i.toLRSHom.toShHom).obj
(Stacks.Conormal.conormalSheaf i)).val.obj (.op V) ≅
ModuleCat.of Γ(X, V) I.Cotangent //
∀ (U : X.Opens) (i' : Z ⟶ U.toScheme) [IsClosedImmersion i']
(hfac : i' ≫ U.ι = i)
(W : U.toScheme.Opens) (hW : W ≤ U.ι ⁻¹ᵁ V)
(a : I)
(x : (Stacks.ClosedImmersion.idealSheaf i'.toLRSHom.toShHom).val.obj (.op W)),
(U.ι.appLE V W hW).hom (a : Γ(X, V)) =
(kernel.ι (SheafOfModules.unitToPushforwardObjUnit
(structureSheafHom i'.toLRSHom.toShHom))).val.app (.op W) x →
(Stacks.Conormal.conormalSheaf i).val.map
(homOfLE (show i' ⁻¹ᵁ W ≤ i ⁻¹ᵁ V from by
rw [← hfac]; exact i'.preimage_mono hW)).op
(c.inv.hom (I.toCotangent a)) =
(Stacks.Conormal.conormalQuotientMap i U i' hfac).val.app (.op W) x }
Stacks.Tag01R3PartTwo.affineConormalIsoCotangent_inv_toCotangent_liftCoborder, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PartTwo/Generators.lean, line 170. The attribute's comment: “part (2): defining adjunction-unit generators”.
[Stacks, Tag 01R3], part (2): defining adjunction-unit generators. On the defining factorization the affine generator is the image under the defining adjunction unit itself.
This is
affineConormalIsoCotangent_inv_toCotangentat(i.coborderRange, i.liftCoborder), withStacks.Conormal.OpenFactorizations.conormalQuotientMap_liftCoborder— the normalizationStacks.Conormal.conormalSheafIsoPullbackIdealSheaf_liftCoborderread on the quotient map — replacing the quotient map by the unit.
theorem affineConormalIsoCotangent_inv_toCotangent_liftCoborder {Z X : Scheme.{u}} (i : Z ⟶ X)
[IsImmersion i] (V : X.Opens) (hV : IsAffineOpen V) (I : Ideal Γ(X, V))
(e : Limits.pullback i V.ι ≅ Spec (.of (Γ(X, V) ⧸ I)))
(he : Limits.pullback.snd i V.ι ≫ hV.isoSpec.hom =
e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
(W : i.coborderRange.toScheme.Opens) (hW : W ≤ i.coborderRange.ι ⁻¹ᵁ V)
(a : I)
(x : (Stacks.ClosedImmersion.idealSheaf i.liftCoborder.toLRSHom.toShHom).val.obj (.op W))
(hx : (i.coborderRange.ι.appLE V W hW).hom (a : Γ(X, V)) =
(kernel.ι (SheafOfModules.unitToPushforwardObjUnit
(structureSheafHom i.liftCoborder.toLRSHom.toShHom))).val.app (.op W) x) :
(Stacks.Conormal.conormalSheaf i).val.map
(homOfLE (show i.liftCoborder ⁻¹ᵁ W ≤ i ⁻¹ᵁ V from
(i.liftCoborder.preimage_mono hW).trans_eq
(congrArg (fun f : Z ⟶ X ↦ f ⁻¹ᵁ V) i.liftCoborder_ι))).op
((Stacks.Conormal.affineConormalIsoCotangent i V hV I e he).inv.hom
(I.toCotangent a)) =
((modulePullbackPushforwardAdjunction i.liftCoborder.toLRSHom.toShHom).unit.app
(Stacks.ClosedImmersion.idealSheaf i.liftCoborder.toLRSHom.toShHom)).val.app (.op W) x
Stacks.Tag01R3PartTwo.affineConormalIsoCotangent_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PartTwo/Restrict.lean, line 72. The attribute's comment: “part (2): compatibility with restriction”.
[Stacks, Tag 01R3], part (2): compatibility with restriction. The affine identifications commute with restriction: the class of an ideal section restricts to the class of its restriction.
This is the generator-level naturality needed to use the affine formula to characterize morphisms of conormal sheaves. See the module docstring for the route; the point is that
affineConormalIsoCotangent_inv_toCotangentis available at the coborder factorization over the smaller open, so one section of the coborder ideal sheaf serves both presentations.
theorem affineConormalIsoCotangent_restrict {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i]
(U V : X.Opens) (hVU : V ≤ U) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
(I : Ideal Γ(X, U)) (J : Ideal Γ(X, V))
(eU : Limits.pullback i U.ι ≅ Spec (.of (Γ(X, U) ⧸ I)))
(heU : Limits.pullback.snd i U.ι ≫ hU.isoSpec.hom =
eU.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
(eV : Limits.pullback i V.ι ≅ Spec (.of (Γ(X, V) ⧸ J)))
(heV : Limits.pullback.snd i V.ι ≫ hV.isoSpec.hom =
eV.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk J)))
(x : I)
(hx : (X.presheaf.map (homOfLE hVU).op).hom (x : Γ(X, U)) ∈ J) :
(Stacks.Conormal.affineConormalIsoCotangent i V hV J eV heV).hom.hom
(((modulePushforward i.toLRSHom.toShHom).obj
(Stacks.Conormal.conormalSheaf i)).val.map (homOfLE hVU).op
((Stacks.Conormal.affineConormalIsoCotangent i U hU I eU heU).inv.hom
(I.toCotangent x))) =
J.toCotangent
⟨(X.presheaf.map (homOfLE hVU).op).hom (x : Γ(X, U)), hx⟩
Tag 01R4, a lemma
Tag 01R4 in the Stacks Project.
Stacks.Immersion.immersionConormalSheafMap_ideal_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Conormal/SquareMap.lean, line 180. The attribute's comment: “affine ideal containment”.
[Stacks Project, Tag 01R4]: the ambient ring map carries the target ideal into the source ideal. On a pair of affine opens
U ⊆ XandV ⊆ X'withg(U) ⊆ Vpresenting the scheme-theoretic intersections asSpec (Γ(X, U) ⧸ I)andSpec (Γ(X', V) ⧸ J), the mapg^♯ : Γ(X', V) ⟶ Γ(X, U)sendsJintoI.This is what lets the affine characterisation speak of the class in
I/I²of the image of a class inJ/J².
theorem immersionConormalSheafMap_ideal_mem (i : Z ⟶ X) (i' : Z' ⟶ X')
[IsImmersion i] [IsImmersion i'] (f : Z ⟶ Z') (g : X ⟶ X') (comm : i ≫ g = f ≫ i')
(U : X.Opens) (hU : IsAffineOpen U) (V : X'.Opens) (hV : IsAffineOpen V)
(hUV : U ≤ g ⁻¹ᵁ V) (I : Ideal Γ(X, U)) (J : Ideal Γ(X', V))
(eZ : pullback i U.ι ≅ Spec (quotRing I))
(heZ : pullback.snd i U.ι ≫ hU.isoSpec.hom = eZ.hom ≫ quotImmersion Γ(X, U) I)
(eZ' : pullback i' V.ι ≅ Spec (quotRing J))
(heZ' : pullback.snd i' V.ι ≫ hV.isoSpec.hom = eZ'.hom ≫ quotImmersion Γ(X', V) J)
(a : J) : (g.appLE V U hUV).hom (a : Γ(X', V)) ∈ I
Stacks.Immersion.immersionConormalSheafMap_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Conormal/SquareMap.lean, line 321. The attribute's comment: “uniqueness”.
[Stacks Project, Tag 01R4]: the affine formula determines the map. A morphism
f^* 𝒞_{Z'/X'} ⟶ 𝒞_{Z/X}satisfying the affine characterisation isStacks.Immersion.immersionConormalSheafMap.Transposing along
f^* ⊣ f_*and testing on the basis ofZ'given by the opensi' ⁻¹ᵁ Vfor affineV ⊆ X'insidei'.coborderRangereduces this toStacks.Immersion.transpose_eq_of_coborder_affine.
theorem immersionConormalSheafMap_unique (i : Z ⟶ X) (i' : Z' ⟶ X')
[IsImmersion i] [IsImmersion i'] (f : Z ⟶ Z') (g : X ⟶ X') (comm : i ≫ g = f ≫ i')
(φ : (modulePullback f.toLRSHom.toShHom).obj
(conormalSheaf i'.liftCoborder.toLRSHom.toShHom) ⟶
conormalSheaf i.liftCoborder.toLRSHom.toShHom)
(hφ : IsInducedConormalSheafMap i i' f g comm φ) :
φ = immersionConormalSheafMap i i' f g (toShHom_square comm)
Declarations registered for the tag:
Stacks.Immersion.immersionConormalSheafMap, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Conormal/SquareMap.lean, line 618 (StacksFrontier): “canonical map”.Stacks.Immersion.isInducedConormalSheafMap_immersionConormalSheafMap, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Conormal/SquareMap.lean, line 620 (StacksFrontier): “affine formula”.
Tag 0473, a lemma
Tag 0473 in the Stacks Project.
Stacks.Immersion.epi_immersionConormalSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Conormal/SquareEpi.lean, line 310. The attribute's comment: “surjectivity”.
For a cartesian square of schemes whose horizontal maps
iandi'are immersions, the canonical mapf^* 𝒞_{Z'/X'} ⟶ 𝒞_{Z/X}of conormal sheaves is an epimorphism.
theorem epi_immersionConormalSheafMap (i : Z ⟶ X) (i' : Z' ⟶ X') [IsImmersion i] [IsImmersion i']
(f : Z ⟶ Z') (g : X ⟶ X') (sq : IsPullback i f g i') :
Epi (immersionConormalSheafMap i i' f g (toShHom_square sq.w))
Stacks.Immersion.isIso_immersionConormalSheafMap_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Conormal/SquareFlatIso.lean, line 254. The attribute's comment: “flat base change”.
For a cartesian square of schemes whose horizontal maps
iandi'are immersions and whose ambient vertical mapgis flat, the canonical mapf^* 𝒞_{Z'/X'} ⟶ 𝒞_{Z/X}of [Stacks Project, Tag 01R4] is an isomorphism.
theorem isIso_immersionConormalSheafMap_of_flat (i : Z ⟶ X) (i' : Z' ⟶ X')
[IsImmersion i] [IsImmersion i']
(f : Z ⟶ Z') (g : X ⟶ X') [Flat g] (sq : IsPullback i f g i') :
IsIso (Stacks.Immersion.immersionConormalSheafMap i i' f g
(Stacks.Immersion.toShHom_square sq.w))
Deformation.Examples.isBaseCompatibleConormalMap_deformationConormalBaseChangeIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeDeformationConormalBaseChange.lean, line 252. The attribute's comment: “naturality in the base object: the flat base change for the conormal sheaf of the special fibre of the target of an arrow of deformations is the conormal datum compatible with the base along the factorisation through the spectrum of the source's base object, the map on the base being the conormal map of the morphism of base objects. This is one of the two readings of a single canonical map of Tag 01R4, not a computation of either reading on sections”.
The flat base change of the target deformation is compatible with the base, along the other factorisation of the same composite square. The square carrying the special fibre of
Qover the closed point ofSpec Aalso factors throughSpec B: the special-fibre square ofQfollowed by the square of closed pointsDeformation.Examples.residueSpecMap_naturality. Reading the canonical map of [Stacks Project, Tag 01R4] along that factorisation makesDeformation.Examples.deformationConormalBaseChangeIsoatQthe compatible datum, the map coming from the base being the conormal mapDeformation.Examples.residueConormalMapofφ.base.Together with
Deformation.Examples.isBaseCompatibleConormalMap_deformationConormalMapthis is the naturality of flat base change for the conormal sheaf of a special fibre in the base object of𝒞_Λ: the two statements are the two readings of one canonical map.
theorem isBaseCompatibleConormalMap_deformationConormalBaseChangeIso (φ : P ⟶ Q) :
IsBaseCompatibleConormalMap Q.specialMap (residueSpecMap Q.base) (residueSpecMap P.base)
(𝟙 (Spec (CommRingCat.of k))) (baseSpecMap φ.base) (Q.toBase ≫ baseSpecMap φ.base) X.hom
(residueSpecMap_comp_baseSpecMap' φ.base)
(square_comp Q.specialCartesian.w (residueSpecMap_comp_baseSpecMap' φ.base))
(deformationConormalBaseChangeIso Q).hom
Deformation.Examples.deformationConormalBaseChangeIso_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeDeformationConormalBaseChange.lean, line 322. The attribute's comment: “naturality of flat base change for the conormal sheaf of a special fibre in the base object: for an arrow of deformations, the pullback along the structure morphism of the conormal map of the morphism of base objects, followed by the flat base change of the target, is the flat base change of the source followed by the conormal map of the arrow -- up to the eqToHom comparing the two unit composites of the edge on the closed subschemes. Both conormal maps are the canonical maps of Tag 01R4; nothing is computed on sections and the map on the base is NOT identified with the map of maximal ideals”.
The flat base change of the conormal sheaf of a special fibre is natural in the base object of
𝒞_Λ. For an arrowφ : P ⟶ Qof deformations ofXthe square
p_X^* 𝒞_{Spec k/Spec A} ⟶ 𝒞_{X/P.scheme},p_X^* 𝒞_{Spec k/Spec B} ⟶ 𝒞_{X/Q.scheme}commutes, the horizontal maps being
Deformation.Examples.deformationConormalBaseChangeIsoand the vertical ones the pullback alongp_Xof the conormal map ofφ.baseand the conormal map ofφ. This is the statement that the conormal map of an arrow of deformations corresponds, under flat base change, to the conormal map of the morphism of base objects.Both maps of conormal sheaves are written in the unstripped shape [Stacks Project, Tag 01R4] produces — that is, out of the pullback along the edge on the closed subschemes, which is an identity — so each composite begins with the comparison
RingedSpaceModuleAdjunction.modulePullbackCompof the pullback along a composite with the composite of the pullbacks, and the two composites𝟙_X ≫ p_Xandp_X ≫ 𝟙_{Spec k}of those edges differ by aCategoryTheory.eqToHom. The stripped maps areDeformation.Examples.deformationConormalMapandDeformation.Examples.residueConormalMap.The proof is the two factorisations
Deformation.Examples.isBaseCompatibleConormalMap_deformationConormalBaseChangeIsoandDeformation.Examples.isBaseCompatibleConormalMap_deformationConormalMapof the one canonical map, compared byStacks.Immersion.immersionConormalSheafMap_congralong the equality of edges; the right-hand edges of the two squares overSpec Aare identified by the cartesian squareDeformation.Examples.SchemeDeformationCategory.Hom.cartesianof the arrow.
theorem deformationConormalBaseChangeIso_naturality (φ : P ⟶ Q) :
(modulePullbackComp X.hom.toLRSHom.toShHom
(Scheme.Hom.toLRSHom (𝟙 (Spec (CommRingCat.of k)))).toShHom).hom.app
(immersionConormalSheaf (residueSpecMap P.base)) ≫
(modulePullback X.hom.toLRSHom.toShHom).map
(immersionConormalSheafMap (residueSpecMap Q.base) (residueSpecMap P.base)
(𝟙 (Spec (CommRingCat.of k))) (baseSpecMap φ.base)
(toShHom_square (residueSpecMap_comp_baseSpecMap' φ.base))) ≫
(deformationConormalBaseChangeIso Q).hom =
eqToHom (congrArg (fun p : X.left ⟶ Spec (CommRingCat.of k) =>
(modulePullback p.toLRSHom.toShHom).obj
(immersionConormalSheaf (residueSpecMap P.base)))
((Category.id_comp X.hom).trans (Category.comp_id X.hom).symm).symm) ≫
(modulePullbackComp (Scheme.Hom.toLRSHom (𝟙 X.left)).toShHom
X.hom.toLRSHom.toShHom).hom.app
(immersionConormalSheaf (residueSpecMap P.base)) ≫
(modulePullback (Scheme.Hom.toLRSHom (𝟙 X.left)).toShHom).map
(deformationConormalBaseChangeIso P).hom ≫
immersionConormalSheafMap Q.specialMap P.specialMap (𝟙 X.left) φ.map
(toShHom_square (specialMap_comp_map φ))
Ideal.bijective_cotangentBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/CotangentBaseChange.lean, line 332. The attribute's comment: “flat case, affine”. References: EGA IV (16.2.2), “(iii)”; EGA IV (17.13.1), “special case”; SGA 6 VIII (2.2), “special case”.
[Stacks Project, Tag 0473], the flat case in the affine picture. Let
Sbe a flatR-algebra, letIbe an ideal ofRand letI Sbe the ideal ofSgenerated by its image. Then the canonical map
I ⧸ I ^ 2 ⊗[R] S ⟶ I S ⧸ (I S) ^ 2is an isomorphism. This is the commutative algebra statement the proof of that tag reduces to; the sheaf-level statement for a cartesian square of immersions of schemes is not proved here, and the surjectivity half of the tag is
Stacks.Immersion.epi_immersionConormalSheafMap.
theorem bijective_cotangentBaseChange [Module.Flat R S] :
Function.Bijective (I.cotangentBaseChange S)
Tag 062S, a lemma
Tag 062S in the Stacks Project.
Stacks.Immersion.conormalSequenceRightMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Conormal/ConormalSequence.lean, line 92. The attribute's comment: “the second arrow 𝒞_{Z/X} ⟶ 𝒞_{Z/Y}”.
The right-hand map
𝒞_{Z/X} ⟶ 𝒞_{Z/Y}of the conormal sequence of [Stacks Project, Tag 062S]. It is the canonical map of [Stacks Project, Tag 01R4] attached to the square with horizontal mapsiandi ≫ jand vertical maps𝟙_Zandj, read through the identification of the pullback along the identity with the identity functor.
def conormalSequenceRightMap (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i] [IsImmersion j] :
conormalSheaf (i ≫ j).liftCoborder.toLRSHom.toShHom ⟶
conormalSheaf i.liftCoborder.toLRSHom.toShHom
Stacks.Immersion.epi_conormalSequenceRightMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Conormal/ConormalSequence.lean, line 109. The attribute's comment: “exactness at the right term: the canonical map 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} is epi”. References: EGA IV (16.2.7), “surjectivity at right”.
[Stacks Project, Tag 062S]: the conormal sequence is exact at
𝒞_{Z/Y}. For immersionsZ ⟶ Y ⟶ Xthe canonical map𝒞_{Z/X} ⟶ 𝒞_{Z/Y}is an epimorphism, which is the⟶ 0at the right-hand end of the canonical sequencei^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} ⟶ 0.The defining square is cartesian by
Stacks.Immersion.conormalSequence_isPullback, soStacks.Immersion.epi_immersionConormalSheafMapapplies; the pullback-identity isomorphism is an epimorphism.
theorem epi_conormalSequenceRightMap (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i] [IsImmersion j] :
Epi (conormalSequenceRightMap i j)
Stacks.Immersion.conormalSequence_comp_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Conormal/ConormalSequenceExact.lean, line 198. The attribute's comment: “the two canonical maps form a complex: the composite i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} is zero, for any immersions i : Z ⟶ Y and j : Y ⟶ X; the left-hand map is Stacks.Immersion.conormalLeftMap, equal to Stacks.AlgebraicGeometry.conormalSequenceLeftMap by Stacks.AlgebraicGeometry.conormalSequenceLeftMap_eq”.
[Stacks Project, Tag 062S]: the two canonical maps of the conormal sequence compose to zero. For immersions
Z ⟶ Y ⟶ Xthe compositei^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y}vanishes.Transposing along
i^* ⊣ i_*turns the statement into one about sections over opens ofY. Over the preimage of a chart a section of𝒞_{Y/X}is the class of a functionkcutting outY, the left-hand map carries it to the class ofkas a function cutting outZinX, and the right-hand map carries that to the class of the restriction ofkto the preimage of the chart inY, which is zero becausekvanishes there. The charts refine every open ofY.
theorem conormalSequence_comp_zero (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i] [IsImmersion j] :
conormalLeftMap i j ≫ conormalSequenceRightMap i j = 0
Stacks.Immersion.conormalSequenceShortComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Conormal/ConormalSequenceExact.lean, line 280. The attribute's comment: “the sequence as a short complex”.
The conormal sequence of [Stacks Project, Tag 062S] as a two-term complex of
𝒪_Z-modules,i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y}.
def conormalSequenceShortComplex (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i] [IsImmersion j] :
ShortComplex (SheafOfModules.{u} (structureSheafRing Z.toLocallyRingedSpace.toRingedSpace))
Stacks.Immersion.conormalSequence_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Conormal/ConormalSequenceExact.lean, line 298. The attribute's comment: “exactness in the middle: for any immersions i : Z ⟶ Y and j : Y ⟶ X the image of i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X} is the kernel of 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} (equality, as ShortComplex.Exact of the complex built from the two canonical maps of Tag 01R4); no hypothesis beyond the two immersions”.
[Stacks Project, Tag 062S]: the conormal sequence is exact at
𝒞_{Z/X}. For immersionsZ ⟶ Y ⟶ Xthe kernel of the canonical map𝒞_{Z/X} ⟶ 𝒞_{Z/Y}is the image of the canonical mapi^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X}.Exactness is local, and it is tested over the preimages of the charts of the chain (
Stacks.Immersion.exact_of_chartwise). Over a chart the two maps are, on sections, the two maps of conormal modules of the tower of ringsΓ(X, V) ⟶ Γ(X, V) ⟶ Γ(Y, j⁻¹V), whose exactness isStacks.Conormal.exact_mapCotangent_comap; that isStacks.Immersion.ConormalChart.exists_leftMap_eq.
theorem conormalSequence_exact (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i] [IsImmersion j] :
(conormalSequenceShortComplex i j).Exact
Stacks.AlgebraicGeometry.conormalSequenceLeftMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Conormal/SplitSequence.lean, line 43. The attribute's comment: “the first arrow i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X}”.
The left-hand map
i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X}of the conormal sequence of [Stacks Project, Tag 062S]. It is the canonical map of [Stacks Project, Tag 01R4] attached to the square with horizontal mapsi ≫ jandjand vertical mapsiand𝟙 X.
def conormalSequenceLeftMap (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i] [IsImmersion j] :
(modulePullback i.toLRSHom.toShHom).obj
(Stacks.ClosedImmersion.conormalSheaf j.liftCoborder.toLRSHom.toShHom) ⟶
Stacks.ClosedImmersion.conormalSheaf (i ≫ j).liftCoborder.toLRSHom.toShHom
Sources
Section29.33 Sheaf of differentials of a morphism#
Section 29.33 of the Stacks Project, Tag 01UM. 18 tags here are carried by 48 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 01UQ, a definition
Tag 01UQ in the Stacks Project.
Stacks.Smooth.cotangentDerivation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Smooth/CotangentDerivation.lean, line 70. The attribute's comment: “the universal S-derivation d_{X/S} that the sheaf of differentials Stacks.Smooth.cotangentSheaf of a morphism of schemes is equipped with”.
The universal
S-derivationd_{X/S} : 𝒪_X ⟶ Ω_{X/S}that the sheaf of differentials of a morphism of schemesf : X ⟶ Sis equipped with: the universal derivation of the underlying morphism of ringed spaces, read as a relative derivation over the structural mapf⁻¹𝒪_S ⟶ 𝒪_Xoff.
noncomputable def cotangentDerivation :
SheafOfModules.SheafDerivation (inverseImageStructureMap f) (cotangentSheaf f)
Stacks.Smooth.cotangentSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Smooth/CotangentSheafScheme.lean, line 93. The attribute's comment: “the sheaf of differentials of a morphism of schemes, namely the differentials of the underlying morphism of ringed spaces; the universal S-derivation d_{X/S} it is equipped with is Stacks.Smooth.cotangentDerivation”. References: SGA 6 0 (2.1).
The sheaf of relative differentials
Ω_{X/S}of a morphism of schemesf : X ⟶ S, as a sheaf of𝒪_X-modules: the module of differentials of the morphism of sheaves of ringsf⁻¹𝒪_S ⟶ 𝒪_X, which is how Stacks Project, Tag 01UM defines it.
noncomputable def cotangentSheaf {X S : Scheme.{u}} (f : X ⟶ S) : X.Modules
Tag 01UR, a lemma
Tag 01UR in the Stacks Project.
AlgebraicGeometry.SheafOfModules.universalDerivation_isUniversal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials.lean, line 130. The attribute's comment: “postcomposition with the universal derivation is bijective onto the derivations”. References: EGA IV (16.5.3), “(ii)”.
Stacks Project, Tag 08RM. Postcomposition with the universal derivation gives the unique morphism from the module of relative differentials to any coefficient sheaf.
theorem universalDerivation_isUniversal {X : TopCat.{u}}
{O₁ O₂ : TopCat.Sheaf CommRingCat.{max u v} X} (φ : O₁ ⟶ O₂) :
IsUniversal.{u, v, u_1} (universalDerivation.{u, v, u_1} φ)
Tag 01US, a lemma
Tag 01US in the Stacks Project.
Stacks.AlgebraicGeometry.DifferentialsRestrict.existsUnique_relativeDifferentials_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DifferentialsRestrict/Basic.lean, line 488.
Restricting a morphism of schemes to compatible open subschemes identifies the restriction of its sheaf of relative differentials with the sheaf of relative differentials of the restricted morphism, and this is the unique identification carrying the restricted universal derivation to the universal derivation.
theorem existsUnique_relativeDifferentials_restrict :
∃! i : Scheme.Modules.restrict (Scheme.Hom.relativeDifferentials f) U.ι ≅
Scheme.Hom.relativeDifferentials (f.resLE V U e),
∀ (W : U.toScheme.Opens) (x : Γ(U.toScheme, W)),
(i.hom.val.app (.op W)).hom
((Scheme.Modules.restrictAppIso U.ι
(Scheme.Hom.relativeDifferentials f) W).inv.hom
((Scheme.Hom.universalRelativeDerivation f).d (((U.ι.appIso W).inv).hom x))) =
(Scheme.Hom.universalRelativeDerivation (f.resLE V U e)).d x
Tag 01UO, a lemma
Tag 01UO in the Stacks Project.
AlgebraicGeometry.AffineDerivations.globalSectionsDerivation_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery252629/Chapter29.lean, line 708. References: EGA IV (16.5.2).
Stacks Project, Tag 01UO. On an affine scheme, evaluation on global sections gives a bijection from relative sheaf derivations to relative ring derivations.
theorem globalSectionsDerivation_bijective {R A : CommRingCat.{u}} (φ : R ⟶ A)
(F : SheafOfModules.{v} (SheafOfModules.underlyingRingSheaf (Spec A).sheaf)) :
Function.Bijective (globalSectionsDerivation φ F)
Tag 01UT, a lemma
Tag 01UT in the Stacks Project.
Stacks.AlgebraicGeometry.AffineDifferentialsIso.existsUnique_sectionsIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineDifferentialsIso/SpecComparison.lean, line 300. The attribute's comment: “affine case in the coordinate rings: the global differentials of Spec φ are Ω[A⁄R]”.
Uniqueness of the comparison of global differentials. There is exactly one isomorphism of
A-modules fromΩ[A⁄R]to the global differentials ofSpec φcompatible with the universal derivations.
theorem existsUnique_sectionsIso :
∃! e : CommRingCat.KaehlerDifferential φ ≅
moduleSpecΓFunctor.obj (Scheme.Hom.relativeDifferentials (Spec.map φ)),
∀ a : A, e.hom.hom (CommRingCat.KaehlerDifferential.d a) =
(Scheme.Hom.universalRelativeDerivation (Spec.map φ)).d ((Scheme.ΓSpecIso A).inv a)
Stacks.AlgebraicGeometry.AffineDifferentialsIso.existsUnique_tildeKaehlerIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineDifferentialsIso/SpecComparison.lean, line 358. The attribute's comment: “affine case as a sheaf comparison: Ω_{Spec A/Spec R} is the sheaf of Ω[A⁄R]”.
Uniqueness of the comparison of sheaves. There is exactly one isomorphism from the quasi-coherent sheaf associated to
Ω[A⁄R]to the sheaf of relative differentials ofSpec φcarrying the global section determined by the universal differential ofa : Ato the universal relative differential of the global section of𝒪_{Spec A}corresponding toa.
theorem existsUnique_tildeKaehlerIso :
∃! e : (tilde.functor A).obj (CommRingCat.KaehlerDifferential φ) ≅
Scheme.Hom.relativeDifferentials (Spec.map φ),
∀ a : A,
(tilde.toTildeΓNatIso.hom.app (CommRingCat.KaehlerDifferential φ) ≫
moduleSpecΓFunctor.map e.hom).hom (CommRingCat.KaehlerDifferential.d a) =
(Scheme.Hom.universalRelativeDerivation (Spec.map φ)).d
((Scheme.ΓSpecIso A).inv a)
Stacks.AlgebraicGeometry.AffineDifferentialsIso.existsUnique_affineDifferentialsIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineDifferentialsIso/Surjective.lean, line 481.
Stacks Project, Tag 01UT. Let
f : X ⟶ Sbe a morphism of schemes, letVbe an affine open ofSand letU ≤ f ⁻¹ᵁ Vbe an affine open ofX. The sections of the sheaf of relative differentials offonUare uniquely isomorphic to the Kähler differentials ofΓ(S, V) ⟶ Γ(X, U), compatibly with the universal derivations.
theorem existsUnique_affineDifferentialsIso (hV : IsAffineOpen V) :
∃! e : (Scheme.Hom.relativeDifferentials f).val.obj (.op U) ≅
CommRingCat.KaehlerDifferential (f.appLE V U hUV),
∀ a : Γ(X, U), e.hom.hom ((Scheme.Hom.universalRelativeDerivation f).d a) =
CommRingCat.KaehlerDifferential.d a
Stacks.Smooth.existsUnique_linearEquiv_universalD, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Smooth/CotangentSectionsAffineOpen.lean, line 310. The attribute's comment: “unique isomorphism Γ(U, Ω_{X/S}) = Ω_{A/R} compatible with the differentials”.
Let
f : X ⟶ Sbe a morphism of schemes. For any pair of affine opensSpec A = U ⊆ XandSpec R = V ⊆ Swithf(U) ⊆ Vthere is a unique isomorphism
Ω[A⁄R] ≃ₗ[A] Γ(Ω_{X/S}, U)compatible with
d_{X/S}and withd : A → Ω[A⁄R].
theorem existsUnique_linearEquiv_universalD (hU : IsAffineOpen U) (hV : IsAffineOpen V)
(hUV : U ≤ f ⁻¹ᵁ V) :
letI := algebraAppLE f hUV
∃! e : Ω[Γ(X, U)⁄Γ(S, V)] ≃ₗ[Γ(X, U)] Γ(cotangentSheaf f, U),
∀ b : Γ(X, U), e (KaehlerDifferential.D Γ(S, V) Γ(X, U) b) = universalD f U b
Tag 01UU, a remark
Tag 01UU in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.isBasis_affineOpensOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/AffineBasis.lean, line 143. The attribute's comment: “the affine opens mapping into an affine open of the base form a basis”.
The affine opens over affine opens form a basis. The affine opens of
Xmapping into an affine open ofSform a basis of the topology ofX.
theorem isBasis_affineOpensOver : Opens.IsBasis f.affineOpensOver
AlgebraicGeometry.Scheme.Hom.kaehlerOnAffineOpensOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/AffineBasis.lean, line 209. The attribute's comment: “the presheaf on the basis with sections the Kähler differentials”.
The ansatz
Γ(U, Ω_{X/S}) = Ω_{A/R}. The presheaf of modules on the basisf.affineOpensOver, over the restriction of𝒪_X, with sections the Kähler differentialsΩ_{A/R}overU = Spec Alying overV = Spec R. Its restriction maps are described bykaehlerOnAffineOpensOver_map_d.
noncomputable def kaehlerOnAffineOpensOver :
_root_.PresheafOfModules.{u} (restrictRingSheafToBasis
f.isBasis_affineOpensOver X.ringCatSheaf).obj
AlgebraicGeometry.Scheme.Hom.kaehlerOnAffineOpensOver_map_d, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/AffineBasis.lean, line 220. The attribute's comment: “the restriction maps”.
The restriction maps. For
U' ⊆ Uin the basis, the restriction mapΩ_{A/R} ⟶ Ω_{A'/R'}sendsd atod (a|_{U'}).
theorem kaehlerOnAffineOpensOver_map_d
{U U' : BasisCat f.affineOpensOver} (i : U' ⟶ U)
(a : Γ(X, U.obj)) :
(f.kaehlerOnAffineOpensOver.map i.op).hom (CommRingCat.KaehlerDifferential.d a) =
CommRingCat.KaehlerDifferential.d
(X.presheaf.map ((basisInclusion _).map i).op a)
AlgebraicGeometry.Scheme.Hom.isSheaf_kaehlerOnAffineOpensOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/AffineBasis.lean, line 235. The attribute's comment: “the sheaf condition”.
The sheaf condition. The presheaf with sections
Ω_{A/R}is a sheaf on the basis.
theorem isSheaf_kaehlerOnAffineOpensOver :
Presheaf.IsSheaf (basisGrothendieckTopology f.isBasis_affineOpensOver)
f.kaehlerOnAffineOpensOver.presheaf
AlgebraicGeometry.Scheme.Hom.restrictRelativeDifferentialsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/AffineBasis.lean, line 253. The attribute's comment: “the sheaf on the basis is the restriction of the sheaf of differentials”.
The construction gives
Ω_{X/S}. The restriction of the sheaf of relative differentials to the basisf.affineOpensOveris the sheaf with sectionsΩ_{A/R}; on sections it is the identification of Stacks 01UT (restrictRelativeDifferentialsIso_hom_app_d).
noncomputable def restrictRelativeDifferentialsIso :
(restrictModuleSheaf.{u, u} f.isBasis_affineOpensOver
X.ringCatSheaf).obj (relativeDifferentials f) ≅ f.kaehlerSheafOnAffineOpensOver
AlgebraicGeometry.Scheme.Hom.nonempty_iso_relativeDifferentials_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/AffineBasis.lean, line 270. The attribute's comment: “the sheaf on the basis determines the sheaf of differentials”.
The sheaf on the basis determines
Ω_{X/S}. A sheaf of𝒪_X-modules is isomorphic to the sheaf of relative differentials if and only if its restriction to the basisf.affineOpensOveris isomorphic to the sheaf with sectionsΩ_{A/R}.
theorem nonempty_iso_relativeDifferentials_iff (M : X.Modules) :
Nonempty (M ≅ relativeDifferentials f) ↔
Nonempty ((restrictModuleSheaf.{u, u} f.isBasis_affineOpensOver
X.ringCatSheaf).obj M ≅ f.kaehlerSheafOnAffineOpensOver)
Tag 08S2, a lemma
Tag 08S2 in the Stacks Project.
Stacks.Tag08S2Assembly.relativeDifferentialsIsoDiagonalConormal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Assembly/Basic.lean, line 543. References: EGA IV (16.3.1), “Ω¹_{X/S}=Gr₁(Δ_f)”; EGA IV (17.13.5); SGA 7 VI (5.5), “ordinary schemes”.
[Stacks, Tag 08S2]. The canonical isomorphism from the sheaf of relative differentials of
XoverSto the conormal sheaf of its diagonal inX ×_S X.This is
Stacks.LeibnizDerivation.diagonalConormalIso, whose single hypothesisIsIso (Stacks.LeibnizDerivation.toConormal f)is now discharged byisIso_toConormaland so is carried by no argument here:fis an arbitrary morphism of schemes, and nothing is affine, separated, Noetherian or quasi-compact.
noncomputable def relativeDifferentialsIsoDiagonalConormal :
Scheme.Hom.relativeDifferentials f ≅
Stacks.Conormal.conormalSheaf (pullback.diagonal f)
Stacks.Tag08S2Assembly.relativeDifferentialsIsoDiagonalConormal_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Assembly/Basic.lean, line 556. The attribute's comment: “canonical quotient formula”.
[Stacks, Tag 08S2], the canonical quotient formula. The comparison isomorphism sends
d bto the image ofp₂^♯ b - p₁^♯ bunder the canonical quotient map from the ideal sheaf of the diagonal to its conormal sheaf, on any openVof the coborder neighbourhood admitting the tag's two containments.This is
Stacks.LeibnizDerivation.diagonalConormalIso_hom_d_eq_quotientMap, again with its hypothesis discharged.
theorem relativeDifferentialsIsoDiagonalConormal_apply
(V : (pullback.diagonal f).coborderRange.toScheme.Opens)
(h₁ : (pullback.diagonal f).coborderRange.ι ''ᵁ V ≤
(pullback.fst f f) ⁻¹ᵁ ((pullback.diagonal f).liftCoborder ⁻¹ᵁ V))
(h₂ : (pullback.diagonal f).coborderRange.ι ''ᵁ V ≤
(pullback.snd f f) ⁻¹ᵁ ((pullback.diagonal f).liftCoborder ⁻¹ᵁ V))
(b : Γ(X, (pullback.diagonal f).liftCoborder ⁻¹ᵁ V))
(x : (Stacks.ClosedImmersion.idealSheaf
(pullback.diagonal f).liftCoborder.toLRSHom.toShHom).val.obj (.op V))
(hx : (kernel.ι (SheafOfModules.unitToPushforwardObjUnit (structureSheafHom
(pullback.diagonal f).liftCoborder.toLRSHom.toShHom))).val.app (.op V) x =
((pullback.snd f f).appLE _ _ h₂).hom b - ((pullback.fst f f).appLE _ _ h₁).hom b) :
((relativeDifferentialsIsoDiagonalConormal f).hom.val.app
(.op ((pullback.diagonal f).liftCoborder ⁻¹ᵁ V))).hom
((Scheme.Hom.universalRelativeDerivation f).d b) =
(Stacks.Conormal.conormalQuotientMap (pullback.diagonal f)
(pullback.diagonal f).coborderRange (pullback.diagonal f).liftCoborder
(pullback.diagonal f).liftCoborder_ι).val.app (.op V) x
Tag 01UV, a lemma
Tag 01UV in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.existsUnique_relativeDifferentialsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/Functoriality.lean, line 110. References: EGA IV (16.5.13), “more general”; EGA IV (17.3.6), “more general”; SGA 3 III (0.1.7), “partial”.
A commutative square of schemes induces a unique morphism
f^* Ω_{X/S} ⟶ Ω_{X'/S'}carrying the universal differential of every local section to the universal differential of its pullback.
theorem existsUnique_relativeDifferentialsMap {X' X S' S : Scheme.{u}} (f : X' ⟶ X)
(p : X ⟶ S) (p' : X' ⟶ S') (g : S' ⟶ S) (hcomm : f ≫ p = p' ≫ g) :
∃! c : (Scheme.Modules.pullback f).obj (relativeDifferentials p) ⟶
relativeDifferentials p', IsRelativeDifferentialsMap f p p' c
AlgebraicGeometry.Scheme.Hom.isRelativeDifferentialsMap_iff_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/Functoriality.lean, line 137. The attribute's comment: “characterization of the canonical map”.
Compatibility with the universal derivations characterizes the canonical morphism on relative differentials associated to a commutative square of schemes.
theorem isRelativeDifferentialsMap_iff_eq {X' X S' S : Scheme.{u}} (f : X' ⟶ X)
(p : X ⟶ S) (p' : X' ⟶ S') (g : S' ⟶ S) (hcomm : f ≫ p = p' ≫ g)
(c : (Scheme.Modules.pullback f).obj (relativeDifferentials p) ⟶
relativeDifferentials p') :
IsRelativeDifferentialsMap f p p' c ↔ c = relativeDifferentialsMap f p p' g hcomm
Tag 01UX, a lemma
Tag 01UX in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.toRelativeDifferentials_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/Triangle.lean, line 181. The attribute's comment: “exactness at the right term”.
Stacks Project, Tag 01UX. The canonical map
Ω_{X/S} ⟶ Ω_{X/Y}of a composable pair of morphisms of schemes is an epimorphism; equivalently, the canonical sequencef^* Ω_{Y/S} ⟶ Ω_{X/S} ⟶ Ω_{X/Y} ⟶ 0is exact atΩ_{X/Y}. For the underlying ringed spaces this is Stacks Project, Tag 0H79.
theorem toRelativeDifferentials_epi (f : X ⟶ Y) (g : Y ⟶ S) :
Epi (f.toRelativeDifferentials g)
AlgebraicGeometry.Scheme.Hom.toRelativeDifferentials_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/Triangle.lean, line 195. The attribute's comment: “exactness at the middle term”.
Stacks Project, Tag 01UX. For morphisms of schemes
f : X ⟶ Yandg : Y ⟶ Sthe canonical maps of relative differentials, both obtained fromAlgebraicGeometry.Scheme.Hom.relativeDifferentialsMap, form a complexf^* Ω_{Y/S} ⟶ Ω_{X/S} ⟶ Ω_{X/Y}which is exact atΩ_{X/S}. Together withAlgebraicGeometry.Scheme.Hom.toRelativeDifferentials_epithis is the exactness off^* Ω_{Y/S} ⟶ Ω_{X/S} ⟶ Ω_{X/Y} ⟶ 0. For the underlying ringed spaces this is Stacks Project, Tag 0H79.
theorem toRelativeDifferentials_exact (f : X ⟶ Y) (g : Y ⟶ S) :
∃ h : relativeDifferentialsMap f g (f ≫ g) (𝟙 S) (Category.comp_id (f ≫ g)).symm ≫
f.toRelativeDifferentials g = 0,
(ShortComplex.mk _ _ h).Exact
Tag 01V0, a lemma
Tag 01V0 in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.isIso_relativeDifferentialsMap_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/BaseChange.lean, line 119.
Stacks Project, Tag 01V0. For a cartesian square of schemes with left edge
f' : X' ⟶ S', right edgef : X ⟶ Sand top edgeg' : X' ⟶ X, the canonical mapg'^* Ω_{X/S} ⟶ Ω_{X'/S'}of Tag 01UV is an isomorphism.
theorem isIso_relativeDifferentialsMap_of_isPullback {X' X S' S : Scheme.{u}} (g' : X' ⟶ X)
(f' : X' ⟶ S') (f : X ⟶ S) (g : S' ⟶ S) (h : IsPullback g' f' f g) :
IsIso (relativeDifferentialsMap g' f f' g h.w)
Tag 01V1, a lemma
Tag 01V1 in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.isIso_biprodDesc_relativeDifferentialsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/BaseChange.lean, line 152. References: EGA IV (16.4.23).
Stacks Project, Tag 01V1. Let
f : X ⟶ Sandg : Y ⟶ Sbe morphisms of schemes with the same target and letp : W ⟶ X,q : W ⟶ Ybe the projections of a fibre product offandg. The two canonical maps of Tag 01UV give an isomorphismp^* Ω_{X/S} ⊕ q^* Ω_{Y/S} ⟶ Ω_{W/S}.
theorem isIso_biprodDesc_relativeDifferentialsMap {W X Y S : Scheme.{u}} (p : W ⟶ X) (q : W ⟶ Y)
(f : X ⟶ S) (g : Y ⟶ S) (h : IsPullback p q f g) :
IsIso (biprod.desc
(relativeDifferentialsMap p f (p ≫ f) (𝟙 S) (Category.comp_id (p ≫ f)).symm)
(relativeDifferentialsMap q g (p ≫ f) (𝟙 S)
(h.w.symm.trans (Category.comp_id (p ≫ f)).symm)))
Tag 01V2, a lemma
Tag 01V2 in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.isFiniteType_relativeDifferentials, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/FiniteType.lean, line 86. References: EGA IV (17.4.1.2).
Stacks Project, Tag 01V2. The sheaf of relative differentials of a morphism of schemes which is locally of finite type is an
𝒪_X-module of finite type.
instance Scheme.Hom.isFiniteType_relativeDifferentials (f : X ⟶ S) [LocallyOfFiniteType f] :
(Scheme.Hom.relativeDifferentials f).IsFiniteType
Tag 01V3, a lemma
Tag 01V3 in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.isFinitePresentation_relativeDifferentials, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/FinitePresentation.lean, line 85. References: EGA IV (16.4.22); EGA IV (17.4.1.2), “special case”; SGA 3 III (0.14), “more general”.
Stacks Project, Tag 01V3. The sheaf of relative differentials of a morphism of schemes which is locally of finite presentation is an
𝒪_X-module of finite presentation.
instance Scheme.Hom.isFinitePresentation_relativeDifferentials (f : X ⟶ S)
[LocallyOfFinitePresentation f] :
(Scheme.Hom.relativeDifferentials f).IsFinitePresentation
Tag 01UY, a lemma
Tag 01UY in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.isZero_relativeDifferentials_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Differentials.lean, line 75.
The sheaf of relative differentials of a monomorphism of schemes is a zero object.
theorem isZero_relativeDifferentials_of_mono (f : X ⟶ S) [Mono f] :
IsZero (relativeDifferentials f)
AlgebraicGeometry.Scheme.Hom.isZero_relativeDifferentials_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Differentials.lean, line 81. The attribute's comment: “the immersion case named in the first clause of the statement”.
The sheaf of relative differentials of an immersion of schemes is a zero object.
theorem isZero_relativeDifferentials_of_isImmersion (f : X ⟶ S) [IsImmersion f] :
IsZero (relativeDifferentials f)
Tag 01UZ, a lemma
Tag 01UZ in the Stacks Project.
Stacks.ConormalSequenceRight.differentialsMapOver_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalSequenceRight/Basic.lean, line 257. The attribute's comment: “exactness at the right term”. References: EGA IV (16.4.21), “→ 0 (surjectivity)”.
[Stacks, Tag 01UZ], exactness at the right term. For an immersion
i : Z ⟶ Xof schemes overS, the canonical mapi^*Ω_{X/S} ⟶ Ω_{Z/S}of [Stacks, Tag 01UV] is an epimorphism, so the conormal sequence ofiends in zero.
theorem differentialsMapOver_epi (i : Z ⟶ X) [IsImmersion i] (p : X ⟶ S) :
Epi (Scheme.Hom.relativeDifferentialsMap i p (i ≫ p) (𝟙 S) (by simp))
Stacks.ConormalSequenceRight.conormalDifferential, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalSequenceRight/Basic.lean, line 380. The attribute's comment: “the first arrow”.
[Stacks, Tag 01UZ], the first arrow. For an immersion
i : Z ⟶ Xof schemes overS, the canonical morphism𝒞_{Z/X} ⟶ i^*Ω_{X/S}induced byd_{X/S}: the adjoint transpose of the map carrying a sectionfof the defining ideal sheaf of the closed factor to1 ⊗ d f.
noncomputable def conormalDifferential :
(conormalSheaf i : Z.Modules) ⟶
(Scheme.Modules.pullback i).obj (Scheme.Hom.relativeDifferentials p)
Stacks.ConormalSequenceRight.equationDifferentialsComplexOver_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalSequenceRight/Middle.lean, line 395. The attribute's comment: “exactness at the middle term”.
[Stacks, Tag 01UZ], exactness at the middle term. For an immersion
i : Z ⟶ Xof schemes overScut out by global sectionsf jof𝒪_X, the conormal sequence is exact ati^*Ω_{X/S}: the kernel of the canonical mapi^*Ω_{X/S} ⟶ Ω_{Z/S}of [Stacks, Tag 01UV] is generated by the pulled-back differentialsd (f j), which generate the image of the conormal module of the immersion.
theorem equationDifferentialsComplexOver_exact (i : Z ⟶ X) [IsImmersion i] (p : X ⟶ S)
{I : Type u} (f : I → Γ(X, ⊤)) (hf : IsCutOutBy i f) :
(equationDifferentialsComplex i p (by simp) f hf).Exact
Stacks.ConormalSequenceRight.conormalShortComplex_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalSequenceRight/SchemeShortExact.lean, line 359. The attribute's comment: “exactness at the middle term of the sequence 𝒞_{Z/X} ⟶ i^*Ω_{X/S} ⟶ Ω_{Z/S}, for an arbitrary immersion and with the conormal sheaf itself at the left-hand end”. References: SGA 7 XI (1.3), “partial”.
[Stacks, Tag 01UZ], exactness at the middle term of the conormal sequence, unconditionally. For an immersion of schemes
i : Z ⟶ Xoverp : X ⟶ Sthe conormal sequence𝒞_{Z/X} ⟶ i^*Ω_{X/S} ⟶ Ω_{Z/S} ⟶ 0is exact ati^*Ω_{X/S}: the image of the conormal differential is the kernel of the canonical map of [Stacks, Tag 01UV].No hypothesis beyond
IsImmersion iis used, and the sequence is the canonical one rather than a presentation by equations. Injectivity of the first arrow, which would make the sequence short exact, is false in general and holds under the smoothness hypothesis of [Stacks, Tag 06AA]; seeStacks.ConormalSequenceRight.conormalShortComplex_shortExact.
theorem conormalShortComplex_exact (p : X ⟶ S) : (conormalShortComplex i p).Exact
Declarations registered for the tag:
AlgebraicGeometry.Scheme.Hom.relativeDifferentialsMap, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/ConormalSequenceRight/Basic.lean, line 539 (StacksFrontier): “the functorial second arrow”.
Tag 0474, a lemma
Tag 0474 in the Stacks Project.
Stacks.ConormalSequenceSplit.isSplitEpi_differentialsMapOver_of_retraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalSequenceSplit/Basic.lean, line 175. The attribute's comment: “a left inverse splits the second arrow”.
[Stacks, Tag 0474], a left inverse splits the second arrow. For an immersion
i : Z ⟶ Xof schemes overSadmitting a left inverseg : X ⟶ ZoverS, the second arrowi^*Ω_{X/S} ⟶ Ω_{Z/S}of the conormal sequence of [Stacks, Tag 01UZ] is a split epimorphism.Together with
Stacks.ConormalSequenceRight.differentialsMapOver_epithis is the right-hand half of the source's conclusion. Split exactness of the three-term sequence, which this statement supplies the section for, isStacks.ConormalSequenceSplit.conormalShortComplexSplitting_of_retraction.
theorem isSplitEpi_differentialsMapOver_of_retraction (i : Z ⟶ X) [IsImmersion i] (p : X ⟶ S)
(g : X ⟶ Z) (hg : i ≫ g = 𝟙 Z) (hgS : g ≫ (i ≫ p) = p) :
IsSplitEpi (relativeDifferentialsMap i p (i ≫ p) (𝟙 S) (by simp))
Stacks.ConormalSequenceSplit.forall_exists_isSplitEpi_restrict_of_localRetraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalSequenceSplit/Basic.lean, line 251. The attribute's comment: “a local left inverse locally splits the second arrow”.
[Stacks, Tag 0474], a local left inverse locally splits the second arrow. Let
i : Z ⟶ Xbe an immersion of schemes overSwhich locally has a left inverse: every pointzofZhas an open neighbourhoodVwhichimaps into an openUofX, the restricted morphismj : V ⟶ Uadmitting a left inverseg : U ⟶ VoverS. Then the second arrowi^*Ω_{X/S} ⟶ Ω_{Z/S}of the conormal sequence of [Stacks, Tag 01UZ] restricts to a split epimorphism on a neighbourhood of every point ofZ.This is the "(locally)" reading of the source's hypothesis and conclusion, on the second arrow. Local split exactness of the three-term sequence is
Stacks.ConormalSequenceSplit.forall_exists_nonempty_splitting_restrict_of_localRetraction, which combines this splitting with the short exactnessStacks.ConormalSequenceSplit.conormalShortComplex_shortExact_of_localRetractionproved under the same hypothesis.
theorem forall_exists_isSplitEpi_restrict_of_localRetraction
(i : Z ⟶ X) [IsImmersion i] (p : X ⟶ S)
(hloc : ∀ z : Z, ∃ (V : Z.Opens) (U : X.Opens) (j : V.toScheme ⟶ U.toScheme)
(g : U.toScheme ⟶ V.toScheme), z ∈ V ∧ V.ι ≫ i = j ≫ U.ι ∧ j ≫ g = 𝟙 V.toScheme ∧
g ≫ (V.ι ≫ i ≫ p) = U.ι ≫ p) :
∀ z : Z, ∃ V : Z.Opens, z ∈ V ∧
IsSplitEpi ((Scheme.Modules.pullback V.ι).map
(relativeDifferentialsMap i p (i ≫ p) (𝟙 S) (by simp)))
Stacks.ConormalSequenceSplit.conormalShortComplex_shortExact_of_localRetraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalSequenceSplit/ShortExact.lean, line 499. The attribute's comment: “the local clause: under a local left inverse — every point of Z has a neighbourhood V mapping into an open U of X with the restricted morphism admitting a left inverse over S — the sequence 0 ⟶ 𝒞_{Z/X} ⟶ i^*Ω_{X/S} ⟶ Ω_{Z/S} ⟶ 0 of Tag 01UZ is short exact. This is exactness, globally; the local splitting under the same hypothesis is forall_exists_nonempty_splitting_restrict_of_localRetraction”.
[Stacks, Tag 0474], short exactness under a local left inverse. Let
i : Z ⟶ Xbe an immersion of schemes overp : X ⟶ Swhich locally has a left inverse: every pointzofZhas an open neighbourhoodVwhichimaps into an openUofX, the restricted morphismj : V ⟶ Uadmitting a left inverseg : U ⟶ VoverS. Then the conormal sequence0 ⟶ 𝒞_{Z/X} ⟶ i^*Ω_{X/S} ⟶ Ω_{Z/S} ⟶ 0of [Stacks, Tag 01UZ] is short exact.This is the exactness half of the source's locally split exact under the source's local hypothesis, and it is global: being a monomorphism is a stalkwise condition, so a left inverse near each point is enough. The splitting half under the same hypothesis is
Stacks.ConormalSequenceSplit.forall_exists_isSplitEpi_restrict_of_localRetraction, which splits the second arrow over a neighbourhood of every point; the two combine into the local split exactnessStacks.ConormalSequenceSplit.forall_exists_nonempty_splitting_restrict_of_localRetraction.
theorem conormalShortComplex_shortExact_of_localRetraction {Z X S : Scheme.{u}} (i : Z ⟶ X)
[IsImmersion i] (p : X ⟶ S)
(hloc : ∀ z : Z, ∃ (V : Z.Opens) (U : X.Opens) (j : V.toScheme ⟶ U.toScheme)
(g : U.toScheme ⟶ V.toScheme), z ∈ V ∧ V.ι ≫ i = j ≫ U.ι ∧ j ≫ g = 𝟙 V.toScheme ∧
g ≫ (V.ι ≫ i ≫ p) = U.ι ≫ p) :
(conormalShortComplex i p).ShortExact
Stacks.ConormalSequenceSplit.conormalShortComplexSplitting_of_retraction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalSequenceSplit/ShortExact.lean, line 523. The attribute's comment: “a left inverse over S splits the sequence 0 ⟶ 𝒞_{Z/X} ⟶ i^*Ω_{X/S} ⟶ Ω_{Z/S} ⟶ 0 of Tag 01UZ: a splitting is produced, so in particular the sequence is short exact. The hypothesis is a global left inverse g : X ⟶ Z with i ≫ g = 𝟙 Z and g ≫ (i ≫ p) = p; the source's parenthetical local clause is forall_exists_nonempty_splitting_restrict_of_localRetraction”.
[Stacks, Tag 0474], a left inverse splits the sequence. For an immersion
i : Z ⟶ Xof schemes overp : X ⟶ Sadmitting a left inverseg : X ⟶ ZoverS, the conormal sequence0 ⟶ 𝒞_{Z/X} ⟶ i^*Ω_{X/S} ⟶ Ω_{Z/S} ⟶ 0of [Stacks, Tag 01UZ] is split short exact: a splitting is produced, consisting of a retraction of the first arrow and a section of the second whose composites add up to the identity ofi^*Ω_{X/S}.The section of the second arrow is the source's
i^*c_g, throughStacks.ConormalSequenceSplit.isSplitEpi_differentialsMapOver_of_retraction; the sequence is short exact byStacks.ConormalSequenceSplit.conormalShortComplex_shortExact_of_retraction, and a short exact sequence whose epimorphism has a section is split.
noncomputable def conormalShortComplexSplitting_of_retraction {Z X S : Scheme.{u}} (i : Z ⟶ X)
[IsImmersion i] (p : X ⟶ S) (g : X ⟶ Z) (hg : i ≫ g = 𝟙 Z) (hgS : g ≫ (i ≫ p) = p) :
(conormalShortComplex i p).Splitting
Stacks.ConormalSequenceSplit.forall_exists_nonempty_splitting_restrict_of_localRetraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalSequenceSplit/ShortExact.lean, line 582. The attribute's comment: “the parenthetical local clause: under a local left inverse — every point of Z has a neighbourhood V mapping into an open U of X with the restricted morphism j : V ⟶ U admitting a left inverse over S — the sequence 0 ⟶ 𝒞_{Z/X} ⟶ i^Ω_{X/S} ⟶ Ω_{Z/S} ⟶ 0 of Tag 01UZ is locally split exact*: every point of Z has an open neighbourhood V over which the restricted sequence carries a ShortComplex.Splitting, so both a retraction of the first arrow and a section of the second are produced over V. This is the full (locally) reading of the source's hypothesis and conclusion; the global reading is conormalShortComplexSplitting_of_retraction”. References: EGA IV (16.4.21), “special case”.
[Stacks, Tag 0474], a local left inverse makes the conormal sequence locally split exact. Let
i : Z ⟶ Xbe an immersion of schemes overp : X ⟶ Swhich locally has a left inverse: every pointzofZhas an open neighbourhoodVwhichimaps into an openUofX, the restricted morphismj : V ⟶ Uadmitting a left inverseg : U ⟶ VoverS. Then every point ofZhas an open neighbourhoodVover which the conormal sequence0 ⟶ 𝒞_{Z/X} ⟶ i^*Ω_{X/S} ⟶ Ω_{Z/S} ⟶ 0of [Stacks, Tag 01UZ] is split short exact: the sequence restricted toVcarries aCategoryTheory.ShortComplex.Splitting.This is the source's (locally) split exact under the source's (locally) has a left inverse. The neighbourhood produced is the one the hypothesis supplies, and the splitting over it is
Stacks.ConormalSequenceSplit.conormalShortComplexRestrictSplitting_of_localRetraction.
theorem forall_exists_nonempty_splitting_restrict_of_localRetraction
{Z X S : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i] (p : X ⟶ S)
(hloc : ∀ z : Z, ∃ (V : Z.Opens) (U : X.Opens) (j : V.toScheme ⟶ U.toScheme)
(g : U.toScheme ⟶ V.toScheme), z ∈ V ∧ V.ι ≫ i = j ≫ U.ι ∧ j ≫ g = 𝟙 V.toScheme ∧
g ≫ (V.ι ≫ i ≫ p) = U.ι ≫ p) :
∀ z : Z, ∃ V : Z.Opens, z ∈ V ∧
Nonempty (((conormalShortComplex i p).map
(Scheme.Modules.restrictFunctor V.ι)).Splitting)
Stacks.ConormalSequenceSplit.isIso_conormalDifferential_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalSequenceSplit/ShortExact.lean, line 606. The attribute's comment: “the source's final assertion: for a section s of p, the first arrow 𝒞_{S/X} ⟶ s^*Ω_{X/S} of the sequence of Tag 01UZ, which is induced by d_{X/S}, is an isomorphism”. References: SGA 6 VIII (2.2), “(b)”.
[Stacks, Tag 0474], the conormal sheaf of a section. For a section
s : S ⟶ Xofp : X ⟶ Sthe first arrow𝒞_{S/X} ⟶ s^*Ω_{X/S}of the conormal sequence of [Stacks, Tag 01UZ] is an isomorphism.A section is an immersion whose left inverse over
Sispitself, so the sequence ofsis short exact; andΩ_{S/S}is a zero object by [Stacks, Tag 01UY],s ≫ p = 𝟙 Sbeing a monomorphism. The first arrow is therefore both a monomorphism and, the sequence being exact at the middle term with zero on the right, an epimorphism.
theorem isIso_conormalDifferential_of_section {X S : Scheme.{u}} (p : X ⟶ S) (s : S ⟶ X)
(hs : s ≫ p = 𝟙 S) :
haveI := isImmersion_of_section p s hs
IsIso (conormalDifferential s p)
Tag 060N, a remark
Tag 060N in the Stacks Project.
Stacks.DiagonalSplitSequence.diagonalBiprodIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/DiagonalSplitSequence.lean, line 353. The attribute's comment: “the middle term: Δ^*Ω_{X ×_S X/S} = Ω_{X/S} ⊕ Ω_{X/S}”.
[Stacks, Tag 060N]:
Δ^* Ω_{X ×_S X/S} = Ω_{X/S} ⊕ Ω_{X/S}. The direct sum decompositionΩ_{X ×_S X/S} = pr_1^* Ω_{X/S} ⊕ pr_2^* Ω_{X/S}of [Stacks, Tag 01V1], pulled back along the diagonal: the two summands becomeΩ_{X/S}becauseΔ ≫ pr_i = id.
noncomputable def diagonalBiprodIso :
relativeDifferentials f ⊞ relativeDifferentials f ≅
(Scheme.Modules.pullback (pullback.diagonal f)).obj
(relativeDifferentials (pullback.fst f f ≫ f))
Stacks.DiagonalSplitSequence.diagonalBiprodIso_hom_comp_diagonalDifferentialsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/DiagonalSplitSequence.lean, line 363. The attribute's comment: “the right arrow is (1,1)”.
[Stacks, Tag 060N]: the right arrow is
(1, 1). Under the identificationΔ^* Ω_{X ×_S X/S} = Ω_{X/S} ⊕ Ω_{X/S}the canonical mapΔ^* Ω_{X ×_S X/S} ⟶ Ω_{X/S}of [Stacks, Tag 01UV] — the second arrow of the conormal sequence ofΔ— is(1, 1).
theorem diagonalBiprodIso_hom_comp_diagonalDifferentialsMap :
(diagonalBiprodIso f).hom ≫ diagonalDifferentialsMap f =
biprod.desc (𝟙 (relativeDifferentials f)) (𝟙 (relativeDifferentials f))
Stacks.DiagonalSplitSequence.isSplitEpi_diagonalDifferentialsMap, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/DiagonalSplitSequence.lean, line 374. The attribute's comment: “the right arrow is a split surjection”.
[Stacks, Tag 060N]: the right arrow is a split surjection. The diagonal has the global left inverse
pr_1overS, so the second arrow of its conormal sequence is a split epimorphism; this is [Stacks, Tag 0474] forΔ.
instance isSplitEpi_diagonalDifferentialsMap : IsSplitEpi (diagonalDifferentialsMap f)
Stacks.DiagonalSplitSequence.leftArrow_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/DiagonalSplitSequence.lean, line 398. The attribute's comment: “the left arrow is (-1,1)”.
[Stacks, Tag 060N]: the left arrow is
(-1, 1). Written through the identificationΔ^* Ω_{X ×_S X/S} = Ω_{X/S} ⊕ Ω_{X/S}it is the difference of the two projection inclusions.
theorem leftArrow_eq : leftArrow f = sndInclusion f - fstInclusion f
Stacks.DiagonalSplitSequence.pullbackSection_d_diffSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/DiagonalSplitSequence.lean, line 476. The attribute's comment: “the footnote: the left arrow on sections”.
[Stacks, Tag 060N], the footnote. The local section
d_{X/S} b = p_2^♯ b - p_1^♯ bof the ideal sheaf of the diagonal is carried byd_{X ×_S X/S}, pulled back alongΔ, topr_2^* d_{X/S} b - pr_1^* d_{X/S} b; that is, to the image ofd_{X/S} bunder the map(-1, 1)of the direct sum decomposition. This is what fixes the sign of the left arrow.
theorem pullbackSection_d_diffSection (U : X.Opens) (b : Γ(X, U)) :
Scheme.Modules.pullbackSection (pullback.diagonal f)
(relativeDifferentials (pullback.fst f f ≫ f)) (Stacks.Diagonal.prodOpen f U) U
(Stacks.Diagonal.le_diagonal_preimage_prodOpen f U)
((universalRelativeDerivation (pullback.fst f f ≫ f)).d
(Stacks.Diagonal.diffSection f U b)) =
((leftArrow f).val.app (op U)) ((universalRelativeDerivation f).d b)
Stacks.DiagonalSplitSequence.shortComplex_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/DiagonalSplitSequence.lean, line 528. The attribute's comment: “the canonical short exact sequence”.
[Stacks, Tag 060N]: the canonical short exact sequence.
theorem shortComplex_shortExact : (shortComplex f).ShortExact
Tag 067L, a lemma
Tag 067L in the Stacks Project.
Stacks.ConormalSequenceTwoImmersions.epi_conormalDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/TwoImmersionsConormalExact.lean, line 79. The attribute's comment: “surjectivity of the second arrow 𝒞_{Z/X} ⟶ i^*Ω_{X/Y}, which is the ⟶ 0 at the right-hand end of the sequence”.
[Stacks, Tag 067L], surjectivity of the second arrow. For immersions
i : Z ⟶ Xandj : Z ⟶ Yin a commutative trianglei ≫ p = j, the second arrow𝒞_{Z/X} ⟶ i^*Ω_{X/Y}of the conormal sequence is an epimorphism, which is the⟶ 0at its right-hand end.The sequence of [Stacks, Tag 01UZ] for
ioverpis exact ati^*Ω_{X/Y}and continues byi^*Ω_{X/Y} ⟶ Ω_{Z/Y}, whose target vanishes becausejis an immersion, hence formally unramified.
theorem epi_conormalDifferential {Z X Y : Scheme.{u}} (i : Z ⟶ X) (j : Z ⟶ Y) (p : X ⟶ Y)
[IsImmersion i] [IsImmersion j] (h : i ≫ p = j) :
Epi (Stacks.ConormalSequenceRight.conormalDifferential i p)
Stacks.ConormalSequenceTwoImmersions.conormalTransitivityMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/TwoImmersionsConormalSequence.lean, line 112. The attribute's comment: “the first arrow”.
[Stacks, Tag 067L], the first arrow. For immersions
i : Z ⟶ Xandj : Z ⟶ Yin a commutative trianglei ≫ p = j, the canonical map𝒞_{Z/Y} ⟶ 𝒞_{Z/X}of conormal sheaves.It is the canonical map of [Stacks, Tag 01R4] for the square whose top morphism is
𝟙 Z, transported along the identification of pullback along an identity with the identity functor.
def conormalTransitivityMap (h : i ≫ p = j) :
Stacks.Conormal.conormalSheaf j ⟶ Stacks.Conormal.conormalSheaf i
Stacks.ConormalSequenceTwoImmersions.conormalDifferentialModules, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UnramifiedPairSplitConormalSequence.lean, line 1166. The attribute's comment: “the second arrow 𝒞_{Z/X} ⟶ i^*Ω_{X/Y}, in the spelling that composes with the first arrow: the conormal differential of Tag 01UZ for i over p, read through the identification conormalSheafComparisonIso of the two presentations of 𝒞_{Z/X}”.
The second arrow
𝒞_{Z/X} ⟶ i^*Ω_{X/Y}of [Stacks, Tag 067L], with its source in the spelling the first arrow uses. The conormal differential of [Stacks, Tag 01UZ] is built on the pullback of a sectionwise kernel and the first arrow on the pullback of the categorical kernel;Stacks.ConormalSequenceUnramifiedPair.conormalSheafComparisonIsoidentifies the two presentations, and this arrow is the conormal differential read through it.
def conormalDifferentialModules :
immersionConormalSheafModules i ⟶
(Scheme.Modules.pullback i).obj (Scheme.Hom.relativeDifferentials p)
Stacks.ConormalSequenceTwoImmersions.conormalTransitivityMapModules_comp_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UnramifiedPairSplitConormalSequence.lean, line 1177. The attribute's comment: “the composite 𝒞_{Z/Y} ⟶ 𝒞_{Z/X} ⟶ i^*Ω_{X/Y} of the two arrows vanishes, so they form a complex; only the commutative triangle i ≫ p = j of immersions is assumed”.
[Stacks, Tag 067L]: the two arrows of the conormal sequence form a complex. The composite
𝒞_{Z/Y} ⟶ 𝒞_{Z/X} ⟶ i^*Ω_{X/Y}vanishes, for immersionsi : Z ⟶ Xandj : Z ⟶ Yin a commutative trianglei ≫ p = jand with no hypothesis onp.
theorem conormalTransitivityMapModules_comp_eq_zero (h : i ≫ p = j) :
conormalTransitivityMapModules i j p h ≫ conormalDifferentialModules i p = 0
Stacks.ConormalSequenceTwoImmersions.conormalShortComplexModules_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UnramifiedPairSplitConormalSequence.lean, line 1188. The attribute's comment: “exactness at the middle term 𝒞_{Z/X}: the image of the first arrow 𝒞_{Z/Y} ⟶ 𝒞_{Z/X} is the kernel of the second arrow 𝒞_{Z/X} ⟶ i^*Ω_{X/Y}; only the commutative triangle i ≫ p = j of immersions is assumed”.
[Stacks, Tag 067L]: the conormal sequence of two immersions is exact at
𝒞_{Z/X}. The kernel of the second arrow𝒞_{Z/X} ⟶ i^*Ω_{X/Y}is exactly the image of the first arrow𝒞_{Z/Y} ⟶ 𝒞_{Z/X}, for immersionsi : Z ⟶ Xandj : Z ⟶ Yin a commutative trianglei ≫ p = jand with no hypothesis onp.
theorem conormalShortComplexModules_exact (h : i ≫ p = j) :
(ShortComplex.mk _ _
(conormalTransitivityMapModules_comp_eq_zero i j p h)).Exact
Sources
Section29.34 Finite order differential operators#
Section 29.34 of the Stacks Project, Tag 0G43. 3 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0G44, a lemma
Tag 0G44 in the Stacks Project.
AlgebraicGeometry.AffineDiffOp.globalDiffOpEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/AffineDifferentialOperators.lean, line 1080.
On an affine scheme, taking global sections gives a bijection from differential operators of order at most
kbetween sheaves to differential operators of order at mostkbetween the corresponding modules. The source sheaf is required to be quasi-coherent; the target sheaf is arbitrary.
noncomputable def globalDiffOpEquiv
{R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
(F G : (Spec (.of A)).Modules) [F.IsQuasicoherent] (k : ℕ) :
letI _modAF : Module A Γ(F, ⊤) :=
Module.compHom _ (Scheme.ΓSpecIso (.of A)).inv.hom
letI _modAG : Module A Γ(G, ⊤) :=
Module.compHom _ (Scheme.ΓSpecIso (.of A)).inv.hom
letI _modRF : Module R Γ(F, ⊤) := Module.compHom _ (algebraMap R A)
letI _modRG : Module R Γ(G, ⊤) := Module.compHom _ (algebraMap R A)
letI _towerF : IsScalarTower R A Γ(F, ⊤) := IsScalarTower.of_compHom R A _
letI _towerG : IsScalarTower R A Γ(G, ⊤) := IsScalarTower.of_compHom R A _
{e :
{D : DiffOp.GlobalOp F G //
DiffOp.IsGlobalDiffOpOfOrder
(Scheme.Hom.relativeStructureSheafMap
(Spec.map (CommRingCat.ofHom (algebraMap R A)))) k D} ≃
{D : Γ(F, ⊤) →ₗ[R] Γ(G, ⊤) //
D.IsDifferentialOperatorOfOrderLE A k} //
∀ D x, (e D).1 x = D.1 (.op ⊤) x}
Tag 0G45, a lemma
Tag 0G45 in the Stacks Project.
Stacks.FibreProductAffineChart.Chart.diffOpEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/ChartBaseChange.lean, line 205. The attribute's comment: “the affine-chart reduction step of the proof: over an affine chart of X ×_S Y, the differential operators of order at most k on X ×_S Y / Y are the differential operators of order at most k relative to B ⟶ A ⊗_R B on the chart's sections. Neither the construction of D' nor its characterisation on pure tensors is included”.
Differential operators on an affine chart of a fibre product. The differential operators of order at most
konX ×_S Y / Ybetween two modules onX ×_S Y, defined over the opens contained in a chart, are the differential operators of order at mostkrelative toΓ(Y, V) ⟶ Γ(X, U) ⊗_{Γ(S, W)} Γ(Y, V)between the two modules of sections on the chart.
noncomputable def diffOpEquiv (M M' : (pullback a b).Modules)
[(Scheme.Modules.restrict M ((c.specIso hl hr).inv ≫ c.ι)).IsQuasicoherent] (k : ℕ) :
letI _modAF : Module (Γ(X, c.left) ⊗[Γ(S, c.base)] Γ(Y, c.right))
Γ(Scheme.Modules.restrict M ((c.specIso hl hr).inv ≫ c.ι), ⊤) :=
Module.compHom _ (Scheme.ΓSpecIso
(.of (Γ(X, c.left) ⊗[Γ(S, c.base)] Γ(Y, c.right)))).inv.hom
letI _modAG : Module (Γ(X, c.left) ⊗[Γ(S, c.base)] Γ(Y, c.right))
Γ(Scheme.Modules.restrict M' ((c.specIso hl hr).inv ≫ c.ι), ⊤) :=
Module.compHom _ (Scheme.ΓSpecIso
(.of (Γ(X, c.left) ⊗[Γ(S, c.base)] Γ(Y, c.right)))).inv.hom
letI _modRF : Module Γ(Y, c.right)
Γ(Scheme.Modules.restrict M ((c.specIso hl hr).inv ≫ c.ι), ⊤) :=
Module.compHom _ (algebraMap Γ(Y, c.right)
(Γ(X, c.left) ⊗[Γ(S, c.base)] Γ(Y, c.right)))
letI _modRG : Module Γ(Y, c.right)
Γ(Scheme.Modules.restrict M' ((c.specIso hl hr).inv ≫ c.ι), ⊤) :=
Module.compHom _ (algebraMap Γ(Y, c.right)
(Γ(X, c.left) ⊗[Γ(S, c.base)] Γ(Y, c.right)))
letI _towerF : IsScalarTower Γ(Y, c.right) (Γ(X, c.left) ⊗[Γ(S, c.base)] Γ(Y, c.right))
Γ(Scheme.Modules.restrict M ((c.specIso hl hr).inv ≫ c.ι), ⊤) :=
IsScalarTower.of_compHom _ _ _
letI _towerG : IsScalarTower Γ(Y, c.right) (Γ(X, c.left) ⊗[Γ(S, c.base)] Γ(Y, c.right))
Γ(Scheme.Modules.restrict M' ((c.specIso hl hr).inv ≫ c.ι), ⊤) :=
IsScalarTower.of_compHom _ _ _
{D : DiffOp.RawOp M M' c.ι.opensRange //
DiffOp.IsDiffOpOfOrder (pullback.snd a b).relativeStructureSheafMap k D} ≃
{D : Γ(Scheme.Modules.restrict M ((c.specIso hl hr).inv ≫ c.ι), ⊤) →ₗ[Γ(Y, c.right)]
Γ(Scheme.Modules.restrict M' ((c.specIso hl hr).inv ≫ c.ι), ⊤) //
D.IsDifferentialOperatorOfOrderLE
(Γ(X, c.left) ⊗[Γ(S, c.base)] Γ(Y, c.right)) k}
AlgebraicGeometry.globalDiffOp_ext_of_chart_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/ChartBaseChange.lean, line 327. The attribute's comment: “the local-global step of the proof: a differential operator of order at most k on X ×_S Y / Y out of a quasi-coherent module is determined by its action on the sections over the affine charts. This is not the uniqueness clause of the tag, which is uniqueness among the operators satisfying the characterisation on pure tensors”.
A differential operator on a fibre product is determined by its action on the affine charts. Two differential operators of order at most
konX ×_S Y / Y, out of a quasi-coherent module, which agree on the sections over every affine chart ofX ×_S Y, are equal.
theorem globalDiffOp_ext_of_chart_sections {X Y S : Scheme.{u}} (a : X ⟶ S) (b : Y ⟶ S) (k : ℕ)
{M M' : (pullback a b).Modules} [M.IsQuasicoherent] (D E : DiffOp.GlobalOp M M')
(hD : DiffOp.IsGlobalDiffOpOfOrder (pullback.snd a b).relativeStructureSheafMap k D)
(hE : DiffOp.IsGlobalDiffOpOfOrder (pullback.snd a b).relativeStructureSheafMap k E)
(hagree : ∀ (c : Chart a b) (s : Γ(M, c.ι.opensRange)),
D (op c.ι.opensRange) s = E (op c.ι.opensRange) s) :
D = E
AlgebraicGeometry.existsUnique_globalDiffOp_externalTensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/ChartBoxOperatorGluing.lean, line 290.
Base change of a differential operator. Let
a : X ⟶ Sandb : Y ⟶ Sbe morphisms of schemes, letF,F'be quasi-coherent𝒪_X-modules, letGbe a quasi-coherent𝒪_Y-module and letD : F ⟶ F'be a differential operator of order at mostkonX/S. There is a unique differential operator of order at mostkonX ×_S Y / Yfrompr₁^*F ⊗ pr₂^*Gtopr₁^*F' ⊗ pr₂^*Gwhich carries, for all local sectionssofFandtofG, the section attached tosandtto the section attached toD sandt.
theorem existsUnique_globalDiffOp_externalTensorProduct {X Y S : Scheme.{u}} (a : X ⟶ S)
(b : Y ⟶ S) (F F' : X.Modules) (G : Y.Modules)
[F.IsQuasicoherent] [F'.IsQuasicoherent] [G.IsQuasicoherent] (k : ℕ)
(D : DiffOp.GlobalOp F F')
(hD : DiffOp.IsGlobalDiffOpOfOrder a.relativeStructureSheafMap k D) :
∃! E : DiffOp.GlobalOp (externalTensorProduct a b F G) (externalTensorProduct a b F' G),
DiffOp.IsGlobalDiffOpOfOrder (pullback.snd a b).relativeStructureSheafMap k E ∧
∀ (U' : X.Opens) (V' : Y.Opens) (s : Γ(F, U')) (t : Γ(G, V'))
(W : (pullback a b).Opens) (hW₁ : W ≤ pullback.fst a b ⁻¹ᵁ U')
(hW₂ : W ≤ pullback.snd a b ⁻¹ᵁ V'),
E (op W) (externalTensorSection a b F G s t W hW₁ hW₂) =
externalTensorSection a b F' G (D (op U') s) t W hW₁ hW₂
Stacks.FibreProductAffineChart.Chart.existsUnique_boxDiffOp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/ChartBoxProductOperator.lean, line 492. The attribute's comment: “the affine-chart step of the construction of D': over ONE affine chart of X ×_S Y this gives the existence of D', its order bound, its characterisation on pure tensors and its uniqueness, all read through the identification of the sections of F ⊠ G on the chart with Γ(Spec A, F) ⊗_R Γ(Spec B, G). The global operator on X ×_S Y is NOT constructed: the chart-wise operators are not glued, and the characterisation is not expressed on the sections of F ⊠ G attached to a pair of local sections of F and of G”.
The affine-chart base change of a differential operator (Tag 0G45 on a chart). Let
D : F ⟶ F'be a differential operator of order at mostkonX/Sbetween quasi-coherent modules and letGbe a quasi-coherent𝒪_Y-module. Over the opens of an affine chart ofX ×_S Ythere is exactly one differential operator of order at mostkonX ×_S Y / YfromF ⊠ GtoF' ⊠ Gwhich, read through the identification of the sections of a box product on the chart withΓ(Spec Γ(X, U), F) ⊗_{Γ(S, W)} Γ(Spec Γ(Y, V), G), carriess ⊗ ttoD s ⊗ t.
theorem existsUnique_boxDiffOp (F' : X.Modules) [F'.IsQuasicoherent] (k : ℕ)
(D : DiffOp.GlobalOp F F')
(hD : DiffOp.IsGlobalDiffOpOfOrder a.relativeStructureSheafMap k D) :
∃! E : {E : DiffOp.RawOp (externalTensorProduct a b F G) (externalTensorProduct a b F' G)
c.ι.opensRange //
DiffOp.IsDiffOpOfOrder (pullback.snd a b).relativeStructureSheafMap k E},
∀ (s : Γ((Scheme.Modules.pullback c.fromSpecLeft).obj F, ⊤))
(t : Γ((Scheme.Modules.pullback c.fromSpecRight).obj G, ⊤)),
(c.boxDiffOpTensorEquiv hl hr F G F' k E).1 (s ⊗ₜ[Γ(S, c.base)] t) =
(c.leftDiffOpEquiv hl F F' k
⟨D.restrict c.fromSpecLeft.opensRange, hD c.fromSpecLeft.opensRange⟩).1 s
⊗ₜ[Γ(S, c.base)] t
Tag 0G46, a remark
Tag 0G46 in the Stacks Project.
Stacks.FibreProductAffineChart.Chart.boxHom_boxSectionOfTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/BoxProductAffineDescription.lean, line 395. The attribute's comment: “the MORPHISM half of the affine description of the remark: on an affine chart of X ×_S Y, and so in particular for X = Spec A, Y = Spec B, S = Spec R and the chart whose three opens are everything, the operator D ⊠ E read on the sections of F ⊠ G through the identification of those sections with M ⊗_R N is D ⊗ E. Carries a chosen order bound for each of the two operators (hD, hE), which exists for every morphism of the category. The OBJECT half (M, N) ↦ M ⊗_R N is Chart.boxSectionsEquiv”.
The affine description of the box product on morphisms. Read on the sections of
F ⊠ Gover the image of a chart, through the identification of those sections withΓ(Spec A, F) ⊗_R Γ(Spec B, G), the operatorD ⊠ Eis the tensor productD ⊗ Eof the operator attached toDonΓ(Spec A, F)and the operator attached toEonΓ(Spec B, G).
theorem boxHom_boxSectionOfTensor
(z : Γ((Scheme.Modules.pullback c.fromSpecLeft).obj F.module, ⊤) ⊗[Γ(S, c.base)]
Γ((Scheme.Modules.pullback c.fromSpecRight).obj G.module, ⊤)) :
(AlgebraicGeometry.FiniteOrderDifferentialOperatorCategory.boxHom D E).1
(op (((c.specIso hl hr).inv ≫ c.ι) ''ᵁ ⊤))
(c.boxSectionOfTensor hl hr F.module G.module z) =
c.boxSectionOfTensor hl hr F'.module G'.module
(TensorProduct.map
(c.leftDiffOpEquiv hl F.module F'.module k
⟨D.1.restrict c.fromSpecLeft.opensRange, hD c.fromSpecLeft.opensRange⟩).1
(c.rightDiffOpEquiv hr G.module G'.module l
⟨E.1.restrict c.fromSpecRight.opensRange, hE c.fromSpecRight.opensRange⟩).1 z)
AlgebraicGeometry.FiniteOrderDifferentialOperatorCategory.boxHom_add_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/BoxProductFunctor.lean, line 200. The attribute's comment: “half of the bilinearity on morphisms asserted by the remark: the box product D ⊠ E is additive in the operator D on X/S”.
The box product is additive in its first argument.
theorem boxHom_add_left {F F' : FiniteOrderDifferentialOperatorCategory a}
{G G' : FiniteOrderDifferentialOperatorCategory b} (D D' : F ⟶ F') (E : G ⟶ G') :
boxHom (D + D') E = boxHom D E + boxHom D' E
AlgebraicGeometry.FiniteOrderDifferentialOperatorCategory.boxHom_add_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/BoxProductFunctor.lean, line 210. The attribute's comment: “the other half of the bilinearity on morphisms asserted by the remark: the box product D ⊠ E is additive in the operator E on Y/S”.
The box product is additive in its second argument.
theorem boxHom_add_right {F F' : FiniteOrderDifferentialOperatorCategory a}
{G G' : FiniteOrderDifferentialOperatorCategory b} (D : F ⟶ F') (E E' : G ⟶ G') :
boxHom D (E + E') = boxHom D E + boxHom D E'
AlgebraicGeometry.FiniteOrderDifferentialOperatorCategory.boxProductFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/BoxProductFunctor.lean, line 225. The attribute's comment: “the box product bifunctor of the remark: (F, G) ↦ F ⊠ G on objects and (D, E) ↦ D ⊠ E on morphisms, with both functor laws. NOT the notation F ⊠ G, and NOT the affine description (M, N) ↦ M ⊗_R N, (D, D') ↦ D ⊗ D', which is covered by Chart.boxSectionsEquiv and Chart.boxHom_boxSectionOfTensor”.
The box-product bifunctor of [Stacks, Tag 0G46]. The external tensor product on objects and the box product of two differential operators on morphisms form a functor from the product of the categories of finite-order differential operators on
X/Sand onY/Sto the category of finite-order differential operators onX ×_S Y / S.
noncomputable def boxProductFunctor (a : X ⟶ S) (b : Y ⟶ S) :
FiniteOrderDifferentialOperatorCategory a × FiniteOrderDifferentialOperatorCategory b ⥤
FiniteOrderDifferentialOperatorCategory (pullback.fst a b ≫ a)
AlgebraicGeometry.FiniteOrderDifferentialOperatorCategory.boxHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/BoxProductRightOperator.lean, line 218. The attribute's comment: “the assignment on morphisms of the box product of the remark: for D : F ⟶ F' on X/S and E : G ⟶ G' on Y/S the operator D ⊠ E = (1 ⊠ E) ∘ (D ⊠ 1), a morphism F ⊠ G ⟶ F' ⊠ G' of the category of finite-order differential operators on X ×_S Y / S. The FUNCTOR of the remark is not constructed HERE: map_id, map_comp and the bilinearity on morphisms are proved in BoxProductFunctor, and the affine description (M, N) ↦ M ⊗_R N, (D, D') ↦ D ⊗ D' in BoxProductAffineDescription”.
The box product
D ⊠ Eof two finite-order differential operators. For morphismsD : F ⟶ F'of the category of finite-order differential operators onX/SandE : G ⟶ G'of the category onY/S, the composite(1 ⊠ E) ∘ (D ⊠ 1) : F ⊠ G ⟶ F' ⊠ G'of the category of finite-order differential operators onX ×_S Y / S.
def boxHom {F F' : FiniteOrderDifferentialOperatorCategory a}
{G G' : FiniteOrderDifferentialOperatorCategory b} (D : F ⟶ F') (E : G ⟶ G') :
boxProductObj F G ⟶ boxProductObj F' G'
Stacks.FibreProductAffineChart.Chart.boxSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/ChartBoxProductOperator.lean, line 442. The attribute's comment: “the OBJECT half of the affine description of the remark: on an affine chart of X ×_S Y, and so in particular for X = Spec A, Y = Spec B, S = Spec R and the chart whose three opens are everything, the module of sections of F ⊠ G is M ⊗_R N, linearly over the ring A ⊗_R B of the chart. NOT the morphism half (D, D') ↦ D ⊗ D', which is Chart.boxHom_boxSectionOfTensor”.
The sections of a box product on a chart. The module of sections of
F ⊠ Gon a chart is the tensor product overΓ(S, W)of the sections ofFonSpec Γ(X, U)and ofGonSpec Γ(Y, V), linearly overΓ(X, U) ⊗_{Γ(S, W)} Γ(Y, V), which acts on the tensor product by(f ⊗ g) • (s ⊗ t) = (f • s) ⊗ (g • t).
noncomputable def boxSectionsEquiv :
Γ((Scheme.Modules.pullback ((c.specIso hl hr).inv ≫ c.ι)).obj
(externalTensorProduct a b F G), ⊤)
≃ₗ[Γ(X, c.left) ⊗[Γ(S, c.base)] Γ(Y, c.right)]
(Γ((Scheme.Modules.pullback c.fromSpecLeft).obj F, ⊤) ⊗[Γ(S, c.base)]
Γ((Scheme.Modules.pullback c.fromSpecRight).obj G, ⊤))
AlgebraicGeometry.externalTensorProduct, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/ExternalTensorProduct.lean, line 43. The attribute's comment: “external_tensor_product_of_modules”.
The external tensor product of an
O_X-module and anO_Y-module on the fibre product of two schemesXandYoverS.
noncomputable abbrev externalTensorProduct {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)
(F : X.Modules) (G : Y.Modules) : (pullback f g).Modules
AlgebraicGeometry.FiniteOrderDifferentialOperatorCategory, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/FiniteOrderCategory.lean, line 69. The attribute's comment: “category_of_finite_order_differential_operators”.
A quasi-coherent module, regarded as an object of the category of finite-order differential operators on
X/S.
structure FiniteOrderDifferentialOperatorCategory (a : X ⟶ S)
AlgebraicGeometry.FiniteOrderDifferentialOperatorCategory.Hom, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/FiniteOrderCategory.lean, line 131. The attribute's comment: “category_of_finite_order_differential_operators”.
Morphisms in the category of finite-order differential operators.
noncomputable abbrev Hom (F G : FiniteOrderDifferentialOperatorCategory a)
AlgebraicGeometry.FiniteOrderDifferentialOperatorCategory.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/FiniteOrderCategory.lean, line 159. The attribute's comment: “category_of_finite_order_differential_operators”.
Composition of finite-order differential operators makes quasi-coherent modules into a category.
noncomputable instance instCategory :
Category (FiniteOrderDifferentialOperatorCategory a)
AlgebraicGeometry.FiniteOrderDifferentialOperatorCategory.instPreadditive, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/FiniteOrderCategory.lean, line 186. The attribute's comment: “category_of_finite_order_differential_operators”.
The pointwise addition of finite-order differential operators is compatible with composition.
noncomputable instance instPreadditive :
Preadditive (FiniteOrderDifferentialOperatorCategory a)
Sources
Section29.35 Smooth morphisms#
Section 29.35 of the Stacks Project, Tag 01V4. 21 tags here are carried by 19 declarations of the repository (all in StacksFrontier) and 10 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 01V5, a definition
Tag 01V5 in the Stacks Project.
AlgebraicGeometry.IsStandardSmooth, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/Defs.lean, line 79. The attribute's comment: “standard_smooth_affine”.
A morphism of affine schemes is standard smooth if the corresponding ring homomorphism on global sections is standard smooth.
public abbrev IsStandardSmooth {X S : AlgebraicGeometry.Scheme.{u}}
[AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine S] (f : X ⟶ S) : Prop
Declarations registered for the tag:
InfinitesimalLifting.SmoothAt, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/AtPoint.lean, line 69 (StacksFrontier): “smooth_at_point”.AlgebraicGeometry.Smoothregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/Defs.lean, line 63 (StacksFrontier): “smooth_morphism”. References: EGA IV (17.3.1); SGA 1 II (1.1); SGA 3 XI (1.1); SGA 3 XI (1.6); SGA 7 XIV (2.1), “partial”.
Tag 01V6, a lemma
Tag 01V6 in the Stacks Project.
RingHom.Smooth.stacksPropertyIsLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/LocallyOfType.lean, line 114. The attribute's comment: “smoothness of ring maps is local”.
Smoothness of ring maps is a local property.
theorem Smooth.stacksPropertyIsLocal : StacksPropertyIsLocal RingHom.Smooth
AlgebraicGeometry.smooth_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/LocallyOfType.lean, line 256. The attribute's comment: “moreover: restriction to open subschemes”.
If
fis smooth then so is its restrictionU → Vto any opensU ⊆ X,V ⊆ Swithf(U) ⊆ V.
theorem smooth_resLE {f : X ⟶ S} (hf : Smooth f) (V : S.Opens) (U : X.Opens)
(e : U ≤ f ⁻¹ᵁ V) : Smooth (f.resLE V U e)
AlgebraicGeometry.smooth_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/LocallyOfType.lean, line 264. The attribute's comment: “equivalence of (1), (2), (3) and (4)”.
Smoothness of a morphism of schemes can be checked on all pairs of affine opens, on open coverings of target and preimages, or on affine such coverings.
theorem smooth_tfae (f : X ⟶ S) :
List.TFAE [
Smooth f,
∀ (V : S.affineOpens) (U : X.affineOpens) (e : U.1 ≤ f ⁻¹ᵁ V.1),
(f.appLE V U e).hom.Smooth,
∃ 𝒱 : Set S.Opens, sSup 𝒱 = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.Opens, sSup 𝒰 = f ⁻¹ᵁ V ∧
∀ U ∈ 𝒰, ∃ e : U ≤ f ⁻¹ᵁ V, Smooth (f.resLE V U e),
∃ 𝒱 : Set S.affineOpens, (⨆ V ∈ 𝒱, V.1) = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.affineOpens,
(⨆ U ∈ 𝒰, U.1) = f ⁻¹ᵁ V.1 ∧ ∀ U ∈ 𝒰, ∃ e : U.1 ≤ f ⁻¹ᵁ V.1,
(f.appLE V U e).hom.Smooth]
AlgebraicGeometry.smooth_tfae_and_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/LocallyOfType.lean, line 280.
The whole statement: the four characterizations of smoothness agree, and smoothness passes to restrictions to open subschemes.
theorem smooth_tfae_and_resLE (f : X ⟶ S) :
List.TFAE [
Smooth f,
∀ (V : S.affineOpens) (U : X.affineOpens) (e : U.1 ≤ f ⁻¹ᵁ V.1),
(f.appLE V U e).hom.Smooth,
∃ 𝒱 : Set S.Opens, sSup 𝒱 = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.Opens, sSup 𝒰 = f ⁻¹ᵁ V ∧
∀ U ∈ 𝒰, ∃ e : U ≤ f ⁻¹ᵁ V, Smooth (f.resLE V U e),
∃ 𝒱 : Set S.affineOpens, (⨆ V ∈ 𝒱, V.1) = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.affineOpens,
(⨆ U ∈ 𝒰, U.1) = f ⁻¹ᵁ V.1 ∧ ∀ U ∈ 𝒰, ∃ e : U.1 ≤ f ⁻¹ᵁ V.1,
(f.appLE V U e).hom.Smooth] ∧
(Smooth f → ∀ (U : X.Opens) (V : S.Opens) (e : U ≤ f ⁻¹ᵁ V), Smooth (f.resLE V U e))
Tag 01V8, a lemma
Tag 01V8 in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.Smooth.of_smooth_fiberToSpecResidueFieldregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/FlatSmoothFibres.lean, line 20 (StacksFrontier). References: EGA IV (17.5.1), “b)⇒a), global form”; EGA IV (17.8.2), “special case”; SGA 1 II (2.1), “sufficiency, global form”; SGA 1 II (2.2), “sufficiency with Y=S”; SGA 3 VIB (3.10), “partial”; SGA 3 VIB (4.4), “more general”; SGA 3 VIB (8.4), “(ii)”; SGA 3 VIII (2.1), “partial”; SGA 3 XI (1.2), “(i)”; SGA 3 XV (1.1), “partial”.
Tag 01VA, a lemma
Tag 01VA in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.smooth_compregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 252 (StacksFrontier). References: EGA IV (17.3.3), “smooth branch of (ii)”; EGA IV (6.8.3), “more general”; SGA 1 II (1.3), “more general”.
Tag 01VB, a lemma
Tag 01VB in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.smooth_isStableUnderBaseChangeregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/SmoothMorphisms/Basic.lean, line 56 (StacksFrontier): “the base change of a smooth morphism is smooth”. References: EGA IV (17.3.3), “smooth branch of (iii)”; EGA IV (17.7.3), “(ii)”; EGA IV (6.8.2), “globally smooth f”; EGA IV (6.8.3), “more general”; SGA 1 II (1.3), “more general”; SGA 1 II (4.13), “global ascent”; SGA 3 VIB (10.1), “smooth morphisms”; SGA 3 VIB (2.1.2), “partial”; SGA 3 XIX (2.1), “(i)”; SGA 6 VIII (1.6), “partial”; SGA 6 VIII (1.8), “partial”; SGA 6 X (7.13.3), “partial”.
Tag 01VC, a lemma
Tag 01VC in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.instSmoothOfIsOpenImmersionregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 253 (StacksFrontier). References: SGA 1 II (1.3), “more general”.
Tag 01VD, a lemma
Tag 01VD in the Stacks Project.
AlgebraicGeometry.syntomic_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/SmoothMorphisms/Basic.lean, line 45.
A smooth morphism of schemes is syntomic.
theorem syntomic_of_smooth {X S : Scheme.{u}} (f : X ⟶ S) [Smooth f] : Syntomic f
Tag 01VE, a lemma
Tag 01VE in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.instLocallyOfFinitePresentationOfSmoothregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 254 (StacksFrontier). References: SGA 3 III (0.6), “partial”; SGA 3 III (2.5), “partial”.
Tag 01VF, a lemma
Tag 01VF in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.instFlatOfSmoothregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 255 (StacksFrontier). References: EGA IV (17.5.1), “a)⇒flatness in b)”; EGA IV (17.5.2), “necessity”; EGA IV (17.15.15), “necessity: flatness”; SGA 1 II (2.1), “necessity of (a)”; SGA 1 IX (1.2), “more general”; SGA 3 VIB (8.4), “(ii)”; SGA 3 XI (1.2), “(i)”.
Tag 056G, a lemma
Tag 056G in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.UniversallyOpen.of_flatregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 320 (StacksFrontier): “flat and locally of finite presentation; smooth morphisms are both (instances)”. References: EGA IV (1.10.4), “b) ⇒ a), special case”; EGA IV (11.3.1), “special case”; EGA IV (14.4.10), “special case”; EGA IV (15.2.1); EGA IV (15.2.4), “(ii), special case”; EGA IV (18.2.7), “partial”; EGA IV (2.4.6); EGA IV (2.4.7), “more general”; EGA IV (4.4.1), “special case”; SGA 1 IV (6.6), “F = O_X”; SGA 1 VIII (4.9), “more general”; SGA 3 V (10.1.1), “more general”; SGA 3 V (4.1.1), “flat and fp implies open”; SGA 3 VIA (2.5.4), “Final implication”; SGA 3 VIB (3.11), “more general”; SGA 3 VIB (4.3); SGA 3 VIB (7.5), “f|_V is an open morphism”; SGA 3 X (5.4), “partial”; SGA 3 XVI (2.1), “more general”; SGA 6 VIII (1.3), “more general”.
Tag 01V7, a lemma
Tag 01V7 in the Stacks Project.
InfinitesimalLifting.smoothAt_iff_exists_affine_isStandardSmooth, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/AtPoint.lean, line 145.
Smoothness at a point is equivalent to standard smoothness on a suitable affine neighbourhood lying over any prescribed affine neighbourhood of the image point.
public lemma smoothAt_iff_exists_affine_isStandardSmooth
{X S : Scheme.{u}} (f : X ⟶ S) (x : X) (V : S.Opens)
(hV : IsAffineOpen V) (hxV : x ∈ f ⁻¹ᵁ V) :
InfinitesimalLifting.SmoothAt f x ↔
∃ (U : X.Opens) (hU : IsAffineOpen U) (_ : x ∈ U)
(hUV : U ≤ f ⁻¹ᵁ V),
@AlgebraicGeometry.IsStandardSmooth
U.toScheme V.toScheme hU hV (f.resLE V U hUV)
Tag 02G1, a lemma
Tag 02G1 in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.isFiniteLocallyFree_relativeDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/DifferentialsLocallyFree.lean, line 86. The attribute's comment: “differentials_finite_locally_free”. References: EGA IV (17.15.15), “necessity: Ω loc free”; EGA IV (17.10.2), “locally free”; EGA IV (17.15.5), “a) => c) (free)”; SGA 1 II (4.3), “(ii) local freeness”; SGA 3 XI (1.9), “finite locally free”.
The sheaf of relative differentials of a smooth morphism of schemes is finite locally free.
theorem Scheme.Hom.isFiniteLocallyFree_relativeDifferentials (f : X ⟶ S) [Smooth f] :
SheafOfModules.IsFiniteLocallyFree (R := X.ringCatSheaf)
(Scheme.Hom.relativeDifferentials f)
AlgebraicGeometry.finrank_stalk_relativeDifferentials_eq_fiberDimensionAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/DifferentialsRank.lean, line 76. The attribute's comment: “differentials_rank_eq_fibre_dimension”. References: EGA IV (17.10.2), “rank_x = dim_x f”; EGA IV (17.15.5), “a) => c) rank”; EGA IV (17.15.15), “smooth ⇒ rank=dim_x f”; SGA 3 XI (1.9), “rank = fiber dimension”; SGA 1 II (4.3), “(ii) rank formula”.
Stacks Project, Tag 02G1. For a smooth morphism of schemes, the rank at a point of the sheaf of relative differentials is the local dimension of the fibre at that point.
theorem finrank_stalk_relativeDifferentials_eq_fiberDimensionAt {X S : Scheme.{u}} (f : X ⟶ S)
[Smooth f] (x : X) :
(Module.finrank (ToType (X.sheaf.presheaf.stalk x))
(ToType (TopCat.Presheaf.stalk (C := AddCommGrpCat.{u})
(Scheme.Hom.relativeDifferentials f).val.presheaf x)) : WithBot ℕ∞) =
topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x)
Tag 02G2, a definition
Tag 02G2 in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.SmoothOfRelativeDimensionregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/Defs.lean, line 70 (StacksFrontier). References: SGA 1 II (1.5), “special case”; SGA 4 XVII (6.3.8), “partial”; SGA 7 XIV (2.1), “partial”; SGA 7 XVIII (5.6.8).
Tag 01V9, a lemma
Tag 01V9 in the Stacks Project.
Stacks.FiberCotangentAssembly.fiberDifferentialsTensorIdentification, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiberCotangentAssembly/Basic.lean, line 461. The attribute's comment: “canonical identification in part (4)”.
The fibre of the sheaf of relative differentials at
xis canonically identified with the fibre of the relative differentials of the scheme-theoretic fibre.
public noncomputable def fiberDifferentialsTensorIdentification :
FiberDifferentialsTensorIdentification f x
Stacks.Tag01V9NumericalCriterion.smoothAt_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NumericalCriterion/Basic.lean, line 95.
For a morphism locally of finite presentation, the following are equivalent: smoothness at
x; flatness of the local-ring map together with smoothness of the scheme-theoretic fibre; either of the two numerical differential criteria; a standard smooth affine neighbourhood; and an affine presentation whose chosen Jacobian determinant does not vanish atx.
public theorem smoothAt_tfae [LocallyOfFinitePresentation f] :
List.TFAE [
InfinitesimalLifting.SmoothAt f x,
(f.stalkMap x).hom.Flat ∧
InfinitesimalLifting.SmoothAt (f.fiberToSpecResidueField (f x)) (f.asFiber x),
(f.stalkMap x).hom.Flat ∧
(let B := X.presheaf.stalk x
let Ω := relativeDifferentialStalk f x
letI := relativeDifferentialStalkModule f x
GeneratedByAtMost B Ω (topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x))),
(f.stalkMap x).hom.Flat ∧
(let k := X.residueField x
GeneratedByAtMost k (relativeCotangentSpace f x)
(topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x))),
∃ (U : X.affineOpens) (V : S.affineOpens) (_ : x ∈ U.1)
(hUV : U.1 ≤ f ⁻¹ᵁ V.1),
AlgebraicGeometry.IsStandardSmooth (f.resLE V.1 U.1 hUV),
∃ (U : X.affineOpens) (V : S.affineOpens) (hxU : x ∈ U.1)
(hUV : U.1 ≤ f ⁻¹ᵁ V.1),
letI : Algebra Γ(S, V.1) Γ(X, U.1) := (f.appLE V U hUV).hom.toAlgebra
∃ (n c : ℕ) (P : Algebra.PreSubmersivePresentation
Γ(S, V.1) Γ(X, U.1) (Fin n) (Fin c)),
P.jacobian ∉ (U.2.primeIdealOf ⟨x, hxU⟩).asIdeal]
Tag 02V4, a lemma
Tag 02V4 in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_preimage_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/LocusBaseChange.lean, line 111. References: EGA IV (17.7.2), “(ii)”; EGA IV (17.7.4), “(v)”; EGA IV (17.7.1), “(ii) smooth”; SGA 1 II (4.13), “special case”; SGA 3 VIB (2.5), “special case”; SGA 3 VIB (3.10), “special case”; SGA 3 X (8.9), “partial”.
The smooth locus of a base change is the inverse image of the smooth locus. Let
be a cartesian diagram of schemes, withX' → X ↓ ↓ S' → Sf : X ⟶ Slocally of finite presentation. Assume thatfis flat, or thatg : S' ⟶ Sis flat. Then the open subscheme ofX'where the base-changed morphismf' : X' ⟶ S'is smooth is the inverse image underg' : X' ⟶ Xof the open subscheme ofXwherefis smooth.Stacks Project, Tag 02V4. Both of its cases are covered, the first by flatness of
fand the second by flatness ofg.
theorem Scheme.Hom.smoothLocus_eq_preimage_of_isPullback {f : X ⟶ S} {g : S' ⟶ S} {f' : X' ⟶ S'}
{g' : X' ⟶ X} [LocallyOfFinitePresentation f] [LocallyOfFinitePresentation f']
(sq : IsPullback g' f' f g) (hflat : Flat f ∨ Flat g) :
f'.smoothLocus = g' ⁻¹ᵁ f.smoothLocus
Tag 02K4, a lemma
Tag 02K4 in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.toRelativeDifferentials_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/FormallySmooth.lean, line 318. References: EGA IV (17.2.3).
For morphisms of schemes
f : X ⟶ Yandg : Y ⟶ Swithfformally smooth, the canonical sequence0 ⟶ f^* Ω_{Y/S} ⟶ Ω_{X/S} ⟶ Ω_{X/Y} ⟶ 0of𝒪_X-modules is short exact. The case of a smoothfis the special case obtained fromStacks.Smooth.smooth_iff_locallyOfFinitePresentation_and_formallySmooth.
theorem toRelativeDifferentials_shortExact (f : X ⟶ Y) (g : Y ⟶ S) (hf : FormallySmooth f) :
∃ h : relativeDifferentialsMap f g (f ≫ g) (𝟙 S) (Category.comp_id (f ≫ g)).symm ≫
f.toRelativeDifferentials g = 0,
(ShortComplex.mk _ _ h).ShortExact
Tag 06AA, a lemma
Tag 06AA in the Stacks Project.
Stacks.ConormalSequenceRight.conormalShortComplex_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalSequenceRight/SchemeShortExact.lean, line 399. References: SGA 7 XI (1.3), “partial”.
[Stacks, Tag 06AA]. For an immersion of schemes
i : Z ⟶ Xoverp : X ⟶ SwithZsmooth overS, the conormal sequence0 ⟶ 𝒞_{Z/X} ⟶ i^*Ω_{X/S} ⟶ Ω_{Z/S} ⟶ 0of [Stacks, Tag 01UZ] is short exact.A smooth morphism is formally smooth by [Stacks, Tag 02H6], and formal smoothness is all the proof uses.
theorem conormalShortComplex_shortExact {Z X S : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i]
(p : X ⟶ S) (hZ : AlgebraicGeometry.Smooth (i ≫ p)) :
(conormalShortComplex i p).ShortExact
Tag 06AB, a lemma
Tag 06AB in the Stacks Project.
Stacks.ConormalSequenceTwoImmersions.mono_conormalTransitivityMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/TwoImmersionsConormalMono.lean, line 451. The attribute's comment: “exactness on the left, that is, that the first arrow 𝒞_{Z/Y} ⟶ 𝒞_{Z/X} of the sequence of 067L is a monomorphism. Exactness at 𝒞_{Z/X} and surjectivity onto i^*Ω_{X/Y} are the content of 067L and are not restated here; they are proved in the modules named in the module docstring, which also says where the second arrow of the sequence is.”.
[Stacks, Tag 06AB], exactness on the left. For immersions
i : Z ⟶ Xandj : Z ⟶ Yin a commutative trianglei ≫ p = jwithpsmooth, the canonical map𝒞_{Z/Y} ⟶ 𝒞_{Z/X}of [Stacks, Tag 067L] is a monomorphism.A smooth morphism induces a smooth, hence formally smooth, ring map on every compatible pair of affine opens, so this is
mono_conormalTransitivityMap_of_formallySmooth.
theorem mono_conormalTransitivityMap [Smooth p] (h : i ≫ p = j) :
Mono (conormalTransitivityMap i j p h)
Tag 02K5, a lemma
Tag 02K5 in the Stacks Project.
Stacks.Smooth.smooth_of_comp_surjective_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SmoothDescent.lean, line 143.
Stacks Project, Tag 02KM (smooth case). If
fis surjective and smooth andf ≫ qis smooth, thenqis smooth.This is also Stacks 02K5: there the target of
f ≫ qis additionally assumed locally of finite presentation, which that source's own footnote observes is implied by the other hypotheses.
theorem smooth_of_comp_surjective_smooth (f : X ⟶ Y) (q : Y ⟶ S) [Surjective f] [Smooth f]
[Smooth (f ≫ q)] : Smooth q
Tag 05D9, a lemma
Tag 05D9 in the Stacks Project.
AlgebraicGeometry.exists_affineOpens_free_conormal_powerSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/Section.lean, line 253.
At a smooth point of a section, there are compatible affine open neighbourhoods on which the conormal module is free and the completion is a formal power series algebra over the base.
public theorem exists_affineOpens_free_conormal_powerSeries
{X S : Scheme.{u}} (f : X ⟶ S) (σ : S ⟶ X)
(hσ : σ ≫ f = 𝟙 S) (s : S)
(hsmooth : InfinitesimalLifting.SmoothAt f (σ s)) :
∃ (U : S.Opens) (V : X.Opens) (_ : IsAffineOpen U)
(_ : IsAffineOpen V) (_ : s ∈ U) (_ : σ s ∈ V)
(hVU : V ≤ f ⁻¹ᵁ U) (hUV : U ≤ σ ⁻¹ᵁ V),
let A := Γ(S, U)
let B := Γ(X, V)
letI : Algebra A B := (f.appLE U V hVU).hom.toAlgebra
∃ (sectionHom : B →ₐ[A] A),
sectionHom.toRingHom = (σ.appLE V U hUV).hom ∧
(letI : Algebra B A := sectionHom.toAlgebra
Module.Free A (RingHom.ker sectionHom.toRingHom).Cotangent) ∧
(letI : Algebra B A := sectionHom.toAlgebra
Nonempty (AdicCompletion (RingHom.ker sectionHom.toRingHom) B ≃ₐ[A]
MvPowerSeries (Fin (Module.finrank A
(RingHom.ker sectionHom.toRingHom).Cotangent)) A))
Tag 0AFF, a lemma
Tag 0AFF in the Stacks Project.
AlgebraicGeometry.topologicalKrullDimAt_eq_add_topologicalKrullDimAt_fiber_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/SmoothDimensionFormula.lean, line 44.
Stacks Project, Tag 0AFF. For a smooth morphism of locally Noetherian schemes the dimension of the source at a point is the dimension of the target at its image plus the dimension of the fibre at that point.
public theorem topologicalKrullDimAt_eq_add_topologicalKrullDimAt_fiber_of_smooth
{X Y : Scheme.{u}} [IsLocallyNoetherian X] [IsLocallyNoetherian Y] (f : X ⟶ Y) [Smooth f]
(x : X) :
topologicalKrullDimAt X x =
topologicalKrullDimAt Y (f x) +
topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x)
AlgebraicGeometry.topologicalKrullDimAt_eq_add_topologicalKrullDimAt_fiber_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/DimensionFormula.lean, line 99.
Stacks Project, Tag 0AFF. For a smooth morphism of locally Noetherian schemes the dimension of the source at a point is the dimension of the target at its image plus the dimension of the fibre at that point.
public theorem topologicalKrullDimAt_eq_add_topologicalKrullDimAt_fiber_of_smooth
{X Y : Scheme.{u}} [IsLocallyNoetherian X] [IsLocallyNoetherian Y] (f : X ⟶ Y) [Smooth f]
(x : X) :
topologicalKrullDimAt X x =
topologicalKrullDimAt Y (f x) +
topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x)
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.