37.53 Stein factorization to 37.67 Pushouts in the category…

Section37.53 Stein factorization #

Section 37.53 of the Stacks Project, Tag 03GX. 9 tags here are carried by 36 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03GY, a lemma

Tag 03GY in the Stacks Project.

Stacks.SteinFactorization.toNormalization_fromNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Basic.lean, line 63. The attribute's comment: “relative_normalization”.

Stacks Project, Tag 03GY. A quasi-compact, quasi-separated morphism f : X ⟶ S factors as f = f' ≫ π, where S' is the normalization of S in X, where f' is the canonical map to S' and where π is the structure morphism of S'.

A proper morphism is quasi-compact and quasi-separated, so this also supplies the factorization of [Stacks Project, Tag 03H2].

public theorem toNormalization_fromNormalization :
    f.toNormalization ≫ f.fromNormalization = f

Stacks.SteinFactorization.quasiCompact_toNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Basic.lean, line 69. The attribute's comment: “first_quasi_compact”.

Stacks Project, Tag 03GY. The first map of the factorization is quasi-compact.

public theorem quasiCompact_toNormalization : QuasiCompact f.toNormalization

Stacks.SteinFactorization.quasiSeparated_toNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Basic.lean, line 74. The attribute's comment: “first_quasi_separated”.

Stacks Project, Tag 03GY. The first map of the factorization is quasi-separated.

public theorem quasiSeparated_toNormalization : QuasiSeparated f.toNormalization

Stacks.SteinFactorization.isIntegralHom_fromNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Basic.lean, line 83. The attribute's comment: “integral_second_map”.

Stacks Project, Tag 03GY. The second map of the factorization, the structure morphism of the normalization of S in X, is integral.

A proper morphism is quasi-compact and quasi-separated, so this also supplies the integrality of the second factor in [Stacks Project, Tag 03H2].

public theorem isIntegralHom_fromNormalization : IsIntegralHom f.fromNormalization

Stacks.SteinFactorization.universallyClosed_toNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Basic.lean, line 95. The attribute's comment: “first_universally_closed”.

Stacks Project, Tag 03GY. The first map of the factorization of a universally closed, quasi-separated morphism is universally closed.

public theorem universallyClosed_toNormalization : UniversallyClosed f.toNormalization

Stacks.SteinFactorization.surjective_toNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Basic.lean, line 101. The attribute's comment: “first_surjective”.

Stacks Project, Tag 03GY. The first map of the factorization of a universally closed, quasi-separated morphism is surjective: it is universally closed and dominant.

public theorem surjective_toNormalization : Surjective f.toNormalization

Stacks.SteinFactorization.isIso_normalizationPullback, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/FlatBaseChange.lean, line 228. The attribute's comment: “flat_base_change”. References: EGA III (4.3.4), “more general”.

Stacks Project, Tag 03GY (flat_base_change). Formation of the factorization f = π ∘ f' of a universally closed, quasi-separated morphism commutes with flat base change: the comparison morphism from the normalization of the base change f_T : X ×_S T ⟶ T to the base change T ×_S S' of the normalization of S in X is an isomorphism.

Together with AlgebraicGeometry.Scheme.Hom.normalizationPullback_snd and AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationPullback_fst, which say that the comparison morphism matches the two factors, this is the assertion that the whole factorization is obtained from that of f by base change.

public instance isIso_normalizationPullback : IsIso (f.normalizationPullback g)

Stacks.SteinFactorization.normalizationPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/FlatBaseChange.lean, line 244. The attribute's comment: “flat_base_change”. References: EGA III (4.3.4), “more general”.

Stacks Project, Tag 03GY (flat_base_change). The identification, over T, of the intermediate scheme of the factorization of the base change f_T : X ×_S T ⟶ T with the base change T ×_S S' of the intermediate scheme of the factorization of f.

public noncomputable def normalizationPullbackIso :
    Over.mk (pullback.snd f g).fromNormalization ≅
      Over.mk (pullback.snd f.fromNormalization g)

Stacks.SteinFactorization.toNormalization_normalizationPullbackIso_hom_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/FlatBaseChange.lean, line 252. The attribute's comment: “flat_base_change”.

Stacks Project, Tag 03GY (flat_base_change). Under that identification the first factor of the factorization of f_T becomes the base change of the first factor of f.

public theorem toNormalization_normalizationPullbackIso_hom_left :
    (pullback.snd f g).toNormalization ≫ (normalizationPullbackIso f g).hom.left ≫
        pullback.fst f.fromNormalization g = pullback.fst f g ≫ f.toNormalization

Stacks.SteinFactorization.overIsoPushforwardSpectrum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/RelativeSpectrum.lean, line 67. The attribute's comment: “relative_spectrum”. References: EGA III (7.8.10), “partial”; SGA 1 X (1.2), “Y′ ≅ Spec f_*O_X over Y”; SGA 6 XII (2.5), “partial”.

Stacks Project, Tag 03GY (relative_spectrum). Clause (4) of the factorization of a universally closed, quasi-separated morphism f : X ⟶ S: the intermediate scheme S' of the factorization is, as a scheme over S, the relative spectrum Spec_S(f_* 𝒪_X) of the pushed-forward structure sheaf. Being an isomorphism over S is the statement that the second factor π : S' ⟶ S becomes the structure morphism of the relative spectrum.

public noncomputable def overIsoPushforwardSpectrum :
    Over.mk f.fromNormalization ≅ Over.mk (pushforwardSpectrum f).toBase

Stacks.SteinFactorization.toNormalization_overIsoPushforwardSpectrum_hom_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/RelativeSpectrum.lean, line 79. The attribute's comment: “relative_spectrum”. References: EGA III (7.8.10), “partial”; SGA 1 X (1.2), “Under Y′ ≅ Spec f_*O_X”; SGA 6 XII (2.5), “partial”.

Stacks Project, Tag 03GY (relative_spectrum). Under the identification of the intermediate scheme of the factorization with Spec_S(f_* 𝒪_X), the first factor f' : X ⟶ S' becomes the canonical morphism X ⟶ Spec_S(f_* 𝒪_X) of [Stacks, Tag 01LY].

public theorem toNormalization_overIsoPushforwardSpectrum_hom_left :
    f.toNormalization ≫ (overIsoPushforwardSpectrum f).hom.left = canonicalMorphism f

Stacks.SteinFactorization.isIso_c_toNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/StructureSheaf.lean, line 158. The attribute's comment: “pushforward_structure_sheaf”.

Stacks Project, Tag 03GY. Clause (3) of the factorization of a universally closed, quasi-separated morphism f : X ⟶ S: the canonical map from the structure sheaf of the normalization S' of S in X to the pushforward of the structure sheaf of X along the first map f' : X ⟶ S' is an isomorphism, that is, f'_*𝒪_X = 𝒪_{S'}.

public theorem isIso_c_toNormalization : IsIso f.toNormalization.c

Tag 0E0M, a lemma

Tag 0E0M in the Stacks Project.

Stacks.SteinFactorization.finite_preimage_singleton_fromNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/FiniteFibres.lean, line 183. The attribute's comment: “finite_fibre”.

For a universally closed, quasi-separated morphism f that is locally of finite type, the fibres of the second map π of the factorization X ⟶ f.normalization ⟶ S are finite.

public theorem finite_preimage_singleton_fromNormalization (s : S) :
    (f.fromNormalization ⁻¹' {s}).Finite

Stacks.SteinFactorization.finite_residueFieldMap_fromNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/FiniteFibres.lean, line 240. The attribute's comment: “finite_residue_extensions”.

For a universally closed, quasi-separated morphism f that is locally of finite type, the residue field of f.normalization at a point is a finite extension of the residue field of S at its image under the second map π of the factorization: the ring map κ(π s') ⟶ κ(s') makes κ(s') a finite κ(π s')-module.

public theorem finite_residueFieldMap_fromNormalization (s' : f.normalization) :
    (f.fromNormalization.residueFieldMap s').hom.Finite

Tag 03GZ, a lemma

Tag 03GZ in the Stacks Project.

AlgebraicGeometry.geometricallyConnected_fiber_iff_forall_etaleNeighborhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/GeometricallyConnectedFibre.lean, line 85.

Stacks Project, Tag 03GZ. The fibre of a morphism at a point is geometrically connected if and only if the fibre at the distinguished point after pullback to every étale neighborhood is connected.

theorem geometricallyConnected_fiber_iff_forall_etaleNeighborhood
    {X S : Scheme.{u}} (f : X ⟶ S) (s : S) :
    GeometricallyConnected (f.fiberToSpecResidueField s) ↔
      ∀ U : EtaleNeighborhood S s,
        ConnectedSpace ((pullback.snd f U.toBase).fiber U.point)

Tag 03H0, a theorem

Tag 03H0 in the Stacks Project.

Stacks.SteinFactorization.isFinite_fromNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Noetherian.lean, line 213. The attribute's comment: “clause (2): the second factor of the Stein factorization of a proper morphism over a locally Noetherian base is finite. Proved from [Stacks, Tag 02O5] (AlgebraicGeometry.ProperCoherenceWitness.isCoherent_pushforward), with no carried hypothesis”. References: EGA III (7.8.10), “partial”; SGA 1 X (1.2), “Y′ is finite over Y”.

Stacks Project, Tag 03H0, clause (2). For a proper morphism f : X ⟶ S onto a locally Noetherian scheme, the second factor π : S' ⟶ S of the Stein factorization — the structure morphism of the normalization of S in X — is finite. No hypothesis.

This is the one clause of Tag 03H0 that is not already a clause of the general Tag 03H2, where π is only asserted to be integral, and it is where local Noetherianness of S is used. The proof is the source's: f_* 𝒪_X is coherent by [Stacks, Tag 02O5], so Γ(S, U) ⟶ Γ(X, f ⁻¹ᵁ U) is finite for U ⊆ S affine open (Stacks.SteinFactorization.finite_app_of_isProper); that map is Γ(S, U) ⟶ Γ(S', π ⁻¹ᵁ U) ⟶ Γ(X, f ⁻¹ᵁ U) and the second map is an isomorphism by [Stacks, Tag 03GY] (Stacks.SteinFactorization.isIso_app_toNormalization), so the first is finite; and π is affine, being integral.

public theorem isFinite_fromNormalization : IsFinite f.fromNormalization

Stacks.SteinFactorization.geometricallyConnected_toNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Noetherian.lean, line 349. The attribute's comment: “clause (1), the geometric connectedness conjunct: the first factor of the Stein factorization of a proper morphism onto a locally Noetherian base has geometrically connected fibres. The properness conjunct of the same clause is isProper_toNormalization_of_isLocallyNoetherian”. References: EGA III (4.3.4), “special case”.

Stacks Project, Tag 03H0, clause (1), the geometric connectedness conjunct. For f proper onto a locally Noetherian scheme S, the first factor f' : X ⟶ S' of the Stein factorization — S' the normalization of S in X and f' = f.toNormalization — has geometrically connected fibres.

Unconditional, at the hypotheses of the tag. It is the reading of Stacks.SteinFactorization.geometricallyConnected_toNormalization_of_isProper, clause (1) of the general [Stacks, Tag 03H2], at the stronger hypotheses of this tag; the local Noetherianness of S is not used.

The properness conjunct of the same clause is Stacks.SteinFactorization.isProper_toNormalization_of_isLocallyNoetherian below.

public theorem geometricallyConnected_toNormalization (f : X ⟶ S) [IsLocallyNoetherian S]
    [IsProper f] : GeometricallyConnected f.toNormalization

Stacks.SteinFactorization.toNormalization_fromNormalization_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Noetherian.lean, line 373. The attribute's comment: “the factorization itself together with clause (5): f factors as X --f'--> S' --π--> S with S' the normalization of S in X (Stacks 035H), f' = f.toNormalization and π = f.fromNormalization. No carried hypothesis”.

Stacks Project, Tag 03H0: the factorization, together with clause (5). A proper morphism f : X ⟶ S onto a locally Noetherian scheme factors as X --f'--> S' --π--> S through the normalization of S in X ([Stacks, Tag 035H], AlgebraicGeometry.Scheme.Hom.normalization), with f' = f.toNormalization and π = f.fromNormalization. That the intermediate scheme of the factorization is the normalization of S in X is clause (5), and since the intermediate scheme produced here is f.normalization the whole content of that clause is the displayed equation.

Local Noetherianness is not needed: this is the general factorization of [Stacks, Tag 03H2], which holds for any proper morphism, specialized to the hypotheses of Tag 03H0.

public theorem toNormalization_fromNormalization_of_isLocallyNoetherian :
    f.toNormalization ≫ f.fromNormalization = f

Stacks.SteinFactorization.isProper_toNormalization_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Noetherian.lean, line 385. The attribute's comment: “clause (1), the properness half: the first factor of the Stein factorization is proper. No carried hypothesis”.

Stacks Project, Tag 03H0, clause (1), properness half. The first factor f' : X ⟶ S' of the Stein factorization of a proper morphism onto a locally Noetherian scheme is proper. Local Noetherianness is not needed: f' is universally closed because f is, and separated and locally of finite type by cancellation along π, which is the general [Stacks, Tag 03H2] specialized to the hypotheses of Tag 03H0.

public theorem isProper_toNormalization_of_isLocallyNoetherian : IsProper f.toNormalization

Stacks.SteinFactorization.isIso_c_toNormalization_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Noetherian.lean, line 396. The attribute's comment: “clause (3): f'_ 𝒪_X = 𝒪_{S'}, i.e. the canonical map 𝒪_{S'} ⟶ f'_ 𝒪_X is an isomorphism. No carried hypothesis”.

Stacks Project, Tag 03H0, clause (3). f'_* 𝒪_X = 𝒪_{S'} for the first factor of the Stein factorization of a proper morphism onto a locally Noetherian scheme: the canonical map 𝒪_{S'} ⟶ f'_* 𝒪_X is an isomorphism. Local Noetherianness is not needed; this is [Stacks, Tag 03H2] clause (3), which holds for any proper morphism, specialized to the hypotheses of Tag 03H0.

public theorem isIso_c_toNormalization_of_isLocallyNoetherian : IsIso f.toNormalization.c

Stacks.SteinFactorization.overIsoPushforwardSpectrum_of_isLocallyNoetherian, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Noetherian.lean, line 408. The attribute's comment: “clause (4): S' = Spec_S(f_ 𝒪_X), as an isomorphism in Over S, so that π is carried to the structure morphism of the relative spectrum. No carried hypothesis”. References: EGA III (7.8.10), “partial”; SGA 1 X (1.2), “Y′ ≅ Spec f_O_X over Y”; SGA 6 XII (2.5), “partial”.

Stacks Project, Tag 03H0, clause (4). The intermediate scheme S' of the Stein factorization of a proper morphism onto a locally Noetherian scheme is the relative spectrum Spec_S(f_* 𝒪_X), as a scheme over S. Being an isomorphism in CategoryTheory.Over S is what makes this an identification of factorizations: it says that π is carried to the structure morphism of the relative spectrum. Local Noetherianness is not needed; this is [Stacks, Tag 03H2] clause (4) specialized to the hypotheses of Tag 03H0.

public noncomputable def overIsoPushforwardSpectrum_of_isLocallyNoetherian :
    Over.mk f.fromNormalization ≅ Over.mk (pushforwardSpectrum f).toBase

Stacks.SteinFactorization.toNormalization_overIsoPushforwardSpectrum_hom_left_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Noetherian.lean, line 420. The attribute's comment: “clause (4), continued: the identification of clause (4) carries f' to the canonical morphism X ⟶ Spec_S(f_ 𝒪_X) of Stacks 01LY. No carried hypothesis”. References: SGA 1 X (1.2), “Under Y′ ≅ Spec f_O_X”.

Stacks Project, Tag 03H0, clause (4), continued. The identification of clause (4) carries the first factor f' to the canonical morphism X ⟶ Spec_S(f_* 𝒪_X) of [Stacks, Tag 01LY]; this is what makes clause (4) an identification of the factorization f = f' ≫ π with the factorization of f through its relative spectrum.

public theorem toNormalization_overIsoPushforwardSpectrum_hom_left_of_isLocallyNoetherian :
    f.toNormalization ≫ (overIsoPushforwardSpectrum_of_isLocallyNoetherian f).hom.left =
      canonicalMorphism f

Stacks.SteinFactorization.exists_isSteinFactorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Noetherian.lean, line 482. References: EGA II (8.11.8), “(ii), special case”; EGA III (4.3.1); EGA III (7.8.10), “more general”; SGA 1 IX (6.6), “partial”; SGA 1 X (1.2).

Stacks Project, Tag 03H0 (Stein factorization, Noetherian case). Let S be a locally Noetherian scheme and let f : X ⟶ S be proper. Then f factors as X --f'--> S' --π--> S with all five properties of the tag: f' proper with geometrically connected fibres, π finite, f'_* 𝒪_X = 𝒪_{S'}, S' = Spec_S(f_* 𝒪_X), and S' the normalization of S in X.

The witnesses are the ones the source names: S' is the normalization of S in X, f' is f.toNormalization and π is f.fromNormalization.

Unconditional. Each of the five clauses is a theorem of its own above; the last of them to be proved was the connectedness conjunct of clause (1), Stacks.SteinFactorization.geometricallyConnected_toNormalization, which rests on [Stacks, Tag 0G7X] at a locally Noetherian base and through it on the theorem on formal functions.

public theorem exists_isSteinFactorization
    (f : X ⟶ S) [IsLocallyNoetherian S] [IsProper f] :
    ∃ (S' : Scheme.{u}) (f' : X ⟶ S') (π : S' ⟶ S), Nonempty (IsSteinFactorization f f' π)

Tag 03H2, a theorem

Tag 03H2 in the Stacks Project.

Stacks.SteinFactorization.toNormalization_fromNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Basic.lean, line 63. The attribute's comment: “normalization”.

Stacks Project, Tag 03GY. A quasi-compact, quasi-separated morphism f : X ⟶ S factors as f = f' ≫ π, where S' is the normalization of S in X, where f' is the canonical map to S' and where π is the structure morphism of S'.

A proper morphism is quasi-compact and quasi-separated, so this also supplies the factorization of [Stacks Project, Tag 03H2].

public theorem toNormalization_fromNormalization :
    f.toNormalization ≫ f.fromNormalization = f

Stacks.SteinFactorization.isIntegralHom_fromNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Basic.lean, line 83. The attribute's comment: “integral_second_map”.

Stacks Project, Tag 03GY. The second map of the factorization, the structure morphism of the normalization of S in X, is integral.

A proper morphism is quasi-compact and quasi-separated, so this also supplies the integrality of the second factor in [Stacks Project, Tag 03H2].

public theorem isIntegralHom_fromNormalization : IsIntegralHom f.fromNormalization

Stacks.SteinFactorization.geometricallyConnected_toNormalization_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/ConnectedFibres.lean, line 473. The attribute's comment: “clause (1), the geometric connectedness conjunct: the first factor of the Stein factorization of a proper morphism has geometrically connected fibres, over an arbitrary base. The properness conjunct of the same clause is isProper_toNormalization”. References: EGA III (4.3.4), “partial”.

Stacks Project, Tag 03H2, clause (1), the geometric connectedness conjunct. For f proper onto an arbitrary scheme S, the first factor f' : X ⟶ S' of the Stein factorization — S' the normalization of S in X and f' = f.toNormalization — has geometrically connected fibres.

Unconditional, at the hypotheses of the tag: nothing is assumed of S. The two inputs are the reduction above, which is the source's — [Stacks, Tag 03GZ] together with degree-zero flat base change and f'_* 𝒪_X = 𝒪_{S'} — and [Stacks, Tag 0G7X] for the base changes of f' to étale neighbourhoods of S', which is Stacks.AlgebraicGeometry.Fibres.extendsOverNeighbourhood_of_isProper.

The same statement covers the connectedness conjunct of clause (1) of [Stacks, Tag 03H0], whose hypotheses are strictly stronger; Stacks.SteinFactorization.geometricallyConnected_toNormalization in StacksFrontier.AlgebraicGeometry.MoreMorphisms.SteinFactorization.Noetherian is that reading of it. The properness conjunct of clause (1) is Stacks.SteinFactorization.isProper_toNormalization.

public theorem geometricallyConnected_toNormalization_of_isProper :
    GeometricallyConnected f.toNormalization

Stacks.SteinFactorization.isProper_toNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/Proper.lean, line 51. The attribute's comment: “proper_first_map”.

Stacks Project, Tag 03H2. The first map of the factorization of a proper morphism is proper. It is universally closed because f is, separated and locally of finite type by cancellation along the second map.

public theorem isProper_toNormalization : IsProper f.toNormalization

Stacks.SteinFactorization.overIsoPushforwardSpectrum_of_isProper, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/RelativeSpectrum.lean, line 96. The attribute's comment: “relative_spectrum”. References: EGA III (7.8.10), “partial”; SGA 1 X (1.2), “Y′ ≅ Spec f_*O_X over Y”; SGA 6 XII (2.5), “partial”.

Stacks Project, Tag 03H2 (relative_spectrum). Clause (4) of the factorization of a proper morphism f : X ⟶ S: the intermediate scheme S' of the factorization is, as a scheme over S, the relative spectrum Spec_S(f_* 𝒪_X) of the pushed-forward structure sheaf.

public noncomputable def overIsoPushforwardSpectrum_of_isProper :
    Over.mk f.fromNormalization ≅ Over.mk (pushforwardSpectrum f).toBase

Stacks.SteinFactorization.toNormalization_overIsoPushforwardSpectrum_hom_left_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/RelativeSpectrum.lean, line 108. The attribute's comment: “relative_spectrum”. References: EGA III (7.8.10), “partial”; SGA 1 X (1.2), “Under Y′ ≅ Spec f_*O_X”; SGA 6 XII (2.5), “partial”.

Stacks Project, Tag 03H2 (relative_spectrum). Under the identification of the intermediate scheme of the factorization of a proper morphism with Spec_S(f_* 𝒪_X), the first factor f' : X ⟶ S' becomes the canonical morphism X ⟶ Spec_S(f_* 𝒪_X) of [Stacks, Tag 01LY].

public theorem toNormalization_overIsoPushforwardSpectrum_hom_left_of_isProper :
    f.toNormalization ≫ (overIsoPushforwardSpectrum_of_isProper f).hom.left =
      canonicalMorphism f

Stacks.SteinFactorization.isIso_c_toNormalization_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/StructureSheaf.lean, line 173. The attribute's comment: “structure_sheaf_pushforward”.

Stacks Project, Tag 03H2. Clause (3) of the factorization of a proper morphism f : X ⟶ S: the pushforward of the structure sheaf of X along the first map f' : X ⟶ f.normalization is the structure sheaf of f.normalization.

public theorem isIso_c_toNormalization_of_isProper {X S : Scheme.{u}} (f : X ⟶ S) [IsProper f] :
    IsIso f.toNormalization.c

Tag 0AY8, a lemma

Tag 0AY8 in the Stacks Project.

Stacks.SteinFactorization.isIso_c_of_isNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/NormalBase.lean, line 297. The attribute's comment: “pushforward of the structure sheaf”.

Stacks Project, Tag 0AY8, first conclusion. Let f : X ⟶ S be a proper morphism from a reduced scheme onto a normal integral scheme with generic point ξ. If every generic point of an irreducible component of X maps to ξ and H⁰(X_ξ, 𝒪) = κ(ξ), then f_*𝒪_X = 𝒪_S.

The second factor of the Stein factorization is an isomorphism, and the first already satisfies f'_*𝒪_X = 𝒪_{S'} by clause (3) of [Stacks, Tag 03H2].

public theorem isIso_c_of_isNormal (f : X ⟶ S) [IsProper f] [IsIntegral S]
    [AlgebraicGeometry.IsNormal S] [IsReduced X]
    (hgen : ∀ x : X, x ∈ genericPoints X → f x = genericPoint S)
    (hΓ : IsIso ((Scheme.ΓSpecIso (S.residueField (genericPoint S))).inv ≫
      (f.fiberToSpecResidueField (genericPoint S)).appTop)) :
    IsIso f.c

Stacks.SteinFactorization.geometricallyConnected_of_isNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/NormalBase.lean, line 373. The attribute's comment: “the second conclusion, that f has geometrically connected fibres. The first conclusion, f_*𝒪_X = 𝒪_S, is isIso_c_of_isNormal”. References: EGA III (4.3.8), “special case”.

Stacks Project, Tag 0AY8, the second conclusion. Under the hypotheses of Tag 0AY8 — f proper, S integral and normal, X reduced, every generic point of X over the generic point ξ of S, and H⁰(X_ξ, 𝒪) = κ(ξ) — the morphism f has geometrically connected fibres.

The proof follows the source: the second factor π : S' ⟶ S of the Stein factorization is an isomorphism (Stacks.SteinFactorization.isIso_fromNormalization_of_isNormal), so the fibres of f are those of the first factor, and their geometric connectedness is clause (1) of [Stacks, Tag 03H2], Stacks.SteinFactorization.geometricallyConnected_toNormalization_of_isProper.

The first conclusion, f_*𝒪_X = 𝒪_S, is Stacks.SteinFactorization.isIso_c_of_isNormal.

public theorem geometricallyConnected_of_isNormal
    (f : X ⟶ S) [IsProper f] [IsIntegral S] [AlgebraicGeometry.IsNormal S] [IsReduced X]
    (hgen : ∀ x : X, x ∈ genericPoints X → f x = genericPoint S)
    (hΓ : IsIso ((Scheme.ΓSpecIso (S.residueField (genericPoint S))).inv ≫
      (f.fiberToSpecResidueField (genericPoint S)).appTop)) :
    GeometricallyConnected f

Tag 0BUI, a lemma

Tag 0BUI in the Stacks Project.

AlgebraicGeometry.lowerSemicontinuous_numGeometricConnectedComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FibreConnectedComponents/LowerSemicontinuity.lean, line 492. References: EGA IV (15.5.4), “Flat case”; EGA IV (15.5.9).

[Stacks, Tag 0BUI]. For a flat proper morphism of finite presentation, the number of geometric connected components of the fibres is a lower semicontinuous function on the base.

The count is the ℕ∞-valued function of Tag 055F. The proof is the source's: the Stein factorization f = f.fromNormalization ∘ f.toNormalization has a first factor with geometrically connected fibres (Tag 03H2), so it does not change the count, and a second factor that is integral and, as f is flat of finite presentation and f.toNormalization is surjective, universally open.

theorem lowerSemicontinuous_numGeometricConnectedComponents {X S : Scheme.{u}} (f : X ⟶ S)
    [IsProper f] [Flat f] [LocallyOfFinitePresentation f] :
    LowerSemicontinuous (numGeometricConnectedComponents f)

Tag 0E0N, a lemma

Tag 0E0N in the Stacks Project.

AlgebraicGeometry.isLocallyConstant_numGeometricConnectedComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FibreConnectedComponents/LocalConstancy.lean, line 158. References: EGA IV (15.5.7), “Flat”; EGA IV (15.5.9), “(ii), special case”.

The number of geometric connected components of the fibres is locally constant, for f : X ⟶ S proper, flat, of finite presentation, with geometrically reduced fibres.

It is lower semicontinuous by [Stacks, Tag 0BUI], and it is the degree-zero derived-fibre Betti function of the perfect object Rf_*𝒪_X (numGeometricConnectedComponents_eq_derivedFiberBetti), which is upper semicontinuous by part (2) of [Stacks, Tag 0BDI] (DerivedFibreBetti.upperSemicontinuous_derivedFiberBetti). The hypothesis hred that the geometric fibres are reduced asks this of the base change of f to the spectrum of every algebraically closed field; it gives Mathlib's GeometricallyReduced f, reducedness after base change to every field, by geometricallyReduced_iff_forall_isAlgClosed.

theorem isLocallyConstant_numGeometricConnectedComponents
    {X S : Scheme.{u}} (f : X ⟶ S) [IsProper f] [Flat f] [LocallyOfFinitePresentation f]
    (hred : ∀ (k : Type u) [Field k] [IsAlgClosed k] (s : Spec (.of k) ⟶ S),
      IsReduced (pullback f s)) :
    IsLocallyConstant (numGeometricConnectedComponents f)

Tag 0CT9, a lemma

Tag 0CT9 in the Stacks Project.

AlgebraicGeometry.exists_isClopen_isProper_of_henselianPair_of_compactification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ProperPartOverHenselianPair.lean, line 381. The attribute's comment: “the whole statement, with two inputs the source quotes carried as named hypotheses: hcpt, Nagata compactification (Stacks 0F41), and hconn, the connectedness conjunct of clause (1) of Stacks 03H2 (through Stacks 0G7X, 02OC and 02OB); neither is proved in this repository, and neither is any part of this tag's own conclusion”.

[Stacks, Tag 0CT9] with [Stacks, Tag 0F41] carried as hcpt and clause (1) of [Stacks, Tag 03H2] carried as hconn.

Let (A, I) be a henselian pair and let f : X ⟶ Spec A be separated and of finite type. An open and closed subscheme i : Y ⟶ X ×_{Spec A} Spec (A ⧸ I) of the closed fibre which is proper over Spec (A ⧸ I) is the closed fibre of an open and closed subscheme w : W ⟶ X which is proper over Spec A.

Choosing a compactification X ⟶ P ⟶ Spec A of f, the image of Y in the closed fibre of P is open and closed and lifts to an open and closed subset V of P. Since the points of V over the closed fibre lie in X, all of V does, and V cuts out the required subscheme of X.

The tag's hypotheses and its full conclusion are exactly those below. The two extra arguments are the conclusions of other tags, quoted by the source and unavailable here: hcpt is Nagata's compactification theorem, Tag 0F41, and hconn is the connectedness conjunct of clause (1) of Tag 03H2, which rests on Tag 0G7X and hence on Tags 02OC and 02OB. The quantifier on hconn is forced by hcpt being an existential: the connectedness input is applied to the compactification P, which is produced rather than given. The source reaches the same reduction through Chow's lemma (Tag 0202) and Tag 01RG instead of through Tag 0F41; that route is equally unavailable, Tag 0202 being conditional here on Scheme.FiniteTypeApproximation.IsOneAffineOpenStep.

theorem exists_isClopen_isProper_of_henselianPair_of_compactification (A : Type u) [CommRing A]
    (I : Ideal A) (hI : HenselianPair A I) {X : Scheme.{u}} (f : X ⟶ Spec (.of A))
    [LocallyOfFiniteType f] [QuasiCompact f] [IsSeparated f]
    (hcpt : ∃ (P : Scheme.{u}) (j : X ⟶ P) (π : P ⟶ Spec (.of A)),
      IsOpenImmersion j ∧ IsProper π ∧ j ≫ π = f)
    (hconn : ∀ {P : Scheme.{u}} (π : P ⟶ Spec (.of A)) [IsProper π],
      GeometricallyConnected π.toNormalization)
    {Y : Scheme.{u}}
    (i : Y ⟶ pullback f (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))))
    [IsOpenImmersion i] [IsClosedImmersion i]
    [IsProper (i ≫ pullback.snd f (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))))] :
    ∃ (W : Scheme.{u}) (w : W ⟶ X) (_ : IsOpenImmersion w) (_ : IsClosedImmersion w)
      (_ : IsProper (w ≫ f)),
      let q := Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))
      let w₀ : pullback (w ≫ f) q ⟶ pullback f q :=
        pullback.lift (pullback.fst (w ≫ f) q ≫ w) (pullback.snd (w ≫ f) q)
          (by rw [Category.assoc]; exact pullback.condition)
      ∃ e : Y ≅ pullback (w ≫ f) q, e.hom ≫ w₀ = i

AlgebraicGeometry.exists_isClopen_isProper_of_henselianPair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ProperPartOverHenselianPair/Chow.lean, line 257. The attribute's comment: “the whole statement”.

Let (A, I) be a henselian pair and let f : X ⟶ Spec A be separated and of finite type. An open and closed subscheme i : Y ⟶ X ×_{Spec A} Spec (A ⧸ I) of the closed fibre which is proper over Spec (A ⧸ I) is the closed fibre of an open and closed subscheme w : W ⟶ X which is proper over Spec A: there is an isomorphism Y ≅ W ×_{Spec A} Spec (A ⧸ I) over the closed fibre.

theorem exists_isClopen_isProper_of_henselianPair (A : Type u) [CommRing A]
    (I : Ideal A) (hI : HenselianPair A I) {X : Scheme.{u}} (f : X ⟶ Spec (.of A))
    [LocallyOfFiniteType f] [QuasiCompact f] [IsSeparated f] {Y : Scheme.{u}}
    (i : Y ⟶ pullback f (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))))
    [IsOpenImmersion i] [IsClosedImmersion i]
    [IsProper (i ≫ pullback.snd f (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))))] :
    ∃ (W : Scheme.{u}) (w : W ⟶ X) (_ : IsOpenImmersion w) (_ : IsClosedImmersion w)
      (_ : IsProper (w ≫ f)),
      let q := Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))
      let w₀ : pullback (w ≫ f) q ⟶ pullback f q :=
        pullback.lift (pullback.fst (w ≫ f) q ≫ w) (pullback.snd (w ≫ f) q)
          (by rw [Category.assoc]; exact pullback.condition)
      ∃ e : Y ≅ pullback (w ≫ f) q, e.hom ≫ w₀ = i

Sources

LeanStacks.SteinFactorization.toNormalization_fromNormalization · Stacks.SteinFactorization.quasiCompact_toNormalization · Stacks.SteinFactorization.quasiSeparated_toNormalization · Stacks.SteinFactorization.isIntegralHom_fromNormalization · Stacks.SteinFactorization.universallyClosed_toNormalization · Stacks.SteinFactorization.surjective_toNormalization · Stacks.SteinFactorization.isIso_normalizationPullback · Stacks.SteinFactorization.normalizationPullbackIso

Section37.54 Generic flatness stratification #

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

Tag 0ASY, a lemma

Tag 0ASY in the Stacks Project.

AlgebraicGeometry.exists_flat_stratification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GenericFlatness/FlatStratificationQcqs.lean, line 171. References: EGA IV (6.9.3), “more general”; EGA IV (8.9.5).

Stacks Project, Tag 0ASY.

For a morphism of finite presentation f : X ⟶ S between quasi-compact, quasi-separated schemes and a finitely presented 𝒪_X-module ℱ, the base carries a finite ascending chain of quasi-coherent ideal sheaves of finite type whose first closed subscheme is a thickening of S and whose last closed subscheme is empty, such that the pullback of ℱ to the fibre product of X with each locally closed stratum is flat over that stratum.

The general case is reduced to the Noetherian case AlgebraicGeometry.exists_flat_stratification_of_isNoetherian; see the module docstring.

public theorem exists_flat_stratification {X S : Scheme.{u}} (f : X ⟶ S)
    [CompactSpace X] [QuasiSeparatedSpace X] [CompactSpace S] [QuasiSeparatedSpace S]
    (hf : FinitePresentation f) (F : X.Modules) [F.IsFinitePresentation] :
    ∃ (t : ℕ) (I : Fin (t + 1) → S.IdealSheafData),
      Stacks.Thickenings.IsThickening (I 0).subschemeι ∧
      (∀ i, Scheme.IdealSheafData.IsFiniteType (I i)) ∧
      (∀ i : Fin t, I (Fin.castSucc i) ≤ I (Fin.succ i)) ∧
      I (Fin.last t) = ⊤ ∧
      ∀ i : Fin t,
        let Z := I (Fin.castSucc i)
        let V : S.Opens := (I (Fin.succ i)).support.compl
        let U : Z.subscheme.Opens := Z.subschemeι ⁻¹ᵁ V
        let g : U.toScheme ⟶ S := U.ι ≫ Z.subschemeι
        IsFlatOver (pullback.snd f g).toLRSHom.toShHom
          ((Scheme.Modules.pullback (pullback.fst f g)).obj F)

Tag 0H3Z, a lemma

Tag 0H3Z in the Stacks Project.

AlgebraicGeometry.HasFlatStratification.of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GenericFlatness/MorphismFlatStratificationQcqs.lean, line 62. References: EGA IV (6.9.3), “Case F = O_X”; EGA IV (8.9.5), “Case F = O_X”; SGA 6 XIII (1.13), “special case”.

A morphism of finite presentation between quasi-compact quasi-separated schemes has a flat stratification of its base: a finite descending chain of closed subschemes, each cut out by an ideal sheaf of finite type, beginning with a thickening of the base and ending with the empty scheme, over each of whose locally closed strata the base change of the morphism is flat.

public theorem HasFlatStratification.of_finitePresentation {X S : Scheme.{u}} (f : X ⟶ S)
    [CompactSpace X] [QuasiSeparatedSpace X] [CompactSpace S] [QuasiSeparatedSpace S]
    (hf : FinitePresentation f) : HasFlatStratification f

AlgebraicGeometry.HasFlatStratification.of_finitePresentation_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GenericFlatness/NoetherianFlatStratification.lean, line 283. The attribute's comment: “the case of a Noetherian base. The general quasi-compact quasi-separated case of the tag is AlgebraicGeometry.HasFlatStratification.of_finitePresentation, which reduces to this one by absolute Noetherian approximation”.

The Noetherian case of Stacks 0H3Z, with the hypotheses of the tag: a morphism of finite presentation to a Noetherian base has a flat stratification.

theorem HasFlatStratification.of_finitePresentation_of_isNoetherian {X S : Scheme.{u}}
    [IsNoetherian S] (f : X ⟶ S) (hf : FinitePresentation f) : HasFlatStratification f

Tag 0H89, a lemma

Tag 0H89 in the Stacks Project.

AlgebraicGeometry.exists_isFlat_iff_exists_isFlat_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GenericFlatness/FlatSingleDerivedPullbackConverse.lean, line 425.

Stacks 0H89 (Longke Tang). Let f : X ⟶ S be a surjective morphism of finite presentation and let M be an object of D_QCoh(𝒪_S) such that H^i(M) = 0 for i > 0. Then M is isomorphic to a flat 𝒪_S-module placed in degree 0 if and only if Lf^*M is isomorphic to a flat 𝒪_X-module placed in degree 0.

theorem exists_isFlat_iff_exists_isFlat_derivedPullback [Surjective f]
    (hf : FinitePresentation f)
    (M : DerivedCategory (SheafOfModules.{u} (structureSheafRing S.toRingedSpace)))
    (hQCoh : ∀ i : ℤ, ((DerivedCategory.homologyFunctor
      (SheafOfModules.{u} (structureSheafRing S.toRingedSpace)) i).obj M).IsQuasicoherent)
    (hM : ∀ i : ℤ, 0 < i → IsZero ((DerivedCategory.homologyFunctor
      (SheafOfModules.{u} (structureSheafRing S.toRingedSpace)) i).obj M)) :
    (∃ F : SheafOfModules.{u} (structureSheafRing S.toRingedSpace),
      SheafOfModules.IsFlat.{u, u, u, u} (O := S.toRingedSpace.sheaf) F ∧
        Nonempty (M ≅ (DerivedCategory.singleFunctor
          (SheafOfModules.{u} (structureSheafRing S.toRingedSpace)) 0).obj F)) ↔
      ∃ G : SheafOfModules.{u} (structureSheafRing X.toRingedSpace),
        SheafOfModules.IsFlat.{u, u, u, u} (O := X.toRingedSpace.sheaf) G ∧
          Nonempty ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
              f.toLRSHom.toShHom).obj M ≅
            (DerivedCategory.singleFunctor
              (SheafOfModules.{u} (structureSheafRing X.toRingedSpace)) 0).obj G)

Tag 0H40, a lemma

Tag 0H40 in the Stacks Project.

Module.exists_flat_localizedModule_coker, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/CokernelGenericFlatness.lean, line 561. References: SGA 1 IV (6.7), “flatness clause”.

Stacks Project, Tag 0H40. A map from a finite A-module to a finite B-module, for finite type algebras R → A → B over a Noetherian domain, has flat cokernel over R after a suitable principal localization.

theorem Module.exists_flat_localizedModule_coker
    {R : Type uR} {A : Type uA} {B : Type uB}
    [CommRing R] [IsNoetherianRing R] [IsDomain R]
    [CommRing A] [Algebra R A] [Algebra.FiniteType R A]
    [CommRing B] [Algebra A B] [Algebra.FiniteType A B]
    [Algebra R B] [IsScalarTower R A B]
    {M : Type uM} [AddCommGroup M] [Module A M] [Module.Finite A M]
    [Module R M] [IsScalarTower R A M]
    {N : Type uN} [AddCommGroup N] [Module B N] [Module.Finite B N]
    [Module A N] [IsScalarTower A B N]
    [Module R N] [IsScalarTower R A N]
    (φ : M →ₗ[A] N) :
    ∃ f : R, f ≠ 0 ∧
      Module.Flat (Localization.Away f)
        (LocalizedModule.Away f (N ⧸ LinearMap.range (φ.restrictScalars R)))

Tag 0H41, a lemma

Tag 0H41 in the Stacks Project.

AlgebraicGeometry.hasImageBaseChangeStratification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GenericFlatness/ImageStratification.lean, line 392.

Stacks Project, Tag 0H41. Let S be a quasi-compact and quasi-separated scheme and f : X ⟶ Y a morphism of schemes over S with both X and Y of finite presentation over S. Then there are a t ≥ 0 and closed subschemes S ⊇ S₀ ⊇ S₁ ⊇ ⋯ ⊇ S_t = ∅ such that each S_i → S is defined by a finite type ideal sheaf, S₀ ⊆ S is a thickening, and formation of the scheme-theoretic image of the base change of f to each stratum S_i ∖ S_{i+1} commutes with arbitrary base change.

theorem hasImageBaseChangeStratification {S : Scheme.{u}}
    [CompactSpace S] [QuasiSeparatedSpace S] (X Y : Over S) (f : X ⟶ Y)
    (hX : FinitePresentation X.hom) (hY : FinitePresentation Y.hom) :
    HasImageBaseChangeStratification f

Sources

LeanAlgebraicGeometry.exists_flat_stratification · AlgebraicGeometry.HasFlatStratification.of_finitePresentation · AlgebraicGeometry.HasFlatStratification.of_finitePresentation_of_isNoetherian · AlgebraicGeometry.exists_isFlat_iff_exists_isFlat_derivedPullback · Module.exists_flat_localizedModule_coker · AlgebraicGeometry.hasImageBaseChangeStratification

Section37.55 Stratifying a morphism #

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

Tag 0H43, a lemma

Tag 0H43 in the Stacks Project.

AlgebraicGeometry.exists_smooth_stratification_at_generic_point, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GenericFlatness/SmoothStratification.lean, line 1279.

Stacks Project, Tag 0H43. Smooth stratification near the generic point of an irreducible component of a reduced base.

theorem exists_smooth_stratification_at_generic_point
    {X S : Scheme.{u}} (f : X ⟶ S) (hf : FinitePresentation f)
    [IsReduced S] (η : S)
    (hη : ∃ C ∈ irreducibleComponents S, IsGenericPoint η C) :
    ∃ (U : S.Opens) (_ : η ∈ U) (V : Scheme.{u}) (g : V ⟶ U.toScheme),
      Function.Surjective g ∧ UniversallyInjective g ∧
        Stacks.Morphisms.IsFiniteLocallyFree g ∧
        ∃ (t : ℕ) (Z : Fin (t + 1) → Scheme.{u})
            (j : (i : Fin (t + 1)) → Z i ⟶ pullback f (g ≫ U.ι))
            (k : (i : Fin t) → Z i.succ ⟶ Z i.castSucc)
            (W : (i : Fin t) → (Z i.castSucc).Opens),
          (∀ i, IsClosedImmersion (j i)) ∧
          (∀ i, (Stacks.ClosedImmersion.idealSheaf (j i).toLRSHom.toShHom).IsFiniteType) ∧
          Stacks.Thickenings.IsThickening (j 0) ∧
          IsEmpty (Z (Fin.last t)) ∧
          (∀ i : Fin t, IsClosedImmersion (k i)) ∧
          (∀ i : Fin t, k i ≫ j i.castSucc = j i.succ) ∧
          (∀ (i : Fin t) (x : Z i.castSucc),
            x ∈ W i ↔ j i.castSucc x ∉ Set.range (j i.succ)) ∧
          (∀ i : Fin t, Smooth ((W i).ι ≫ j i.castSucc ≫
            pullback.snd f (g ≫ U.ι)))

Tag 0H44, a lemma

Tag 0H44 in the Stacks Project.

AlgebraicGeometry.hasSmoothStratificationAfterFiniteLocallyFreeCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GenericFlatness/SmoothStratificationQcqs.lean, line 359.

Stacks Project, Tag 0H44. Let f : X ⟶ S be a morphism of finite presentation between quasi-compact and quasi-separated schemes. Then there are a t ≥ 0 and closed subschemes S ⊇ S₀ ⊇ S₁ ⊇ ⋯ ⊇ S_t = ∅ such that each S_i → S is defined by a finite type ideal sheaf, S₀ ⊆ S is a thickening, each stratum S_i ∖ S_{i+1} carries a surjective finite locally free morphism T_i → S_i ∖ S_{i+1}, and X ×_S T_i carries closed subschemes X ×_S T_i ⊇ Z_{i,0} ⊇ ⋯ ⊇ Z_{i,t_i} = ∅, each defined by a finite type ideal sheaf, with Z_{i,0} ⊆ X ×_S T_i a thickening and each Z_{i,j} ∖ Z_{i,j+1} → T_i smooth.

theorem hasSmoothStratificationAfterFiniteLocallyFreeCover {X S : Scheme.{u}}
    [CompactSpace X] [QuasiSeparatedSpace X] [CompactSpace S] [QuasiSeparatedSpace S]
    (f : X ⟶ S) (hf : FinitePresentation f) :
    HasSmoothStratificationAfterFiniteLocallyFreeCover f

Sources

LeanAlgebraicGeometry.exists_smooth_stratification_at_generic_point · AlgebraicGeometry.hasSmoothStratificationAfterFiniteLocallyFreeCover

Section37.56 Improving morphisms of relative dimension one #

Section 37.56 of the Stacks Project, Tag 0GK6. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GK7, a lemma

Tag 0GK7 in the Stacks Project.

AlgebraicGeometry.exists_curveDiagram_near_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeDimensionOne/CurveDiagram.lean, line 483.

Stacks Project, Tag 0GK7. Let f : X ⟶ S be separated and of finite presentation, and let η be a generic point of an irreducible component of S such that dim(X_η) ≤ 1. Then there are

an open neighbourhood U of η,

a finite, surjective, universally injective morphism V ⟶ U,

the base change X_V = V ×_S X, a pullback square over V ⟶ U ⟶ S,

a finite surjective morphism ν : ∐ Yᵢ ⟶ X_V and an open W ⊆ X_V such that W is dense in all fibres of X_V ⟶ V, ν⁻¹(W) ∩ Yᵢ is dense in all fibres of Yᵢ ⟶ Tᵢ, and ν⁻¹(W) ⟶ W is a thickening,

open immersions jᵢ : Yᵢ ⟶ Ȳᵢ,

finite étale morphisms Tᵢ ⟶ V,

surjective smooth morphisms Yᵢ ⟶ Tᵢ, and

smooth proper morphisms Ȳᵢ ⟶ Tᵢ with geometrically connected fibres of dimension at most one,

such that the diagram commutes: jᵢ ≫ (Ȳᵢ ⟶ Tᵢ) = (Yᵢ ⟶ Tᵢ) and the map Yᵢ ⟶ X_V ⟶ V is Yᵢ ⟶ Tᵢ ⟶ V.

theorem exists_curveDiagram_near_genericPoint {X S : Scheme.{u}} (f : X ⟶ S) [IsSeparated f]
    (hf : FinitePresentation f) (η : S) (hη : η ∈ genericPoints S)
    (hdim : topologicalKrullDim (f.fiber η) ≤ 1) :
    ∃ (U : S.Opens) (_ : η ∈ U) (V : Scheme.{u}) (v : V ⟶ U.toScheme),
      IsFinite v ∧ Surjective v ∧ UniversallyInjective v ∧
      ∃ (XV : Scheme.{u}) (a : XV ⟶ X) (pV : XV ⟶ V), IsPullback a pV f (v ≫ U.ι) ∧
      ∃ (n : ℕ) (T Y Ybar : Fin n → Scheme.{u}) (t : ∀ i, T i ⟶ V) (q : ∀ i, Y i ⟶ T i)
        (qbar : ∀ i, Ybar i ⟶ T i) (j : ∀ i, Y i ⟶ Ybar i) (ν : (∐ Y) ⟶ XV) (W : XV.Opens),
        (∀ i, j i ≫ qbar i = q i) ∧ (∀ i, Sigma.ι Y i ≫ ν ≫ pV = q i ≫ t i) ∧
        IsFinite ν ∧ Surjective ν ∧
        (∀ s : V, Dense ((pV.fiberι s) ⁻¹' (W : Set XV))) ∧
        (∀ i (s : T i), Dense (((q i).fiberι s) ⁻¹' ((Sigma.ι Y i ≫ ν) ⁻¹' (W : Set XV)))) ∧
        Stacks.Thickenings.IsThickening (ν ∣_ W) ∧
        (∀ i, IsOpenImmersion (j i)) ∧ (∀ i, IsFinite (t i) ∧ Etale (t i)) ∧
        (∀ i, Surjective (q i) ∧ Smooth (q i)) ∧
        (∀ i, IsProper (qbar i) ∧ Smooth (qbar i) ∧
          (∀ s : T i, GeometricallyConnected ((qbar i).fiberToSpecResidueField s)) ∧
          ∀ s : T i, topologicalKrullDim ((qbar i).fiber s) ≤ 1)

Sources

LeanAlgebraicGeometry.exists_curveDiagram_near_genericPoint

Section37.57 Descending separated locally quasi-finite morphisms #

Section 37.57 of the Stacks Project, Tag 02W7. 1 tag here is carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02W8, a lemma

Tag 02W8 in the Stacks Project.

AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isSeparated_inf_locallyQuasiFinite_inf_lft, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiAffineEtaleDescent.lean, line 474. The attribute's comment: “effective descent along a surjective étale chart of the site”.

Effective descent along the surjective étale morphisms of the big fppf site of S for the separated, locally quasi-finite morphisms which are locally of finite type.

theorem isEffectiveDescentAlongSurjectiveEtale_isSeparated_inf_locallyQuasiFinite_inf_lft
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    IsEffectiveDescentAlongSurjectiveEtale B S hS
      (@_root_.AlgebraicGeometry.IsSeparated.{u} ⊓ @LocallyQuasiFinite ⊓ @LocallyOfFiniteType :
        MorphismProperty Scheme.{u})

AlgebraicGeometry.Space.isEffectiveDescentAlongCoveringSieve_monomorphisms_inf_lft, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiAffineFlatChartDescent.lean, line 519. The attribute's comment: “effective descent along the covering sieves of the site, at the monomorphisms locally of finite type”.

Effective descent along the covering sieves of the big fppf site of S at the monomorphisms locally of finite type, unconditionally. This is isEffectiveDescentAlongCoveringSieve_monomorphisms_inf_lft_of_isQuasiAffineHom with its hypothesis discharged, and it is the descent hypothesis which the diagonal of a quotient sheaf consumes. (The name of that conditional statement is too long to cite on one line here; it lives in StacksFrontier.AlgebraicGeometry.Descent.CoveringSieveQuasiAffineDescent.)

No cardinal hypothesis and no hypothesis on the site's cutoff is used: the passage from affine to arbitrary base objects is paid for by AlgebraicGeometry.Scheme.size_le_of_mono, available because the property lies below the monomorphisms.

theorem isEffectiveDescentAlongCoveringSieve_monomorphisms_inf_lft :
    IsEffectiveDescentAlongCoveringSieve B S hS
      (MorphismProperty.monomorphisms Scheme.{u} ⊓ @LocallyOfFiniteType)

AlgebraicGeometry.DescentDatum.isEffective_of_isSeparated_of_locallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SeparatedQuasiFiniteSchemeDescent.lean, line 188. The attribute's comment: “the scheme-descent-datum form, for a single quasi-compact chart”. References: SGA 3 X (5.4), “special case”.

Stacks, Tag 02W8 in the scheme-descent-datum form, for a single quasi-compact chart. Let f : X ⟶ S be a surjective, flat, quasi-compact morphism of schemes and let (V, φ) be a descent datum relative to X/S whose structure morphism V ⟶ X is separated, locally quasi-finite and locally of finite type. Then (V, φ) is effective: it is isomorphic to the canonical descent datum of a scheme over S.

Such a structure morphism is ind-quasi-affine by Stacks 0AP9, so this is Gabber's effectivity AlgebraicGeometry.DescentDatum.isEffective_of_isIndQuasiAffineHom_of_quasiCompact.

theorem isEffective_of_isSeparated_of_locallyQuasiFinite {S X : Scheme.{u}} {f : X ⟶ S}
    [Surjective f] [Flat f] [QuasiCompact f] (D : DescentDatum f)
    (hsep : IsSeparated D.over.hom) (hqf : LocallyQuasiFinite D.over.hom)
    (hft : LocallyOfFiniteType D.over.hom) : DescentData.IsEffective D

AlgebraicGeometry.DescentData.isFamilyEffective_of_forall_isSeparated_of_locallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SeparatedQuasiFiniteSchemeDescent.lean, line 224. References: SGA 3 X (5.4), “more general”.

Stacks, Tag 02W8. Let S be a scheme, let {X i ⟶ S} be an fppf covering family and let D = (V i / X i, φ i j) be a descent datum relative to that family. If each morphism V i ⟶ X i is separated and locally quasi-finite, then the descent datum is effective: it is isomorphic to the canonical descent datum of a scheme over S.

Quasi-finiteness is Stacks 02NG — AlgebraicGeometry.LocallyQuasiFinite together with AlgebraicGeometry.LocallyOfFiniteType, as in the formalization of Stacks 01TD, of Stacks 02LR and of Stacks 0AP9, Mathlib's LocallyQuasiFinite not itself asking for local finite type.

Such a structure morphism is ind-quasi-affine by Stacks 0AP9, AlgebraicGeometry.isIndQuasiAffineHom_of_isSeparated_of_locallyQuasiFinite, and an fppf covering family is an fpqc covering family, so this is Gabber's effectivity AlgebraicGeometry.DescentData.isFamilyEffective_of_forall_isIndQuasiAffineHom_of_anyIndex.

theorem isFamilyEffective_of_forall_isSeparated_of_locallyQuasiFinite {ι : Type v}
    {S : Scheme.{u}} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ S)
    (hf : Presieve.ofArrows X f ∈ Scheme.fppfPrecoverage S) (D : DescentData f)
    (hsep : ∀ i, IsSeparated (D.obj i).hom)
    (hqf : ∀ i, LocallyQuasiFinite (D.obj i).hom)
    (hft : ∀ i, LocallyOfFiniteType (D.obj i).hom) :
    D.IsFamilyEffective

AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveFlat_isSeparated_inf_locallyQuasiFinite_inf_lft, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SurjectiveFlatDescent.lean, line 442. The attribute's comment: “effective descent along a single surjective flat chart of the site”.

Effective descent along a single surjective flat morphism of the site locally of finite presentation, for the separated locally quasi-finite morphisms locally of finite type, over an arbitrary base object, unconditionally.

This is the property of Stacks 02W8 descended along the one-element fppf coverings, which is the shape Stacks 046J consumes: that tag reduces to a covering {F → G} by a single surjective, flat morphism locally of finite presentation, not to a general covering sieve.

All five steps of Stacks 02W8 are discharged. Steps 1, 2 and 5 over an affine base, together with steps 3 and 4, are AlgebraicGeometry.Space.coveringSieveBody_affineBase_isSeparated_inf_locallyQuasiFinite_inf_lft; the passage from an affine base object to an arbitrary one is AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveFlat_of_affineBase, whose glueing is paid for by the size bound of the single flat covering morphism.

Compare isEffectiveDescentAlongCoveringSieve_isSeparated_inf_lqf_inf_lft_of_isRegular in this namespace, the same property in the covering-sieve shape, which carries a regularity hypothesis on the site's cutoff. That hypothesis is not an artefact: a covering sieve supplies no single surjective morphism whose size bounds the glueing, and the property of Stacks 02W8 admits no size bound of its own, ∐_{i < κ} Spec A ⟶ Spec A having it for every κ. Restricting to one-element coverings is exactly what removes the hypothesis.

theorem isEffectiveDescentAlongSurjectiveFlat_isSeparated_inf_locallyQuasiFinite_inf_lft
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    IsEffectiveDescentAlongSurjectiveFlat B S hS
      (@_root_.AlgebraicGeometry.IsSeparated.{u} ⊓ @LocallyQuasiFinite ⊓ @LocallyOfFiniteType :
        MorphismProperty Scheme.{u})

AlgebraicGeometry.FormalSpace.isEffectiveDescentAlongSurjectiveEtale_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ReductionDescent.lean, line 147. The attribute's comment: “effective descent along a surjective étale chart of the site, for thickenings”.

Effective descent along a surjective étale morphism of the big fppf site of S holds for the thickenings.

theorem isEffectiveDescentAlongSurjectiveEtale_isThickening :
    Space.IsEffectiveDescentAlongSurjectiveEtale B S hS
      (@Stacks.Thickenings.IsThickening : MorphismProperty Scheme.{u})

Sources

LeanAlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isSeparated_inf_locallyQuasiFinite_inf_lft · AlgebraicGeometry.Space.isEffectiveDescentAlongCoveringSieve_monomorphisms_inf_lft · AlgebraicGeometry.DescentDatum.isEffective_of_isSeparated_of_locallyQuasiFinite · AlgebraicGeometry.DescentData.isFamilyEffective_of_forall_isSeparated_of_locallyQuasiFinite · AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveFlat_isSeparated_inf_locallyQuasiFinite_inf_lft · AlgebraicGeometry.FormalSpace.isEffectiveDescentAlongSurjectiveEtale_isThickening

Section37.58 Relative finite presentation #

Section 37.58 of the Stacks Project, Tag 05GX. 9 tags here are carried by 13 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05H1, a definition

Tag 05H1 in the Stacks Project.

AlgebraicGeometry.IsFinitelyPresentedRelative, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/RelativeFinitePresentation/Defs.lean, line 59.

A sheaf of modules M on X is finitely presented relative to S if there is an affine open cover of S and, over each member, an affine open cover of its inverse image such that the corresponding module of sections of M is finitely presented relative to the ring of functions on the base open.

abbrev IsFinitelyPresentedRelative {X S : Scheme.{u}} (f : X ⟶ S) (M : X.Modules) : Prop

Tag 09T7, a lemma

Tag 09T7 in the Stacks Project.

AlgebraicGeometry.isFinitelyPresentedRelative_iff_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/RelativeFinitePresentation/Affine.lean, line 389. The attribute's comment: “affine-open characterization”.

Stacks Project, Tag 09T7. A quasi-coherent module on a scheme locally of finite type over a base is finitely presented relative to that base if and only if its sections over every affine open are finitely presented relative to the sections over every compatible affine open of the base.

theorem isFinitelyPresentedRelative_iff_affine
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (M : X.Modules) [M.IsQuasicoherent] :
    IsFinitelyPresentedRelative f M ↔
      ∀ (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
            Module.FinitePresentationRel Γ(S, V) Γ(X, U) Γ(M, U)

AlgebraicGeometry.isFinitelyPresentedRelative_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/RelativeFinitePresentation/Affine.lean, line 438. The attribute's comment: “restriction to open subschemes”.

Stacks Project, Tag 09T7. Once a quasi-coherent module is finitely presented relative to a base, its restriction to any open subscheme is finitely presented relative to every compatible open subscheme of the base.

theorem isFinitelyPresentedRelative_resLE
    {X S : Scheme.{u}} {f : X ⟶ S} [LocallyOfFiniteType f]
    (M : X.Modules) [M.IsQuasicoherent]
    (hM : IsFinitelyPresentedRelative f M)
    (U : X.Opens) (V : S.Opens) (hUV : U ≤ f ⁻¹ᵁ V) :
    IsFinitelyPresentedRelative (f.resLE V U hUV) (M.restrict U.ι)

Tag 09T8, a lemma

Tag 09T8 in the Stacks Project.

AlgebraicGeometry.isFinitelyPresentedRelative_iff_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/RelativeFinitePresentation/FinitePresentation.lean, line 163. The attribute's comment: “relative_iff_finite_presentation”.

Stacks Project, Tag 09T8. For a locally finitely presented morphism of schemes, a quasi-coherent sheaf of modules is finitely presented relative to the base if and only if it is finitely presented.

theorem isFinitelyPresentedRelative_iff_isFinitePresentation
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFinitePresentation f]
    (M : X.Modules) [M.IsQuasicoherent] :
    IsFinitelyPresentedRelative f M ↔ M.IsFinitePresentation

AlgebraicGeometry.locallyOfFinitePresentation_iff_structureSheaf_finitelyPresentedRelative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/RelativeFinitePresentation/StructureSheaf.lean, line 79. The attribute's comment: “morphism_iff_structure_sheaf_relative”.

Stacks Project, Tag 09T8. A locally finite type morphism is locally of finite presentation if and only if its structure sheaf is finitely presented relative to the base.

theorem locallyOfFinitePresentation_iff_structureSheaf_finitelyPresentedRelative
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] :
    LocallyOfFinitePresentation f ↔
      IsFinitelyPresentedRelative f (SheafOfModules.unit X.ringCatSheaf)

Tag 09T9, a lemma

Tag 09T9 in the Stacks Project.

AlgebraicGeometry.isFinitelyPresentedRelative_pushforward_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeFinitePresentation/FinitePushforward.lean, line 81.

Stacks Project, Tag 09T9. A quasi-coherent module on the source of a finite morphism between schemes locally of finite type over a base is finitely presented relative to that base if and only if its pushforward is.

theorem isFinitelyPresentedRelative_pushforward_iff
    {X Y S : Scheme.{u}} (π : X ⟶ Y) (f : X ⟶ S) (g : Y ⟶ S)
    (hπ : π ≫ g = f) [IsFinite π] [LocallyOfFiniteType f]
    [LocallyOfFiniteType g] (M : X.Modules) [M.IsQuasicoherent] :
    IsFinitelyPresentedRelative g ((Scheme.Modules.pushforward π).obj M) ↔
      IsFinitelyPresentedRelative f M

Tag 09TA, a lemma

Tag 09TA in the Stacks Project.

AlgebraicGeometry.isFinitelyPresentedRelative_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeFinitePresentation/BaseChange.lean, line 215.

Stacks Project, Tag 09TA. Relative finite presentation of a quasi-coherent module is stable under arbitrary base change: if M on X is finitely presented relative to f : X ⟶ S, then its pullback to X ×_S S' is finitely presented relative to S'.

theorem isFinitelyPresentedRelative_baseChange
    {X S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S)
    [LocallyOfFiniteType f] (M : X.Modules) [M.IsQuasicoherent]
    (hM : IsFinitelyPresentedRelative f M) :
    IsFinitelyPresentedRelative (pullback.snd f g)
      ((Scheme.Modules.pullback (pullback.fst f g)).obj M)

Tag 09TB, a lemma

Tag 09TB in the Stacks Project.

AlgebraicGeometry.isFinitelyPresentedRelative_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeFinitePresentation/Pullback.lean, line 150.

Stacks Project, Tag 09TB. Relative finite presentation of a quasi-coherent module is preserved by pullback along a morphism locally of finite presentation.

theorem isFinitelyPresentedRelative_pullback
    {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
    [LocallyOfFiniteType g]
    [LocallyOfFinitePresentation f]
    (G : Y.Modules) [G.IsQuasicoherent]
    (hG : IsFinitelyPresentedRelative g G) :
    IsFinitelyPresentedRelative (f ≫ g) ((Scheme.Modules.pullback f).obj G)

Tag 09TC, a lemma

Tag 09TC in the Stacks Project.

AlgebraicGeometry.isFinitelyPresentedRelative_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/RelativeFinitePresentation/Operations.lean, line 67.

Stacks Project, Tag 09TC. Relative finite presentation of a quasi-coherent module passes through a locally finitely presented intermediate scheme.

theorem isFinitelyPresentedRelative_comp {X Y S : Scheme.{u}}
    (f : X ⟶ Y) (g : Y ⟶ S) [LocallyOfFiniteType f]
    [LocallyOfFiniteType g] [LocallyOfFinitePresentation g]
    (M : X.Modules) [M.IsQuasicoherent]
    (hM : IsFinitelyPresentedRelative f M) :
    IsFinitelyPresentedRelative (f ≫ g) M

Tag 09TD, a lemma

Tag 09TD in the Stacks Project.

AlgebraicGeometry.isFinitelyPresentedRelative_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/RelativeFinitePresentation/Operations.lean, line 170. The attribute's comment: “extension”.

In a short exact sequence of quasi-coherent modules over a locally finite type morphism, relative finite presentation of the two end terms implies that of the middle term.

theorem isFinitelyPresentedRelative_of_shortExact
    (s : RelativeFinitePresentationExactSequenceSituation.{u})
    (hleft : IsFinitelyPresentedRelative s.f s.sequence.X₁)
    (hright : IsFinitelyPresentedRelative s.f s.sequence.X₃) :
    IsFinitelyPresentedRelative s.f s.sequence.X₂

AlgebraicGeometry.isFinitelyPresentedRelative_of_shortExact_of_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/RelativeFinitePresentation/Operations.lean, line 190. The attribute's comment: “quotient”.

In a short exact sequence of quasi-coherent modules over a locally finite type morphism whose left-hand term is of finite type, relative finite presentation of the middle term implies that of the right-hand term.

theorem isFinitelyPresentedRelative_of_shortExact_of_isFiniteType
    (s : RelativeFinitePresentationExactSequenceSituation.{u})
    (hleft : s.sequence.X₁.IsFiniteType)
    (hmid : IsFinitelyPresentedRelative s.f s.sequence.X₂) :
    IsFinitelyPresentedRelative s.f s.sequence.X₃

Tag 09TE, a lemma

Tag 09TE in the Stacks Project.

AlgebraicGeometry.isFinitelyPresentedRelative_left_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/RelativeFinitePresentation/Operations.lean, line 310. The attribute's comment: “first summand”.

Stacks Project, Tag 09TE. The first summand of a relatively finitely presented direct sum is relatively finitely presented.

theorem isFinitelyPresentedRelative_left_of_biprod
    {X S : Scheme.{u}} (f : X ⟶ S) (M N : X.Modules)
    (h : IsFinitelyPresentedRelative f (M ⊞ N)) :
    IsFinitelyPresentedRelative f M

AlgebraicGeometry.isFinitelyPresentedRelative_right_of_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/RelativeFinitePresentation/Operations.lean, line 318. The attribute's comment: “second summand”.

Stacks Project, Tag 09TE. The second summand of a relatively finitely presented direct sum is relatively finitely presented.

theorem isFinitelyPresentedRelative_right_of_biprod
    {X S : Scheme.{u}} (f : X ⟶ S) (M N : X.Modules)
    (h : IsFinitelyPresentedRelative f (M ⊞ N)) :
    IsFinitelyPresentedRelative f N

Sources

LeanAlgebraicGeometry.IsFinitelyPresentedRelative · AlgebraicGeometry.isFinitelyPresentedRelative_iff_affine · AlgebraicGeometry.isFinitelyPresentedRelative_resLE · AlgebraicGeometry.isFinitelyPresentedRelative_iff_isFinitePresentation · AlgebraicGeometry.locallyOfFinitePresentation_iff_structureSheaf_finitelyPresentedRelative · AlgebraicGeometry.isFinitelyPresentedRelative_pushforward_iff · AlgebraicGeometry.isFinitelyPresentedRelative_baseChange · AlgebraicGeometry.isFinitelyPresentedRelative_pullback

Section37.59 Relative pseudo-coherence #

Section 37.59 of the Stacks Project, Tag 09UH. 18 tags here are carried by 33 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09VC, a lemma

Tag 09VC in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.isPseudoCoherentFrom_some_iff_forall_fin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/SideCondition.lean, line 338.

Stacks 09VC. Let f : X ⟶ S be a morphism of affine schemes locally of finite type, let E be an object of D(𝒪_X) and let m be an integer. Then m-pseudo-coherence of the derived pushforward of E along some closed immersion of X into a finite-dimensional affine space over S factoring f is equivalent to m-pseudo-coherence of the derived pushforward along every such closed immersion.

This is AlgebraicGeometry.Scheme.Modules.isPseudoCoherentFrom_some_iff_forall_of_transport_fin, whose transport hypothesis is supplied by the two halves of Stacks 09VA — AlgebraicGeometry.Scheme.Modules.isPseudoCoherentFrom_pushforward_mapDerivedCategory and AlgebraicGeometry.Scheme.Modules.isPseudoCoherentFrom_of_pushforward_mapDerivedCategory — and whose side condition is AlgebraicGeometry.Scheme.Modules.isPseudoCoherent_singleFunctor_pushforward_unit_affineSpace. Nothing is assumed.

public theorem isPseudoCoherentFrom_some_iff_forall_fin {X S : Scheme.{u}} [IsAffine X]
    [IsAffine S] (f : X ⟶ S) [LocallyOfFiniteType f] (E : DerivedCategory X.Modules) (m : ℤ) :
    (∃ (n : ℕ) (i : X ⟶ AffineSpace (ULift.{u} (Fin n)) S),
      IsClosedImmersion i ∧
        i ≫ (AffineSpace.over (ULift.{u} (Fin n)) S).hom = f ∧
          IsPseudoCoherentFromAfterPushforward i E m) ↔
      (∀ (n : ℕ) (i : X ⟶ AffineSpace (ULift.{u} (Fin n)) S),
        IsClosedImmersion i →
          i ≫ (AffineSpace.over (ULift.{u} (Fin n)) S).hom = f →
            IsPseudoCoherentFromAfterPushforward i E m)

Tag 09UI, a definition

Tag 09UI in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.IsPseudoCoherentFrom, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/Relative.lean, line 75. The attribute's comment: “part (1)”.

An object E of the derived category of 𝒪_X-modules is relatively m-pseudo-coherent for f : X ⟶ S locally of finite type if there are an affine open cover V of S and, for each V i, an affine open cover U of f⁻¹(V i) such that the restriction of E to each U j becomes m-pseudo-coherent after derived pushforward along some closed immersion U j ⟶ 𝔸ⁿ_{V i} over V i through which f restricted to U j factors.

public abbrev IsPseudoCoherentFrom {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (E : DerivedCategory X.Modules) (m : ℤ) : Prop

AlgebraicGeometry.Scheme.Hom.IsPseudoCoherent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/Relative.lean, line 93. The attribute's comment: “part (2)”.

An object of the derived category of 𝒪_X-modules is relatively pseudo-coherent for f if it is relatively m-pseudo-coherent for every integer m.

public abbrev IsPseudoCoherent {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (E : DerivedCategory X.Modules) : Prop

AlgebraicGeometry.Scheme.Hom.IsModulePseudoCoherentFrom, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/Relative.lean, line 100. The attribute's comment: “part (3)”.

A sheaf of 𝒪_X-modules is relatively m-pseudo-coherent for f if it is so as an object of the derived category concentrated in degree zero.

public abbrev IsModulePseudoCoherentFrom {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (F : X.Modules) (m : ℤ) : Prop

AlgebraicGeometry.Scheme.Hom.IsModulePseudoCoherent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/Relative.lean, line 107. The attribute's comment: “part (4)”.

A sheaf of 𝒪_X-modules is relatively pseudo-coherent for f if it is so as an object of the derived category concentrated in degree zero.

public abbrev IsModulePseudoCoherent {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (F : X.Modules) : Prop

Tag 0CSU, a lemma

Tag 0CSU in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isQuasicoherent_homology_of_isPseudoCoherentFrom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeQuasicoherentCohomology.lean, line 98. The attribute's comment: “quasi-coherence of the cohomology sheaves above the bound”.

Let f : X ⟶ S be a morphism of schemes locally of finite type and let E be an object of D(𝒪_X) which is m-pseudo-coherent relative to S. Then the cohomology sheaf H^i(E) is a quasi-coherent 𝒪_X-module for every i > m.

public theorem isQuasicoherent_homology_of_isPseudoCoherentFrom {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (E : DerivedCategory X.Modules) (m i : ℤ)
    (hE : f.IsPseudoCoherentFrom E m) (hi : m < i) :
    ((DerivedCategory.homologyFunctor X.Modules i).obj E).IsQuasicoherent

AlgebraicGeometry.Scheme.Hom.isQuasicoherentDerived_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeQuasicoherentCohomology.lean, line 123. The attribute's comment: “membership in the quasi-coherent derived category”.

Let f : X ⟶ S be a morphism of schemes locally of finite type and let E be an object of D(𝒪_X) which is pseudo-coherent relative to S. Then E is an object of D_QCoh(𝒪_X), that is, H^i(E) is quasi-coherent for every i.

public theorem isQuasicoherentDerived_of_isPseudoCoherent {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (E : DerivedCategory X.Modules) (hE : f.IsPseudoCoherent E) :
    DerivedCategoryB.derivedCategoryB
      (_root_.SheafOfModules.isQuasicoherent X.ringCatSheaf) E

Tag 09VD, a lemma

Tag 09VD in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.isPseudoCoherentFromAfterPushforward_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/StandardOpenSideCondition.lean, line 701.

Stacks 09VD. Let S be affine, let V be a standard open of S, let X be affine and f : X ⟶ V locally of finite type, let E be an object of D(𝒪_X) and let U be an affine open of X. If the equivalent conditions of Stacks 09VC hold for the pair (X ⟶ V, E), then they hold for the pair (U ⟶ S, E|_U).

This is AlgebraicGeometry.Scheme.Modules.exists_isPseudoCoherentFromAfterPushforward_affineOpen' with its three hypotheses discharged: AlgebraicGeometry.Scheme.Modules.pushforwardStructureSheafPseudoCoherentOver_basicOpen at the base S and at the base V, and AlgebraicGeometry.Scheme.Modules.pushforwardStructureSheafPseudoCoherentOver_affineSpace for the affine spaces over V mapping to the affine spaces over S. The last of the three is what needs V to be a standard open.

public theorem isPseudoCoherentFromAfterPushforward_restrict {S X : Scheme.{u}}
    [IsAffine S] [IsAffine X] (V : S.affineOpens) (hV : ∃ a : Γ(S, ⊤), V.1 = S.basicOpen a)
    (f : X ⟶ (V.1 : Scheme.{u})) [LocallyOfFiniteType f] [QuasiCompact f]
    (U : X.affineOpens) (E : DerivedCategory X.Modules) (m : ℤ) :
    (∃ (n : ℕ) (i : X ⟶ AffineSpace (ULift.{u} (Fin n)) (V.1 : Scheme.{u})),
      IsClosedImmersion i ∧
        i ≫ (AffineSpace.over (ULift.{u} (Fin n)) (V.1 : Scheme.{u})).hom = f ∧
          IsPseudoCoherentFromAfterPushforward i E m) →
      (∃ (n : ℕ) (i : (U.1 : Scheme.{u}) ⟶ AffineSpace (ULift.{u} (Fin n)) S),
        IsClosedImmersion i ∧
          i ≫ (AffineSpace.over (ULift.{u} (Fin n)) S).hom = U.1.ι ≫ f ≫ V.1.ι ∧
            IsPseudoCoherentFromAfterPushforward i
              ((restrictFunctor U.1.ι).mapDerivedCategory.obj E) m)

Tag 09VE, a lemma

Tag 09VE in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.isPseudoCoherentFrom_some_iff_forall_standardCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/StandardOpenSideCondition.lean, line 668.

Stacks 09VE. Let f : X ⟶ S be a morphism of affine schemes locally of finite type, let E be an object of D(𝒪_X) and let the basic opens of g : Fin n → Γ(X, ⊤) be a standard affine open cover of X. Then the equivalent conditions of Stacks 09VC hold for every pair (X_{gⱼ} ⟶ S, E|_{X_{gⱼ}}) if and only if they hold for the pair (X ⟶ S, E).

This is AlgebraicGeometry.Scheme.Modules.isPseudoCoherentFrom_some_iff_forall_basicOpen' with its hypothesis hOb discharged by AlgebraicGeometry.Scheme.Modules.pushforwardStructureSheafPseudoCoherentOver_basicOpen.

public theorem isPseudoCoherentFrom_some_iff_forall_standardCover {X S : Scheme.{u}}
    [IsAffine X] [IsAffine S] (f : X ⟶ S) [LocallyOfFiniteType f] [QuasiCompact f]
    (E : DerivedCategory X.Modules) (m : ℤ) {n : ℕ} (g : Fin n → Γ(X, ⊤))
    (hg : PrimeSpectrum.IsStandardOpenCoverOfSpectrum g) :
    (∀ j : Fin n, ∃ (k : ℕ) (i : (X.basicOpen (g j)).toScheme ⟶
        AffineSpace (ULift.{u} (Fin k)) S),
      IsClosedImmersion i ∧
        i ≫ (AffineSpace.over (ULift.{u} (Fin k)) S).hom = (X.basicOpen (g j)).ι ≫ f ∧
          IsPseudoCoherentFromAfterPushforward i
            ((restrictFunctor (X.basicOpen (g j)).ι).mapDerivedCategory.obj E) m) ↔
      (∃ (k : ℕ) (i : X ⟶ AffineSpace (ULift.{u} (Fin k)) S),
        IsClosedImmersion i ∧
          i ≫ (AffineSpace.over (ULift.{u} (Fin k)) S).hom = f ∧
            IsPseudoCoherentFromAfterPushforward i E m)

Tag 09UJ, a lemma

Tag 09UJ in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_iff_forall_affinePair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/AffinePairLocality.lean, line 501. The attribute's comment: “affine-open characterization”.

Stacks 09UJ. For f : X ⟶ S locally of finite type, E an object of the derived category of 𝒪_X-modules and m an integer, E is relatively m-pseudo-coherent if and only if the local condition of Stacks 09UI holds at every compatible pair of affine opens U ⊆ f ⁻¹ᵁ V.

The two implications are AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_of_forall_affinePair and AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFromOnAffinePair_of_isPseudoCoherentFrom.

public theorem isPseudoCoherentFrom_iff_forall_affinePair [LocallyOfFiniteType f]
    (E : DerivedCategory X.Modules) (m : ℤ) : AffinePairComparison f E m

AlgebraicGeometry.Scheme.Hom.IsPseudoCoherentFrom.resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/AffinePairLocality.lean, line 536. The attribute's comment: “restriction to open subschemes”. References: SGA 6 III (1.1), “(i)”.

Stacks 09UJ, the final assertion. If E is m-pseudo-coherent relative to S, then for every pair of open subschemes U ⊆ X and V ⊆ S with f(U) ⊆ V the restriction E|_U is m-pseudo-coherent relative to V.

By AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_iff_forall_affinePair it is enough to check the local condition at a compatible pair of affine opens A ⊆ U, B ⊆ V; their images in X and S are a compatible pair of affine opens there, the same lemma supplies the condition at that pair, and the two canonical isomorphisms A ≅ ι_U(A) and B ≅ ι_V(B) are absorbed by AlgebraicGeometry.exists_isPseudoCoherentFromAfterPushforward_openSource and AlgebraicGeometry.exists_isPseudoCoherentFromAfterPushforward_shrinkBase.

public theorem IsPseudoCoherentFrom.resLE [LocallyOfFiniteType f]
    (E : DerivedCategory X.Modules) (m : ℤ) (U : X.Opens) (V : S.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
    (hE : IsPseudoCoherentFrom f E m) :
    IsPseudoCoherentFrom (f.resLE V U hUV)
      ((Scheme.Modules.restrictFunctor U.ι).mapDerivedCategory.obj E) m

Tag 09VF, a lemma

Tag 09VF in the Stacks Project.

AlgebraicGeometry.derivedSectionsPseudoCoherentComparison', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/AffineSectionsComparison.lean, line 439.

Stacks 09VF. Let f : X ⟶ S be locally of finite type, let E be an object of the derived category of 𝒪_X-modules all of whose cohomology sheaves are quasi-coherent, and let m be an integer. Then the following are equivalent:

E is m-pseudo-coherent relative to S;

there are affine open coverings S = ⋃ Vⱼ and f ⁻¹ᵁ Vⱼ = ⋃ Uⱼᵢ such that each complex RΓ(Uⱼᵢ, E) is m-pseudo-coherent relative to Γ(S, Vⱼ);

for every affine open V ⊆ S and every affine open U ⊆ f ⁻¹ᵁ V, the complex RΓ(U, E) is m-pseudo-coherent relative to Γ(S, V).

This is AlgebraicGeometry.derivedSectionsPseudoCoherentComparison'_of_derivedSectionsSpec with its hypothesis discharged by AlgebraicGeometry.IsAffineOpen.nonempty_iso_derivedSectionsSpec.

public theorem derivedSectionsPseudoCoherentComparison' (f : X ⟶ S) [LocallyOfFiniteType f]
    (E : DerivedCategory X.Modules)
    (hE : ∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj E).IsQuasicoherent) (m : ℤ) :
    DerivedSectionsPseudoCoherentComparison' f E hE m

Tag 09VG, a lemma

Tag 09VG in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_iff_derivedPushforward_of_reductionImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/ReductionClosedPushforward.lean, line 953. The attribute's comment: “corrected statement — Stacks erratum. The source's topological hypothesis, that i induce a homeomorphism of X with a closed subset of Y, makes the lemma false (AlgebraicGeometry.Scheme.Hom.not_forall_isPseudoCoherentFrom_iff_derivedPushforward, over the nodal curve A = {h ∈ k[s] | h(0) = h(1)} with B = k[s, 1/s]); it is replaced here by the hypothesis the source's proof actually uses, that i be a closed immersion on reductions, i.e. that A/rad(A) → B/rad(B) be surjective. Both directions, E and m arbitrary”.

Let f : X ⟶ S and g : Y ⟶ S be morphisms of schemes locally of finite type and let i : X ⟶ Y be a morphism over S which induces a closed immersion on reductions: there is a closed immersion j of the reduction of X into the reduction of Y making the square with the canonical immersions of the reductions commute. Let E be an object of D(𝒪_X) and m an integer. Then E is m-pseudo-coherent relative to S if and only if Ri_*E is m-pseudo-coherent relative to S.

With the hypothesis on i weakened to a homeomorphism of X with a closed subset of Y the equivalence fails, by AlgebraicGeometry.Scheme.Hom.not_forall_isPseudoCoherentFrom_iff_derivedPushforward.

public theorem Scheme.Hom.isPseudoCoherentFrom_iff_derivedPushforward_of_reductionImmersion
    {X Y S : Scheme.{u}}
    (f : X ⟶ S) (g : Y ⟶ S) [LocallyOfFiniteType f] [LocallyOfFiniteType g] (i : X ⟶ Y)
    (hi : i ≫ g = f)
    (hred : ∃ j : X.nilradical.subscheme ⟶ Y.nilradical.subscheme,
      IsClosedImmersion j ∧
        j ≫ Y.nilradical.subschemeι = X.nilradical.subschemeι ≫ i)
    (E : DerivedCategory X.Modules) (m : ℤ) :
    Scheme.Hom.IsPseudoCoherentFrom f E m ↔
      Scheme.Hom.IsPseudoCoherentFrom g
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward
          i.toLRSHom.toShHom).obj E) m

Tag 09UK, a lemma

Tag 09UK in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_iff_derivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeFinitePushforward.lean, line 237. References: SGA 6 III (2.1), “finite morphism, QCoh”; SGA 6 III (2.2), “special case”; SGA 6 IV (3.3.2), “3.3.2.3”.

Stacks 09UK. Let π : X ⟶ Y be a finite morphism of schemes locally of finite type over a base S, and let E be an object of the derived category of 𝒪_X-modules with quasi-coherent cohomology. Then E is m-pseudo-coherent relative to S if and only if Rπ_* E is.

The proof is the translation the source asks for. In one direction Stacks 09VF, which is AlgebraicGeometry.derivedSectionsPseudoCoherentComparison', turns relative m-pseudo-coherence of E into its per-pair condition at every compatible pair of affine opens, and AlgebraicGeometry.derivedSectionsPseudoCoherentOn'_preimage_iff carries the condition at (π ⁻¹ᵁ U, V) to the condition at (U, V) for Rπ_* E, at every pair of the target. In the other direction the covers the source provides for Rπ_* E cannot be used directly — an affine open of X need not be an inverse image — so the "exists an affine cover" form of Stacks 09VF is used instead and its covers are pulled back along π, which is where the morphism being over S enters. That Rπ_* E again has quasi-coherent cohomology, so that Stacks 09VF applies to it, is clause (1) of Stacks 08D5 by way of AlgebraicGeometry.preservesQuasicoherentOnAffineTarget.

public theorem Scheme.Hom.isPseudoCoherentFrom_iff_derivedPushforward
    {X Y S : Scheme.{u}} (π : X ⟶ Y) (f : X ⟶ S) (g : Y ⟶ S)
    (hπ : π ≫ g = f) [IsFinite π] [LocallyOfFiniteType f] [LocallyOfFiniteType g]
    (E : DerivedCategory X.Modules)
    (hE : ∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj E).IsQuasicoherent)
    (m : ℤ) :
    Scheme.Hom.IsPseudoCoherentFrom f E m ↔
      Scheme.Hom.IsPseudoCoherentFrom g
        ((RingedSpace.derivedPushforward π.toLRSHom.toShHom).obj E) m

Tag 09UL, a lemma

Tag 09UL in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_obj₃_of_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeTriangle.lean, line 96. The attribute's comment: “part (1)”. References: SGA 6 I (2.6), “row 1 (n+1, n, n)”; SGA 6 III (1.4), “1st line (G underlined)”.

Stacks 09UL, part (1). If the first term of a distinguished triangle of D(𝒪_X) is (m + 1)-pseudo-coherent relative to S and the second is m-pseudo-coherent relative to S, then the third is m-pseudo-coherent relative to S.

public theorem isPseudoCoherentFrom_obj₃_of_distinguished [LocallyOfFiniteType f] (m : ℤ)
    (T : Triangle (DerivedCategory X.Modules)) (hT : T ∈ distinguishedTriangles)
    (hE : IsPseudoCoherentFrom f T.obj₁ (m + 1)) (hE' : IsPseudoCoherentFrom f T.obj₂ m) :
    IsPseudoCoherentFrom f T.obj₃ m

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_obj₂_of_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeTriangle.lean, line 119. The attribute's comment: “part (2)”. References: SGA 6 I (2.6), “row 2 (n, n, n)”; SGA 6 III (1.4), “2nd line (F underlined)”.

Stacks 09UL, part (2). If the first and third terms of a distinguished triangle of D(𝒪_X) are m-pseudo-coherent relative to S, then so is the second.

public theorem isPseudoCoherentFrom_obj₂_of_distinguished [LocallyOfFiniteType f] (m : ℤ)
    (T : Triangle (DerivedCategory X.Modules)) (hT : T ∈ distinguishedTriangles)
    (hE : IsPseudoCoherentFrom f T.obj₁ m) (hE'' : IsPseudoCoherentFrom f T.obj₃ m) :
    IsPseudoCoherentFrom f T.obj₂ m

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_obj₁_of_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeTriangle.lean, line 144. The attribute's comment: “part (3)”. References: SGA 6 I (2.6), “row 3 (n, n, n-1)”; SGA 6 III (1.4), “3rd line (E underlined)”.

Stacks 09UL, part (3). If the second term of a distinguished triangle of D(𝒪_X) is (m + 1)-pseudo-coherent relative to S and the third is m-pseudo-coherent relative to S, then the first is (m + 1)-pseudo-coherent relative to S.

public theorem isPseudoCoherentFrom_obj₁_of_distinguished [LocallyOfFiniteType f] (m : ℤ)
    (T : Triangle (DerivedCategory X.Modules)) (hT : T ∈ distinguishedTriangles)
    (hE' : IsPseudoCoherentFrom f T.obj₂ (m + 1)) (hE'' : IsPseudoCoherentFrom f T.obj₃ m) :
    IsPseudoCoherentFrom f T.obj₁ (m + 1)

AlgebraicGeometry.Scheme.Hom.isPseudoCoherent_obj₃_of_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeTriangle.lean, line 166. The attribute's comment: “moreover, third term”.

Stacks 09UL, the "moreover" clause for the third term. If the first two terms of a distinguished triangle of D(𝒪_X) are pseudo-coherent relative to S, so is the third.

public theorem isPseudoCoherent_obj₃_of_distinguished [LocallyOfFiniteType f]
    (T : Triangle (DerivedCategory X.Modules)) (hT : T ∈ distinguishedTriangles)
    (hE : IsPseudoCoherent f T.obj₁) (hE' : IsPseudoCoherent f T.obj₂) :
    IsPseudoCoherent f T.obj₃

AlgebraicGeometry.Scheme.Hom.isPseudoCoherent_obj₂_of_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeTriangle.lean, line 175. The attribute's comment: “moreover, second term”.

Stacks 09UL, the "moreover" clause for the second term. If the first and third terms of a distinguished triangle of D(𝒪_X) are pseudo-coherent relative to S, so is the second.

public theorem isPseudoCoherent_obj₂_of_distinguished [LocallyOfFiniteType f]
    (T : Triangle (DerivedCategory X.Modules)) (hT : T ∈ distinguishedTriangles)
    (hE : IsPseudoCoherent f T.obj₁) (hE'' : IsPseudoCoherent f T.obj₃) :
    IsPseudoCoherent f T.obj₂

AlgebraicGeometry.Scheme.Hom.isPseudoCoherent_obj₁_of_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeTriangle.lean, line 184. The attribute's comment: “moreover, first term”.

Stacks 09UL, the "moreover" clause for the first term. If the last two terms of a distinguished triangle of D(𝒪_X) are pseudo-coherent relative to S, so is the first.

public theorem isPseudoCoherent_obj₁_of_distinguished [LocallyOfFiniteType f]
    (T : Triangle (DerivedCategory X.Modules)) (hT : T ∈ distinguishedTriangles)
    (hE' : IsPseudoCoherent f T.obj₂) (hE'' : IsPseudoCoherent f T.obj₃) :
    IsPseudoCoherent f T.obj₁

Tag 09UM, a lemma

Tag 09UM in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isModulePseudoCoherentFrom_neg_one_iff_isFinitelyPresentedRelative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeFinitePresentationDegree.lean, line 153. The attribute's comment: “degree_minus_one”. References: SGA 6 III (1.2.1).

Stacks 09UM, the degree-minus-one clause. For a morphism of schemes locally of finite type, a sheaf of 𝒪_X-modules is (-1)-pseudo-coherent relative to the base if and only if it is quasi-coherent and finitely presented relative to the base.

Stacks 09UJ turns relative (-1)-pseudo-coherence into the local condition of Stacks 09UI at every compatible pair of affine opens U ⊆ f ⁻¹ᵁ V, where by Stacks 09V9(2) it says that the direct image of ℱ|_U along a closed immersion i : U ⟶ 𝔸ⁿ_V over V is of finite presentation. Finite presentation of i_*(ℱ|_U) gives quasi-coherence of ℱ|_U, and quasi-coherence is local on X; it also gives relative finite presentation of ℱ|_U over V by Stacks 09T8 and 09T9, which is the affine-pair criterion of Stacks 09T7. Conversely Stacks 09T7 restricts relative finite presentation to the pair, and Stacks 09T9 and 09T8 turn it back into finite presentation of i_*(ℱ|_U) at a closed immersion of our own choosing.

public theorem isModulePseudoCoherentFrom_neg_one_iff_isFinitelyPresentedRelative
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] (F : X.Modules) :
    IsModulePseudoCoherentFrom f F (-1) ↔
      (F.IsQuasicoherent ∧ IsFinitelyPresentedRelative f F)

AlgebraicGeometry.Scheme.Hom.isModulePseudoCoherentFrom_zero_iff_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeModuleDegrees.lean, line 65. The attribute's comment: “degree_zero”.

Stacks 09UM, the degree-zero clause. For a morphism of schemes locally of finite type, a sheaf of 𝒪_X-modules is 0-pseudo-coherent relative to the base if and only if it is of finite type.

Stacks 09UJ turns relative 0-pseudo-coherence into the local condition of Stacks 09UI at every compatible pair of affine opens, where it is finiteness of type of the restriction of ℱ to the source open; finiteness of type is inherited by restriction and is local on X, which gives the two implications.

public theorem isModulePseudoCoherentFrom_zero_iff_isFiniteType {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (F : X.Modules) :
    IsModulePseudoCoherentFrom f F 0 ↔ F.IsFiniteType

AlgebraicGeometry.Scheme.Hom.isModulePseudoCoherentFrom_of_pos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/TrivialRange.lean, line 168. The attribute's comment: “positive_degrees”.

Stacks 09UM, the positive degrees. For a morphism of schemes locally of finite type, every sheaf of 𝒪_X-modules is relatively m-pseudo-coherent whenever 0 < m.

The affine open covering of the base is the family of all affine opens, and over each member the covering of its inverse image is the family of all affine opens of X contained in it; the closed immersions into affine space are the ones produced by AlgebraicGeometry.exists_isClosedImmersion_affineSpace_resLE, and the local condition at each of them holds because the restriction of a sheaf of modules is still concentrated in degree zero.

public theorem isModulePseudoCoherentFrom_of_pos {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (F : X.Modules) {m : ℤ} (hm : 0 < m) :
    IsModulePseudoCoherentFrom f F m

Tag 09UN, a lemma

Tag 09UN in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.IsPseudoCoherentFrom.of_biprod_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeSummand.lean, line 107. The attribute's comment: “first summand”.

Stacks 09UN, first summand. If E ⊕ K is m-pseudo-coherent relative to S then so is E.

public theorem IsPseudoCoherentFrom.of_biprod_left {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (E K : DerivedCategory X.Modules) (m : ℤ)
    (h : IsPseudoCoherentFrom f (E ⊞ K) m) : IsPseudoCoherentFrom f E m

AlgebraicGeometry.Scheme.Hom.IsPseudoCoherentFrom.of_biprod_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeSummand.lean, line 115. The attribute's comment: “second summand”.

Stacks 09UN, second summand. If E ⊕ K is m-pseudo-coherent relative to S then so is K.

public theorem IsPseudoCoherentFrom.of_biprod_right {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (E K : DerivedCategory X.Modules) (m : ℤ)
    (h : IsPseudoCoherentFrom f (E ⊞ K) m) : IsPseudoCoherentFrom f K m

Tag 09UP, a lemma

Tag 09UP in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_Q_of_locally_boundedAbove, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeBoundedComplex.lean, line 144.

Stacks 09UP. Let f : X ⟶ S be a morphism of schemes locally of finite type, let m be an integer and let 𝓕 be a complex of 𝒪_X-modules which is bounded above on a neighbourhood of every point. If 𝓕ⁱ is (m - i)-pseudo-coherent relative to S for every i, then 𝓕 is m-pseudo-coherent relative to S.

By Stacks 09UJ it is enough to check the local condition of Stacks 09UI at a compatible pair of affine opens U ⊆ f ⁻¹ᵁ V, and by Stacks 09VC it may be checked at any one closed immersion i : U ⟶ 𝔸ⁿ_V over V. There it says that the complex i_*(𝓕|_U) on 𝔸ⁿ_V represents an m-pseudo-coherent object, which is the globally bounded above case of Stacks 09V7: the terms are m-pseudo-coherent in their degrees because each 𝓕ⁱ is relatively (m - i)-pseudo-coherent at the same pair and the same closed immersion, and the complex is bounded above on all of the quasi-compact U.

public theorem isPseudoCoherentFrom_Q_of_locally_boundedAbove [LocallyOfFiniteType f] (m : ℤ)
    (F : CochainComplex X.Modules ℤ)
    (hbdd : ∀ x : X, ∃ U : X.Opens, x ∈ U ∧ ∃ b : ℤ, ∀ i : ℤ, b < i →
      IsZero ((Scheme.Modules.restrictFunctor U.ι).obj (F.X i)))
    (hterms : ∀ i : ℤ, IsModulePseudoCoherentFrom f (F.X i) (m - i)) :
    IsPseudoCoherentFrom f (DerivedCategory.Q.obj F) m

Tag 09UQ, a lemma

Tag 09UQ in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_of_homology_of_locally_boundedAbove, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeBoundedAboveCohomology.lean, line 55.

Let f : X ⟶ S be a morphism of schemes locally of finite type, let m be an integer and let E be an object of D(𝒪_X) whose cohomology sheaves vanish in high degrees on a neighbourhood of every point. If H^i(E) is (m - i)-pseudo-coherent relative to S for every i, then E is m-pseudo-coherent relative to S.

public theorem isPseudoCoherentFrom_of_homology_of_locally_boundedAbove [LocallyOfFiniteType f]
    (m : ℤ) (E : DerivedCategory X.Modules)
    (hbdd : ∀ x : X, ∃ U : X.Opens, x ∈ U ∧ ∃ b : ℤ, ∀ i : ℤ, b < i →
      IsZero ((Scheme.Modules.restrictFunctor U.ι).obj
        ((DerivedCategory.homologyFunctor X.Modules i).obj E)))
    (hcoh : ∀ i : ℤ, IsModulePseudoCoherentFrom f
      ((DerivedCategory.homologyFunctor X.Modules i).obj E) (m - i)) :
    IsPseudoCoherentFrom f E m

Tag 09UR, a lemma

Tag 09UR in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_derivedPullback_of_torIndependent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/ChartTorIndependence.lean, line 467. References: SGA 6 III (1.10); SGA 6 III (1.8), “special case”.

Stacks 09UR. Let f : X ⟶ S be locally of finite type, let E be an object of D(𝒪_X) which is m-pseudo-coherent relative to S, and let g : S' ⟶ S be a morphism of schemes. If S' and X are Tor independent over S, then the derived pullback of E to X ×_S S' is m-pseudo-coherent relative to S'.

This is AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_derivedPullback_of_torIndependentCharts with its chart hypothesis discharged by AlgebraicGeometry.Scheme.Hom.chartTorIndependence_of_torIndependent, so the Tor independence assumed here is the one the source assumes.

No hypothesis beyond the source's is assumed. Stacks 0E23, the base change isomorphism stated as AlgebraicGeometry.DerivedBaseChangeIsoOfTorIndependent, is proved — AlgebraicGeometry.derivedBaseChangeIsoOfTorIndependent, from Stacks.Cohomology.ClosedImmersionBaseChange.isIso_derivedBaseChangeMap_of_torIndependent — so it is not needed as a hypothesis here. The tag for Stacks 09UR sits here rather than on AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_derivedPullback_of_torIndependentCharts, because the source's hypothesis is Tor independence of X and S' over S, which is what this statement assumes; the chart form that one assumes is strictly stronger-looking and is derived here by AlgebraicGeometry.Scheme.Hom.chartTorIndependence_of_torIndependent.

public theorem Scheme.Hom.isPseudoCoherentFrom_derivedPullback_of_torIndependent
    {X S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S) [LocallyOfFiniteType f]
    (E : DerivedCategory X.Modules) (m : ℤ)
    (htor : TorIndependent f g) (hE : f.IsPseudoCoherentFrom E m) :
    (pullback.snd f g).IsPseudoCoherentFrom
      ((derivedPullback (pullback.fst f g).toLRSHom.toShHom).obj E) m

Tag 09US, a lemma

Tag 09US in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_comp_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/DerivedPullback09US.lean, line 1205.

Stacks 09US. Let f : X ⟶ Y be a pseudo-coherent morphism of schemes, let g : Y ⟶ S be locally of finite type and let E be an object of D(𝒪_Y) which is m-pseudo-coherent relative to S. Then the derived pullback Lf^*E is m-pseudo-coherent relative to S.

The hypothesis on f is AlgebraicGeometry.PseudoCoherent, which by Stacks 067Y is the conjunction of the two hypotheses of the source: f is locally of finite type and 𝒪_X is pseudo-coherent relative to Y.

No hypothesis beyond those of the source is needed. The appeal the source makes to Stacks 0E23, through Stacks 09UR, is at a square whose horizontal morphism is flat — it is AlgebraicGeometry.AffineSpace.map of a restriction of the flat projection 𝔸ᵈ_W ⟶ W — and that case of 0E23 is AlgebraicGeometry.nonempty_derivedPullbackPushforwardIso, proved in this file.

public theorem Scheme.Hom.isPseudoCoherentFrom_comp_derivedPullback {X Y S : Scheme.{u}} (f : X ⟶ Y)
    (g : Y ⟶ S) [PseudoCoherent f] [LocallyOfFiniteType g] (E : DerivedCategory Y.Modules)
    (m : ℤ) (hE : g.IsPseudoCoherentFrom E m) :
    (f ≫ g).IsPseudoCoherentFrom ((derivedPullback f.toLRSHom.toShHom).obj E) m

Tag 09UT, a lemma

Tag 09UT in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_iff_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeComp09UT.lean, line 269. The attribute's comment: “the equivalence, with pseudo-coherence of g as a class”. References: SGA 6 III (1.12); SGA 6 I (2.14), “(ii)”; SGA 6 III (1.11), “b), g pseudo-coherent”.

Stacks 09UT. Let f : X ⟶ Y be locally of finite type, let g : Y ⟶ S be pseudo-coherent, let E be an object of D(𝒪_X) and let m be an integer. Then E is m-pseudo-coherent relative to Y if and only if it is m-pseudo-coherent relative to S.

The two implications are AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_comp and AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_of_comp.

public theorem isPseudoCoherentFrom_iff_comp (E : DerivedCategory X.Modules) (m : ℤ) :
    f.IsPseudoCoherentFrom E m ↔ (f ≫ g).IsPseudoCoherentFrom E m

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_iff_comp_of_isModulePseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeComp09UT.lean, line 286. The attribute's comment: “the equivalence, with the hypothesis in the shape of condition (3) of 067Y”. References: SGA 6 III (1.12); SGA 6 I (2.14), “(ii)”; SGA 6 III (1.11), “b), g pseudo-coherent”.

Stacks 09UT with pseudo-coherence of g in the shape of condition (3) of Stacks 067Y. Let f : X ⟶ Y be locally of finite type and let g : Y ⟶ S be locally of finite type with 𝒪_Y pseudo-coherent relative to S. Then an object E of D(𝒪_X) is m-pseudo-coherent relative to Y if and only if it is m-pseudo-coherent relative to S.

The hypothesis is condition (3) of Stacks 067Y rather than AlgebraicGeometry.PseudoCoherent; the two are interchangeable by the unconditional AlgebraicGeometry.pseudoCoherent_iff_isModulePseudoCoherent, so this is AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_iff_comp.

public theorem isPseudoCoherentFrom_iff_comp_of_isModulePseudoCoherent {X Y S : Scheme.{u}}
    (f : X ⟶ Y) (g : Y ⟶ S) [LocallyOfFiniteType f]
    (hg : ∃ hft : LocallyOfFiniteType g,
      letI := hft
      Scheme.Hom.IsModulePseudoCoherent g (SheafOfModules.unit Y.ringCatSheaf))
    (E : DerivedCategory X.Modules) (m : ℤ) :
    letI : LocallyOfFiniteType g := hg.choose
    letI : LocallyOfFiniteType (f ≫ g) := locallyOfFiniteType_comp f g
    f.IsPseudoCoherentFrom E m ↔ (f ≫ g).IsPseudoCoherentFrom E m

Tag 09UU, a lemma

Tag 09UU in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_iff_derivedPushforwardRelative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/DerivedRelative09UU.lean, line 294. The attribute's comment: “the equivalence of clauses (1) and (2), at a closed immersion”. References: SGA 6 III (2.1), “special case”.

Stacks 09UU, the equivalence of clauses (1) and (2). Let i : X ⟶ P be a closed immersion of schemes and let p : P ⟶ S be locally of finite type. For an object E of D(𝒪_X) and an integer m, E is relatively m-pseudo-coherent for i ≫ p if and only if the unbounded derived pushforward Ri_*E is relatively m-pseudo-coherent for p.

This is AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_iff_pushforwardMapDerivedCategory transported along Stacks.ClosedImmersion.derivedPushforwardIsoMapDerivedCategoryOfSchemes, which identifies the chosen total right derived functor Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward with the functor the exact i_* induces on derived categories; relative m-pseudo-coherence depends only on the isomorphism class of its argument.

public theorem Scheme.Hom.isPseudoCoherentFrom_iff_derivedPushforwardRelative {X P S : Scheme.{u}}
    (i : X ⟶ P) (p : P ⟶ S) [IsClosedImmersion i] [LocallyOfFiniteType p]
    (E : DerivedCategory X.Modules) (m : ℤ) :
    (i ≫ p).IsPseudoCoherentFrom E m ↔
      p.IsPseudoCoherentFrom
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward
          i.toLRSHom.toShHom).obj E) m

AlgebraicGeometry.Scheme.Hom.derivedPushforwardRelative_iff_pseudoCoherentFrom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeAbsolute.lean, line 213. The attribute's comment: “the equivalence of clauses (2) and (3)”.

Stacks 09UU, the equivalence of clauses (2) and (3). Let i : X ⟶ P be a morphism of schemes and let p : P ⟶ S be flat and locally of finite presentation. For an object E of D(𝒪_X) and an integer m, the unbounded derived pushforward Ri_*E is relatively m-pseudo-coherent for p if and only if it is m-pseudo-coherent on P.

This is AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_iff_of_pseudoCoherent at the object Ri_*E, together with AlgebraicGeometry.pseudoCoherent_of_flat_of_locallyOfFinitePresentation. Nothing about Ri_*E beyond its being an object of D(𝒪_P) is used, and in particular no hypothesis on i is needed.

public theorem derivedPushforwardRelative_iff_pseudoCoherentFrom {X P S : Scheme.{u}} (i : X ⟶ P)
    (p : P ⟶ S) [Flat p] [LocallyOfFinitePresentation p] (E : DerivedCategory X.Modules)
    (m : ℤ) :
    p.IsPseudoCoherentFrom
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward
          i.toLRSHom.toShHom).obj E) m ↔
      RingedSpace.IsPseudoCoherentFrom (X := P.toRingedSpace)
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward
          i.toLRSHom.toShHom).obj E) m

Sources

LeanAlgebraicGeometry.Scheme.Modules.isPseudoCoherentFrom_some_iff_forall_fin · AlgebraicGeometry.Scheme.Hom.IsPseudoCoherentFrom · AlgebraicGeometry.Scheme.Hom.IsPseudoCoherent · AlgebraicGeometry.Scheme.Hom.IsModulePseudoCoherentFrom · AlgebraicGeometry.Scheme.Hom.IsModulePseudoCoherent · AlgebraicGeometry.Scheme.Hom.isQuasicoherent_homology_of_isPseudoCoherentFrom · AlgebraicGeometry.Scheme.Hom.isQuasicoherentDerived_of_isPseudoCoherent · AlgebraicGeometry.Scheme.Modules.isPseudoCoherentFromAfterPushforward_restrict

Section37.60 Pseudo-coherent morphisms #

Section 37.60 of the Stacks Project, Tag 067X. 13 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 067Y, a lemma

Tag 067Y in the Stacks Project.

AlgebraicGeometry.pseudoCoherent_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/PseudoCoherent.lean, line 114. The attribute's comment: “the equivalence of (1) and (2)”.

For a morphism of schemes the following are equivalent: there is an affine open cover of the base and, over each of its members, an affine open cover of its inverse image on which the maps on sections are pseudo-coherent ring maps; and every compatible pair of affine opens has pseudo-coherent map on sections.

public theorem pseudoCoherent_tfae {X S : Scheme.{u}} (f : X ⟶ S) :
    let pseudoCoherentOn := fun (V : S.Opens) (U : X.Opens)
        (h : U ≤ f ⁻¹ᵁ V) ↦
      letI : Algebra Γ(S, V) Γ(X, U) := (f.appLE V U h).hom.toAlgebra
      Algebra.PseudoCoherent Γ(S, V) Γ(X, U)
    List.TFAE [
      ∃ (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, pseudoCoherentOn (V j) (U i)
                ((le_iSup U i).trans hU.le),
      ∀ (U : X.Opens), IsAffineOpen U →
        ∀ (V : S.Opens), IsAffineOpen V →
          ∀ (h : U ≤ f ⁻¹ᵁ V), pseudoCoherentOn V U h]

AlgebraicGeometry.locallyOfFinitePresentation_of_pseudoCoherent, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/PseudoCoherent.lean, line 162. The attribute's comment: “condition (2) implies the finite-type half of condition (3)”.

Stacks 0682. A pseudo-coherent morphism of schemes is locally of finite presentation.

On every compatible pair of affine opens the map on sections is a pseudo-coherent ring map, hence of finite presentation by RingHom.PseudoCoherent.finitePresentation.

Followed by Mathlib's instance from AlgebraicGeometry.LocallyOfFinitePresentation to AlgebraicGeometry.LocallyOfFiniteType, this is how type class search finds that a pseudo-coherent morphism is locally of finite type, the clause of Stacks 067Y recorded by the second tag.

public instance (priority := 100) locallyOfFinitePresentation_of_pseudoCoherent {X S : Scheme.{u}}
    (f : X ⟶ S) [hf : PseudoCoherent f] : LocallyOfFinitePresentation f

AlgebraicGeometry.pseudoCoherent_tfae_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/StructureSheafComparison.lean, line 442. The attribute's comment: “the full three-condition equivalence”.

Stacks 067Y. For a morphism of schemes f : X ⟶ S the following are equivalent: there are an affine open covering of S and, over each of its members, an affine open covering of its inverse image on which the maps on sections are pseudo-coherent ring maps; the map on sections is pseudo-coherent at every compatible pair of affine opens; and f is locally of finite type with 𝒪_X pseudo-coherent relative to S.

The equivalence of the first two conditions is AlgebraicGeometry.pseudoCoherent_tfae, and the third enters through AlgebraicGeometry.relativeStructureSheafComparison. This declaration states the whole of the source's lemma, so it subsumes the two clauses of it tagged in StacksFrontier/AlgebraicGeometry/Morphisms/PseudoCoherent.lean.

public theorem pseudoCoherent_tfae_three :
    let pseudoCoherentOn := fun (V : S.Opens) (U : X.Opens)
        (h : U ≤ f ⁻¹ᵁ V) ↦
      letI : Algebra Γ(S, V) Γ(X, U) := (f.appLE V U h).hom.toAlgebra
      Algebra.PseudoCoherent Γ(S, V) Γ(X, U)
    List.TFAE [
      ∃ (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, pseudoCoherentOn (V j) (U i)
                ((le_iSup U i).trans hU.le),
      ∀ (U : X.Opens), IsAffineOpen U →
        ∀ (V : S.Opens), IsAffineOpen V →
          ∀ (h : U ≤ f ⁻¹ᵁ V), pseudoCoherentOn V U h,
      ∃ hft : LocallyOfFiniteType f,
        letI := hft
        Scheme.Hom.IsModulePseudoCoherent f (SheafOfModules.unit X.ringCatSheaf)]

Tag 067Z, a definition

Tag 067Z in the Stacks Project.

AlgebraicGeometry.PseudoCoherent, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/PseudoCoherent.lean, line 71.

A morphism of schemes f : X ⟶ S is pseudo-coherent if for every affine open V ⊆ S and every affine open U ⊆ X with U ⊆ f ⁻¹ᵁ V the induced map on sections Γ(S, V) ⟶ Γ(X, U) is a pseudo-coherent ring map.

public class PseudoCoherent {X S : Scheme.{u}} (f : X ⟶ S) : Prop

Tag 0680, a lemma

Tag 0680 in the Stacks Project.

AlgebraicGeometry.pseudoCoherent_of_isPullback_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentMorphism/FlatBaseChange.lean, line 160.

Stacks 0680. A flat base change of a pseudo-coherent morphism of schemes is pseudo-coherent: if f : X ⟶ S is pseudo-coherent, g : S' ⟶ S is flat and the square with sides g' : X' ⟶ X and f' : X' ⟶ S' is cartesian, then f' is pseudo-coherent.

theorem pseudoCoherent_of_isPullback_of_flat {X X' S S' : Scheme.{u}} {f : X ⟶ S} {g : S' ⟶ S}
    {g' : X' ⟶ X} {f' : X' ⟶ S'} (sq : IsPullback g' f' f g) [Flat g] [PseudoCoherent f] :
    PseudoCoherent f'

Tag 0681, a lemma

Tag 0681 in the Stacks Project.

AlgebraicGeometry.pseudoCoherent_comp, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentMorphism/Composition.lean, line 82.

Stacks 0681. A composition of pseudo-coherent morphisms of schemes is pseudo-coherent.

instance pseudoCoherent_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    [hf : PseudoCoherent f] [hg : PseudoCoherent g] : PseudoCoherent (f ≫ g)

Tag 0682, a lemma

Tag 0682 in the Stacks Project.

AlgebraicGeometry.locallyOfFinitePresentation_of_pseudoCoherent, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/PseudoCoherent.lean, line 162.

Stacks 0682. A pseudo-coherent morphism of schemes is locally of finite presentation.

On every compatible pair of affine opens the map on sections is a pseudo-coherent ring map, hence of finite presentation by RingHom.PseudoCoherent.finitePresentation.

Followed by Mathlib's instance from AlgebraicGeometry.LocallyOfFinitePresentation to AlgebraicGeometry.LocallyOfFiniteType, this is how type class search finds that a pseudo-coherent morphism is locally of finite type, the clause of Stacks 067Y recorded by the second tag.

public instance (priority := 100) locallyOfFinitePresentation_of_pseudoCoherent {X S : Scheme.{u}}
    (f : X ⟶ S) [hf : PseudoCoherent f] : LocallyOfFinitePresentation f

Tag 0695, a lemma

Tag 0695 in the Stacks Project.

AlgebraicGeometry.pseudoCoherent_of_flat_of_locallyOfFinitePresentation, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentMorphism/FinitePresentation.lean, line 57.

Stacks 0695. A flat morphism of schemes which is locally of finite presentation is pseudo-coherent.

On every compatible pair of affine opens the map on sections is flat and of finite presentation, hence pseudo-coherent by RingHom.PseudoCoherent.of_flat_of_finitePresentation, the pseudo-coherence half of Stacks 067J.

instance pseudoCoherent_of_flat_of_locallyOfFinitePresentation {X S : Scheme.{u}} (f : X ⟶ S)
    [Flat f] [LocallyOfFinitePresentation f] : PseudoCoherent f

Tag 0683, a lemma

Tag 0683 in the Stacks Project.

AlgebraicGeometry.pseudoCoherent_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentMorphism/Composition.lean, line 95. References: SGA 6 III (1.14), “special case”.

Stacks 0683. If X and Y are pseudo-coherent over a base scheme S, then any morphism f : X ⟶ Y over S is pseudo-coherent.

Pseudo-coherence of f is checked around a point x of X on an affine open U ∋ x of X contained in the preimage of an affine open V of Y, itself contained in the preimage of an affine open W of S. The map Γ(S, W) ⟶ Γ(X, U) is the composite of Γ(S, W) ⟶ Γ(Y, V) with Γ(Y, V) ⟶ Γ(X, U), and the outer two are pseudo-coherent by hypothesis, so the algebra cancellation lemma applies.

theorem pseudoCoherent_of_comp {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
    [PseudoCoherent (f ≫ g)] [PseudoCoherent g] : PseudoCoherent f

Tag 0AVX, a lemma

Tag 0AVX in the Stacks Project.

AlgebraicGeometry.Scheme.isPseudoCoherentSite_pushforward_derivedStructureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointLemmas/ExactSupportSitePseudoCoherent.lean, line 55. The attribute's comment: “for a closed immersion, at the site notion of pseudo-coherence”.

If a closed immersion of schemes i : Z ⟶ X is pseudo-coherent, then Ri_* 𝒪_Z is a pseudo-coherent object of D(𝒪_X) at the ringed site of opens of X, in the sense of [Stacks, Tag 08FT].

theorem isPseudoCoherentSite_pushforward_derivedStructureSheaf (hi : PseudoCoherent i) :
    (Stacks.SheafOfModules.ringedSite X.sheaf).IsPseudoCoherent
      ((modulePushforward
        (Stacks.ClosedImmersion.closedQuotientOfClosedImmersion i).i).mapDerivedCategory.obj
          (RingedSite.derivedStructureSheaf (Stacks.SheafOfModules.ringedSite Z.sheaf)))

AlgebraicGeometry.pseudoCoherent_iff_isPseudoCoherent_pushforward_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentMorphism/FiniteMorphism.lean, line 144.

Stacks 0AVX. A finite morphism of schemes f : X ⟶ S is pseudo-coherent if and only if the direct image f_*𝒪_X of its structure sheaf is a pseudo-coherent 𝒪_S-module, that is, if and only if the object of D(𝒪_S) it determines in degree zero is pseudo-coherent.

public theorem pseudoCoherent_iff_isPseudoCoherent_pushforward_unit {X S : Scheme.{u}} (f : X ⟶ S)
    [IsFinite f] :
    PseudoCoherent f ↔
      RingedSpace.IsPseudoCoherent (X := S.toRingedSpace)
        ((DerivedCategory.singleFunctor S.Modules 0).obj
          ((Scheme.Modules.pushforward f).obj (SheafOfModules.unit X.ringCatSheaf)))

Tag 0684, a lemma

Tag 0684 in the Stacks Project.

AlgebraicGeometry.pseudoCoherent_iff_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentMorphism/Noetherian.lean, line 76. References: SGA 6 III (1.3), “loc. noetherian case”.

Stacks 0684. A morphism of schemes whose target is locally Noetherian is pseudo-coherent if and only if it is locally of finite type.

A pseudo-coherent morphism is always locally of finite type. Conversely, over a locally Noetherian base the sections over an affine open form a Noetherian ring, so every map on sections over a compatible pair of affine opens is a finite-type ring map out of a Noetherian ring, hence pseudo-coherent by Stacks 067I.

theorem pseudoCoherent_iff_locallyOfFiniteType {X S : Scheme.{u}} [IsLocallyNoetherian S]
    (f : X ⟶ S) : PseudoCoherent f ↔ LocallyOfFiniteType f

Tag 0696, a lemma

Tag 0696 in the Stacks Project.

AlgebraicGeometry.pseudoCoherent_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentMorphism/FpqcLocalAtTarget.lean, line 347.

Stacks 0696. Pseudo-coherence of a morphism of schemes is fpqc local on the base: a morphism is pseudo-coherent if and only if its base change along every member of an fpqc covering of its target is pseudo-coherent.

Both implications are part of CategoryTheory.MorphismProperty.IsLocalAtTarget; they are spelled out as a single Iff by AlgebraicGeometry.pseudoCoherent_iff_of_fpqcCover.

instance pseudoCoherent_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@PseudoCoherent : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 0697, a lemma

Tag 0697 in the Stacks Project.

Algebra.pseudoCoherent_quotient_iff_isModulePseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/PseudoCoherentMap/Quotient.lean, line 123.

Stacks 0697. Let A → B be a flat ring map of finite presentation and let I be an ideal of B. Then A → B ⧸ I is pseudo-coherent if and only if I is pseudo-coherent as a B-module.

Pseudo-coherence of A → B ⧸ I is pseudo-coherence of B ⧸ I relative to A; Stacks 0673 restricts that along the finite map B → B ⧸ I, Stacks 0DHQ makes it absolute over B because A → B is itself pseudo-coherent by Stacks 067J, and Stacks 064V exchanges B ⧸ I for I.

theorem pseudoCoherent_quotient_iff_isModulePseudoCoherent
    {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] [Module.Flat A B]
    [Algebra.FinitePresentation A B] (I : Ideal B) :
    Algebra.PseudoCoherent A (B ⧸ I) ↔ IsModulePseudoCoherent (R := B) I

Tag 0698, a lemma

Tag 0698 in the Stacks Project.

AlgebraicGeometry.PseudoCoherent.isLocalAtSource_syntomicPrecoverage, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentMorphism/SyntomicDescent.lean, line 79.

Stacks 0698. Pseudo-coherence of morphisms of schemes is local on the source for the syntomic topology.

This is AlgebraicGeometry.pseudoCoherent_isLocalAtSource_of_affine_descent, the reduction of the source's statement to the case of a surjective syntomic morphism of affine schemes, with that case discharged by AlgebraicGeometry.pseudoCoherent_of_comp_surjective_syntomic_of_isAffine.

instance PseudoCoherent.isLocalAtSource_syntomicPrecoverage :
    MorphismProperty.IsLocalAtSource (@PseudoCoherent.{u} : MorphismProperty Scheme.{u})
      (Scheme.precoverage (@Syntomic.{u}))

Tag 0699, a lemma

Tag 0699 in the Stacks Project.

AlgebraicGeometry.PseudoCoherent.isLocalAtSource_fppfPrecoverage, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentMorphism/FppfDescent.lean, line 56.

Stacks 0699. Pseudo-coherence of morphisms of schemes is local on the source for the fppf topology: a morphism is pseudo-coherent exactly when its composites with the members of an fppf covering of its source are.

This is AlgebraicGeometry.pseudoCoherent_isLocalAtSource_fppf_of_finiteLocallyFree_descent, the reduction of the source's statement to descent along a surjective finite locally free morphism, with that descent discharged by AlgebraicGeometry.pseudoCoherent_of_comp_surjective_finiteLocallyFree.

instance PseudoCoherent.isLocalAtSource_fppfPrecoverage :
    MorphismProperty.IsLocalAtSource (@PseudoCoherent.{u} : MorphismProperty Scheme.{u})
      Scheme.fppfPrecoverage

Sources

LeanAlgebraicGeometry.pseudoCoherent_tfae · AlgebraicGeometry.locallyOfFinitePresentation_of_pseudoCoherent · AlgebraicGeometry.pseudoCoherent_tfae_three · AlgebraicGeometry.PseudoCoherent · AlgebraicGeometry.pseudoCoherent_of_isPullback_of_flat · AlgebraicGeometry.pseudoCoherent_comp · AlgebraicGeometry.pseudoCoherent_of_flat_of_locallyOfFinitePresentation · AlgebraicGeometry.pseudoCoherent_of_comp

Section37.61 Perfect morphisms #

Section 37.61 of the Stacks Project, Tag 0685. 15 tags here are carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0685, the section

Tag 0685 in the Stacks Project.

AlgebraicGeometry.locallyOfFinitePresentation_of_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PerfectMorphism/Flat.lean, line 73. The attribute's comment: “the section's unnumbered assertion that a perfect morphism is pseudo-coherent, hence locally of finite presentation; the fifteen numbered items of the section carry their own tags”.

Stacks 0685. A perfect morphism of schemes is locally of finite presentation: it is pseudo-coherent, and a pseudo-coherent morphism is locally of finite presentation by Stacks 0682.

public theorem locallyOfFinitePresentation_of_perfect {X S : Scheme.{u}} (f : X ⟶ S)
    [Perfect f] : LocallyOfFinitePresentation f

Tag 0686, a lemma

Tag 0686 in the Stacks Project.

AlgebraicGeometry.exists_affine_openCover_perfect_iff_forall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PerfectMorphism/AffineLocal.lean, line 554.

For a locally finite type morphism of schemes, perfectness on some affine open covering of the target and affine open coverings of its preimages is equivalent to perfectness on every pair of affine opens for which the source open maps into the target open.

theorem exists_affine_openCover_perfect_iff_forall
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] :
    (∃ (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 g := (f.appLE (V j) (U i) ((le_iSup U i).trans hU.le)).hom
              letI := g.toAlgebra
              ∀ D : CertifiedDerivedTensoring Γ(S, V j),
                RingHom.IsPerfectRingMap Γ(S, V j) Γ(X, U i)
                  D.tensor D.comparison D.isLeftDerived) ↔
      ∀ (U : X.Opens) (_ : IsAffineOpen U) (V : S.Opens) (_ : IsAffineOpen V)
        (hUV : U ≤ f ⁻¹ᵁ V),
          let g := (f.appLE V U hUV).hom
          letI := g.toAlgebra
          ∀ D : CertifiedDerivedTensoring Γ(S, V),
            RingHom.IsPerfectRingMap Γ(S, V) Γ(X, U)
              D.tensor D.comparison D.isLeftDerived

Tag 0687, a definition

Tag 0687 in the Stacks Project.

AlgebraicGeometry.Perfect, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/Morphism.lean, line 70.

Stacks 0687. A morphism of schemes f : X ⟶ S is perfect if it is locally of finite type and, for every affine open U ⊆ X and every affine open V ⊆ S with U ⊆ f ⁻¹ᵁ V, the induced map on sections Γ(S, V) ⟶ Γ(X, U) is a perfect ring map, with respect to every certified derived tensor product on Γ(S, V).

This is condition (2) of Stacks 0686, which is the condition Stacks 0687 defines perfectness by.

public class Perfect {X S : Scheme.{u}} (f : X ⟶ S) : Prop extends LocallyOfFiniteType f

Tag 0688, a lemma

Tag 0688 in the Stacks Project.

AlgebraicGeometry.perfect_of_isPullback_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PerfectMorphism/FlatBaseChange.lean, line 164.

Stacks 0688. A flat base change of a perfect morphism of schemes is perfect: if f : X ⟶ S is perfect, g : S' ⟶ S is flat and the square with sides g' : X' ⟶ X and f' : X' ⟶ S' is cartesian, then f' is perfect.

theorem perfect_of_isPullback_of_flat {X X' S S' : Scheme.{u}} {f : X ⟶ S} {g : S' ⟶ S}
    {g' : X' ⟶ X} {f' : X' ⟶ S'} (sq : IsPullback g' f' f g) [Flat g] [Perfect f] :
    Perfect f'

Tag 0689, a lemma

Tag 0689 in the Stacks Project.

AlgebraicGeometry.perfect_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PerfectMorphism/Composition.lean, line 146.

Stacks Project, Tag 0689. A composition of perfect morphisms of schemes is perfect.

public theorem perfect_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    [Perfect f] [Perfect g] : Perfect (f ≫ g)

Tag 068A, a lemma

Tag 068A in the Stacks Project.

AlgebraicGeometry.flat_and_perfect_iff_flat_and_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PerfectMorphism/Flat.lean, line 99.

Stacks 068A. A morphism of schemes is flat and perfect if and only if it is flat and locally of finite presentation.

Neither implication uses flatness on the side it starts from: a perfect morphism is always locally of finite presentation, through AlgebraicGeometry.pseudoCoherent_of_perfect and Stacks 0682, and a flat morphism locally of finite presentation is always perfect, through AlgebraicGeometry.perfect_of_flat_of_locallyOfFinitePresentation.

public theorem flat_and_perfect_iff_flat_and_locallyOfFinitePresentation {X S : Scheme.{u}}
    (f : X ⟶ S) : (Flat f ∧ Perfect f) ↔ (Flat f ∧ LocallyOfFinitePresentation f)

Tag 068B, a lemma

Tag 068B in the Stacks Project.

AlgebraicGeometry.perfect_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PerfectMorphism/RegularTarget.lean, line 54.

Stacks 068B. A morphism of schemes locally of finite type over a regular scheme is perfect.

public theorem perfect_of_isRegular {X S : Scheme.{u}} (f : X ⟶ S) (hS : IsRegular S)
    [LocallyOfFiniteType f] : Perfect f

Tag 068C, a lemma

Tag 068C in the Stacks Project.

AlgebraicGeometry.perfect_of_isKoszulRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PerfectMorphism/RegularImmersion.lean, line 200. The attribute's comment: “Koszul-regular immersion”. References: SGA 6 III (4.1.1), “reg. immersion perfect”; SGA 6 III (1.1.2); SGA 6 VII (1.9), “more general”; SGA 6 VIII (1.7), “special case”; SGA 6 X (7.1), “partial”.

Stacks 068C. A Koszul-regular immersion of schemes is a perfect morphism.

The immersion factors as its closed factor into the canonical open, whose defining ideal sheaf is Koszul-regular by definition, followed by an open immersion, which is flat and locally of finite presentation and hence perfect by Stacks 068A; perfectness composes by Stacks 0689.

theorem perfect_of_isKoszulRegularImmersion {X S : Scheme.{u}} (i : X ⟶ S) [IsImmersion i]
    (hi : IsKoszulRegularImmersion i) : Perfect i

AlgebraicGeometry.perfect_of_isRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PerfectMorphism/RegularImmersion.lean, line 213. The attribute's comment: “regular immersion”. References: SGA 6 III (4.1.1), “reg. immersion perfect”; SGA 6 III (1.1.2); SGA 6 VIII (1.7), “special case”; SGA 6 X (7.1), “partial”.

Stacks 068C. A regular immersion of schemes is a perfect morphism, because a regular immersion is Koszul-regular by Stacks 063K.

theorem perfect_of_isRegularImmersion {X S : Scheme.{u}} (i : X ⟶ S) [IsImmersion i]
    (hi : IsRegularImmersion i) : Perfect i

Tag 068D, a lemma

Tag 068D in the Stacks Project.

AlgebraicGeometry.perfect_of_comp_eq_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PerfectMorphism/SmoothTarget.lean, line 68.

Stacks 068D. In a commutative triangle of morphisms of schemes with f ≫ q = p, q smooth and p perfect, the morphism f is perfect.

public theorem perfect_of_comp_eq_of_smooth {X Y S : Scheme.{u}} (f : X ⟶ Y) (q : Y ⟶ S)
    {p : X ⟶ S} (hfq : f ≫ q = p) [Smooth q] [Perfect p] : Perfect f

Tag 069B, a lemma

Tag 069B in the Stacks Project.

AlgebraicGeometry.perfect_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PerfectMorphism/FpqcLocalAtTarget.lean, line 457. References: SGA 6 IV (3.1.1), “special case”.

Stacks 069B. Perfectness of a morphism of schemes is fpqc local on the base: a morphism is perfect if and only if its base change along every member of an fpqc covering of its target is perfect.

Both implications are part of CategoryTheory.MorphismProperty.IsLocalAtTarget; they are spelled out as a single Iff by AlgebraicGeometry.perfect_iff_of_fpqcCover.

public instance perfect_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@Perfect.{u}) Scheme.fpqcPrecoverage

Tag 069C, a lemma

Tag 069C in the Stacks Project.

AlgebraicGeometry.perfect_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PerfectMorphism/RelativeTorDimensionClause.lean, line 231.

Let f : X ⟶ S be a pseudo-coherent morphism of schemes. The following are equivalent: 1. f is perfect; 2. 𝒪_X locally has finite Tor dimension as a sheaf of f^{-1}𝒪_S-modules, that is, the restriction of scalars of 𝒪_X[0] along f^{-1}𝒪_S ⟶ 𝒪_X locally has finite Tor dimension on the inverse-image ringed space (X, f^{-1}𝒪_S), at the derived tensor product; 3. for every x ∈ X the local ring 𝒪_{X, x} has finite Tor dimension as an 𝒪_{S, f x}-module through the stalk map of f.

theorem perfect_tfae {X S : Scheme.{u}} (f : X ⟶ S) [PseudoCoherent f] :
    List.TFAE
      [Perfect f,
        Stacks.Cohomology.TorAmplitude.LocallyHasFiniteTorDimension
          (RingedSpace.inverseImage S.toRingedSpace f.base)
          ((derivedScalarRestriction f).obj
            ((DerivedCategory.singleFunctor (OXMod.{u, u} X.toRingedSpace) 0).obj
              (structureModule X.toRingedSpace))),
        ∀ x : X,
          let _ : Algebra (S.presheaf.stalk (f.base x)) (X.presheaf.stalk x) :=
            (f.stalkMap x).hom.toAlgebra
          HasFiniteTorDimensionCanonical (S.presheaf.stalk (f.base x))
            ((DerivedCategory.singleFunctor (ModuleCat.{u} (S.presheaf.stalk (f.base x))) 0).obj
              (ModuleCat.of (S.presheaf.stalk (f.base x)) (X.presheaf.stalk x)))]

Tag 0G2E, a lemma

Tag 0G2E in the Stacks Project.

AlgebraicGeometry.isPerfect_pushforward_structureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PerfectClosedImmersion.lean, line 359.

Stacks 0G2E. If i : Z ⟶ X is a perfect closed immersion of schemes then i_*𝒪_Z is a perfect 𝒪_X-module, that is, a perfect object of the derived category of 𝒪_X-modules.

theorem isPerfect_pushforward_structureSheaf {Z X : Scheme.{u}} (i : Z ⟶ X)
    [IsClosedImmersion i] [Perfect i]
    [HasDerivedCategory.{d} (OXMod.{u, u} X.toRingedSpace)] :
    RingedSpace.IsPerfect
      ((DerivedCategory.singleFunctor (OXMod.{u, u} X.toRingedSpace) 0).obj
        ((Scheme.Modules.pushforward i).obj (SheafOfModules.unit Z.ringCatSheaf)))

Tag 0B6G, a lemma

Tag 0B6G in the Stacks Project.

Stacks.AlgebraicGeometry.PerfectProperDirectImage.isPerfect_derivedPushforward_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PerfectMorphism/MayerVietorisTorDimension.lean, line 393. References: SGA 6 0 (3.1), “special case”; SGA 6 0 (4.1); SGA 6 III (4.8.1), “special case”; SGA 6 IV (2.12), “special case”; SGA 6 IV (3.3.2), “3.3.2.3, special case”; SGA 6 XIV (2.2), “special case”.

[Stacks, Tag 0B6G]. Let S be a Noetherian scheme, let f : X ⟶ S be a perfect proper morphism of schemes and let E be a perfect object of D(𝒪_X). Then Rf_*E is a perfect object of D(𝒪_S).

By [Stacks, Tag 08CQ] perfectness is pseudo-coherence together with locally finite Tor dimension. Pseudo-coherence is isPseudoCoherent_derivedPushforward_of_isPerfect, and the Tor-dimension half is hasFiniteTorDimension_derivedPushforward_affineOpen fed into isPerfect_derivedPushforward_of_isPerfect_of_forall_affineOpen. Nothing is assumed beyond the source's own hypotheses.

theorem isPerfect_derivedPushforward_of_isPerfect {X S : Scheme.{u}} (f : X ⟶ S)
    [IsNoetherian S] [Perfect f] [IsProper f] (E : DerivedCategory X.Modules)
    (hE : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E) :
    Stacks.Cohomology.PerfectComplexes.IsPerfect (X := S.toRingedSpace)
      ((derivedPushforwardModules f).obj E)

Stacks.AlgebraicGeometry.PerfectProperDirectImage.isPseudoCoherent_derivedPushforward_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PerfectMorphism/ProperDirectImage.lean, line 218. The attribute's comment: “the pseudo-coherence half of the conclusion: Rf_*E is a pseudo-coherent object of D(𝒪_S), proved under the source's own hypotheses and no others”. References: SGA 6 0 (3.1), “partial”; SGA 6 XIV (2.2), “special case”.

[Stacks, Tag 0B6G], the pseudo-coherence half of the conclusion, with no hypothesis. Let S be a Noetherian scheme, let f : X ⟶ S be a perfect proper morphism of schemes and let E be a perfect object of D(𝒪_X). Then Rf_*E is a pseudo-coherent object of D(𝒪_S).

By [Stacks, Tag 08CQ] perfectness is pseudo-coherence together with locally finite Tor dimension; this is the first of the two. The hypotheses the pseudo-coherence half of [Stacks, Tag 08EV] makes of E are supplied by isCoherent_homology_and_bounds_of_isPerfect, and its support hypothesis by the fact that every closed subset of the source of a proper morphism is proper over the target. The hypothesis that half carries for [Stacks, Tag 02O5] is supplied by the proof of [Stacks, Tag 02O5] in this tree, AlgebraicGeometry.ProperCoherenceWitness.higherDirectImageIsCoherentOverAffineBase, so it is not assumed here.

theorem isPseudoCoherent_derivedPushforward_of_isPerfect [IsNoetherian S]
    [AlgebraicGeometry.Perfect f] [IsProper f] (E : DerivedCategory X.Modules)
    (hE : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E) :
    AlgebraicGeometry.RingedSpace.IsPseudoCoherent (X := S.toRingedSpace)
      ((derivedPushforwardModules f).obj E)

Tag 069D, a lemma

Tag 069D in the Stacks Project.

AlgebraicGeometry.Perfect.isLocalAtSource_fppfPrecoverage, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PerfectMorphism/FppfDescent.lean, line 84.

Perfectness of morphisms of schemes is local on the source for the fppf topology: a morphism is perfect exactly when its composites with the members of an fppf covering of its source are.

instance Perfect.isLocalAtSource_fppfPrecoverage :
    MorphismProperty.IsLocalAtSource (@Perfect.{u} : MorphismProperty Scheme.{u})
      Scheme.fppfPrecoverage

Tag 09RK, a lemma

Tag 09RK in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.isRegularImmersion_of_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/PerfectFactor.lean, line 485. The attribute's comment: “i is a regular immersion”.

Stacks tag 09RK for the inner factor. Let i : Z ⟶ Y and j : Y ⟶ X be immersions of schemes with X locally Noetherian and i perfect. If the composite i ≫ j is a regular immersion, then i is a regular immersion.

theorem isRegularImmersion_of_perfect (hji : IsRegularImmersion (i ≫ j)) :
    IsRegularImmersion i

Stacks.AlgebraicGeometry.RegularIdealSheaf.exists_opens_isRegularImmersion_comp_of_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/PerfectFactor.lean, line 510. The attribute's comment: “j is a regular immersion near the image of i”.

Stacks tag 09RK for the outer factor, in its neighbourhood form — the corrected statement of a Stacks erratum. Under the same hypotheses there is an open V ⊆ Y containing the image of i such that the immersion V.ι ≫ j of that open subscheme into X is regular.

The source concludes instead that j itself is a regular immersion, and that is false. Over a field k, take Z = Spec k, Y = Spec k ⊔ Spec k, X = Spec k ⊔ Spec k[ε]/(ε²), let i be the inclusion of the first component of Y, and let j be the identity on the first component and the reduced point Spec k ↪ Spec k[ε]/(ε²) on the second. All three hypotheses hold: X is the spectrum of the Noetherian ring k × k[ε]/(ε²), and i and i ≫ j are inclusions of a component, hence open immersions, hence regular immersions, so i is perfect. Yet j is not a regular immersion: on the second component its ideal is (ε) ⊆ k[ε]/(ε²), and no weakly regular sequence generates it, since every element of (ε) kills ε ≠ 0. This is Stacks.Examples.not_forall_isRegularImmersion_of_perfect_of_isRegularImmersion_comp.

The hypotheses control j only at the points of i(Z) — in the example the first component, where j is an isomorphism — and the neighbourhood form below is exactly what the source's own local-ring argument supplies. See also the implementation notes of this file.

theorem exists_opens_isRegularImmersion_comp_of_perfect (hji : IsRegularImmersion (i ≫ j)) :
    ∃ V : Y.Opens, (∀ z : Z, i.base z ∈ V) ∧ IsRegularImmersion (V.ι ≫ j)

Sources

LeanAlgebraicGeometry.locallyOfFinitePresentation_of_perfect · AlgebraicGeometry.exists_affine_openCover_perfect_iff_forall · AlgebraicGeometry.Perfect · AlgebraicGeometry.perfect_of_isPullback_of_flat · AlgebraicGeometry.perfect_comp · AlgebraicGeometry.flat_and_perfect_iff_flat_and_locallyOfFinitePresentation · AlgebraicGeometry.perfect_of_isRegular · AlgebraicGeometry.perfect_of_isKoszulRegularImmersion

Section37.62 Local complete intersection morphisms #

Section 37.62 of the Stacks Project, Tag 068E. 23 tags here are carried by 42 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 069E, a lemma

Tag 069E in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.exists_opens_isKoszulRegularImmersion_comp_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/SmoothEmbeddingIndependence.lean, line 81.

Stacks 069E. Let i : U ⟶ P and i' : U ⟶ P' be immersions over S of schemes smooth over S. Then i is a Koszul-regular immersion in a neighbourhood of u : U if and only if i' is.

theorem exists_opens_isKoszulRegularImmersion_comp_iff
    {S U P P' : Scheme.{u}} (f : U ⟶ S) (p : P ⟶ S) (p' : P' ⟶ S)
    (i : U ⟶ P) (i' : U ⟶ P') [IsImmersion i] [IsImmersion i'] [Smooth p] [Smooth p']
    (hi : i ≫ p = f) (hi' : i' ≫ p' = f) (u : U) :
    (∃ V : U.Opens, u ∈ V ∧ IsKoszulRegularImmersion (V.ι ≫ i)) ↔
      ∃ V : U.Opens, u ∈ V ∧ IsKoszulRegularImmersion (V.ι ≫ i')

Tag 069F, a definition

Tag 069F in the Stacks Project.

AlgebraicGeometry.KoszulAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/Defs.lean, line 66. The attribute's comment: “part (1): Koszul at a point”. References: SGA 6 VIII (1.1), “at a point”.

Stacks 069F, part (1). A morphism of schemes f : X ⟶ S is Koszul at x : X if it is of finite type at x and there are an open neighbourhood U of x, a scheme P smooth over S and a Koszul-regular immersion i : U ⟶ P through which the restriction of f to U factors.

def KoszulAt {X S : Scheme.{u}} (f : X ⟶ S) (x : X) : Prop

AlgebraicGeometry.IsLocalCompleteIntersectionMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/Defs.lean, line 76. The attribute's comment: “part (2): local complete intersection morphism”. References: SGA 6 VIII (1.1).

Stacks 069F, part (2). A local complete intersection morphism, also called a Koszul morphism, is a morphism of schemes that is Koszul at every point of its source.

def IsLocalCompleteIntersectionMorphism {X S : Scheme.{u}} (f : X ⟶ S) : Prop

Tag 069G, a lemma

Tag 069G in the Stacks Project.

AlgebraicGeometry.isKoszulRegularImmersion_of_koszul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/LocalCompleteIntersectionAffine.lean, line 129. References: SGA 6 VIII (1.2).

Stacks 069G, unconditionally: an immersion over S of an open of the source of a local complete intersection morphism into a scheme smooth over S is Koszul-regular.

theorem isKoszulRegularImmersion_of_koszul {X S P : Scheme.{u}} (f : X ⟶ S) (π : P ⟶ S)
    [Smooth π] (U : X.Opens) (i : U.toScheme ⟶ P) [IsImmersion i]
    (hf : IsLocalCompleteIntersectionMorphism f) (hi : U.ι ≫ f = i ≫ π) :
    IsKoszulRegularImmersion i

Tag 069H, a lemma

Tag 069H in the Stacks Project.

AlgebraicGeometry.perfect_of_isLocalCompleteIntersectionMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/Perfect.lean, line 146. The attribute's comment: “part (3): perfect”. References: SGA 6 III (4.1.1); SGA 6 VIII (1.7); SGA 6 X (7.1), “partial”.

Stacks 069H, part (3). A local complete intersection morphism of schemes is perfect.

Perfectness is Zariski-local on the source, and on a neighbourhood of each point the morphism factors as a Koszul-regular immersion followed by a smooth morphism; the first is perfect by Stacks 068C, the second is flat and locally of finite presentation and hence perfect by Stacks 068A, and perfectness is stable under composition by Stacks 0689.

theorem perfect_of_isLocalCompleteIntersectionMorphism {X S : Scheme.{u}} {f : X ⟶ S}
    (hf : IsLocalCompleteIntersectionMorphism f) : Perfect f

AlgebraicGeometry.pseudoCoherent_of_isLocalCompleteIntersectionMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/Perfect.lean, line 161. The attribute's comment: “part (2): pseudo-coherent”. References: SGA 6 VIII (1.7), “partial”.

Stacks 069H, part (2). A local complete intersection morphism of schemes is pseudo-coherent, because it is perfect and a perfect morphism is pseudo-coherent.

theorem pseudoCoherent_of_isLocalCompleteIntersectionMorphism {X S : Scheme.{u}} {f : X ⟶ S}
    (hf : IsLocalCompleteIntersectionMorphism f) : PseudoCoherent f

AlgebraicGeometry.locallyOfFinitePresentation_of_isLocalCompleteIntersectionMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/Perfect.lean, line 170. The attribute's comment: “part (1): locally of finite presentation”.

Stacks 069H, part (1). A local complete intersection morphism of schemes is locally of finite presentation, because it is pseudo-coherent and a pseudo-coherent morphism is locally of finite presentation by Stacks 0682.

theorem locallyOfFinitePresentation_of_isLocalCompleteIntersectionMorphism
    {X S : Scheme.{u}} {f : X ⟶ S}
    (hf : IsLocalCompleteIntersectionMorphism f) : LocallyOfFinitePresentation f

Tag 07DB, a lemma

Tag 07DB in the Stacks Project.

AlgebraicGeometry.isLocalCompleteIntersectionMorphism_iff_appTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/Affine.lean, line 537.

Stacks 07DB. A morphism of affine schemes is a local complete intersection morphism exactly when the induced homomorphism of the rings of global sections is a local complete intersection homomorphism.

theorem isLocalCompleteIntersectionMorphism_iff_appTop {X S : Scheme.{u}} [IsAffine X]
    [IsAffine S] (f : X ⟶ S) :
    IsLocalCompleteIntersectionMorphism f ↔ f.appTop.hom.IsLocalCompleteIntersection

Tag 069I, a lemma

Tag 069I in the Stacks Project.

AlgebraicGeometry.isLocalCompleteIntersectionMorphism_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/FlatBaseChange.lean, line 92. References: SGA 6 VIII (1.6), “flat base change stable”.

A flat base change of a local complete intersection morphism is a local complete intersection morphism.

public theorem isLocalCompleteIntersectionMorphism_pullback_snd
    {X S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S) [Flat g]
    (hf : IsLocalCompleteIntersectionMorphism f) :
    IsLocalCompleteIntersectionMorphism (pullback.snd f g)

Tag 069J, a lemma

Tag 069J in the Stacks Project.

AlgebraicGeometry.isLocalCompleteIntersectionMorphism_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/Composition.lean, line 126.

Stacks 069J. A composition of local complete intersection morphisms is a local complete intersection morphism.

theorem isLocalCompleteIntersectionMorphism_comp {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
    (hf : IsLocalCompleteIntersectionMorphism f)
    (hg : IsLocalCompleteIntersectionMorphism g) :
    IsLocalCompleteIntersectionMorphism (f ≫ g)

Tag 069K, a lemma

Tag 069K in the Stacks Project.

AlgebraicGeometry.flat_and_isLocalCompleteIntersectionMorphism_of_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/Syntomic.lean, line 118. The attribute's comment: “(2) ⇒ (1): a syntomic morphism is flat and a local complete intersection morphism”.

Stacks 069K, the implication (2) ⇒ (1). A syntomic morphism of schemes is flat and a local complete intersection morphism.

theorem flat_and_isLocalCompleteIntersectionMorphism_of_syntomic {X S : Scheme.{u}} {f : X ⟶ S}
    (hf : Syntomic f) : Flat f ∧ IsLocalCompleteIntersectionMorphism f

AlgebraicGeometry.syntomic_iff_flat_and_isLocalCompleteIntersectionMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/Syntomic.lean, line 147. The attribute's comment: “the equivalence of (1) and (2)”.

Stacks 069K. A morphism of schemes is syntomic if and only if it is flat and a local complete intersection morphism.

theorem syntomic_iff_flat_and_isLocalCompleteIntersectionMorphism {X S : Scheme.{u}} (f : X ⟶ S) :
    Syntomic f ↔ Flat f ∧ IsLocalCompleteIntersectionMorphism f

Tag 069L, a lemma

Tag 069L in the Stacks Project.

AlgebraicGeometry.isLocalCompleteIntersectionMorphism_of_isKoszulRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/RegularImmersion.lean, line 49. The attribute's comment: “Koszul-regular immersion”. References: SGA 5 III (6.8), “Direction”.

Stacks 069L. A Koszul-regular immersion of schemes is a local complete intersection morphism.

theorem isLocalCompleteIntersectionMorphism_of_isKoszulRegularImmersion {X S : Scheme.{u}}
    (i : X ⟶ S) [IsImmersion i] (hi : IsKoszulRegularImmersion i) :
    IsLocalCompleteIntersectionMorphism i

AlgebraicGeometry.isLocalCompleteIntersectionMorphism_of_isRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/RegularImmersion.lean, line 68. The attribute's comment: “regular immersion”. References: SGA 5 III (6.8), “Direction”.

Stacks 069L. A regular immersion of schemes is a local complete intersection morphism.

theorem isLocalCompleteIntersectionMorphism_of_isRegularImmersion {X S : Scheme.{u}}
    (i : X ⟶ S) [IsImmersion i] (hi : IsRegularImmersion i) :
    IsLocalCompleteIntersectionMorphism i

Tag 069M, a lemma

Tag 069M in the Stacks Project.

AlgebraicGeometry.isLocalCompleteIntersectionMorphism_of_comp_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/SmoothTarget.lean, line 75.

Stacks 069M. In a commutative triangle of morphisms of schemes with g : Y ⟶ S smooth, if the composite f ≫ g is a local complete intersection morphism then so is f : X ⟶ Y.

theorem isLocalCompleteIntersectionMorphism_of_comp_of_smooth {X Y S : Scheme.{u}} (f : X ⟶ Y)
    (g : Y ⟶ S) [Smooth g] (h : IsLocalCompleteIntersectionMorphism (f ≫ g)) :
    IsLocalCompleteIntersectionMorphism f

Tag 0E9K, a lemma

Tag 0E9K in the Stacks Project.

AlgebraicGeometry.isLocalCompleteIntersectionMorphism_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/RegularSchemes.lean, line 77.

A morphism of schemes which is locally of finite type and whose source and target are regular is a local complete intersection morphism.

theorem isLocalCompleteIntersectionMorphism_of_isRegular {X Y : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] (hX : IsRegular X) (hY : IsRegular Y) :
    IsLocalCompleteIntersectionMorphism f

Tag 09RL, a lemma

Tag 09RL in the Stacks Project.

AlgebraicGeometry.isLocalCompleteIntersectionMorphism_of_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/PerfectOverBase.lean, line 301. The attribute's comment: “the morphism to the intermediate scheme is a local complete intersection morphism”.

Stacks 09RL, the relative conclusion. Let X ⟶ Y ⟶ S be a commutative triangle of morphisms of schemes with S locally Noetherian and Y ⟶ S locally of finite type. If f : X ⟶ Y is perfect and X ⟶ S is a local complete intersection morphism, then f is a local complete intersection morphism.

theorem isLocalCompleteIntersectionMorphism_of_perfect {X Y S : Scheme.{u}} (f : X ⟶ Y)
    (g : Y ⟶ S) {h : X ⟶ S} (hcomm : f ≫ g = h) [IsLocallyNoetherian S] [LocallyOfFiniteType g]
    [AlgebraicGeometry.Perfect f] (hh : IsLocalCompleteIntersectionMorphism h) :
    IsLocalCompleteIntersectionMorphism f

AlgebraicGeometry.koszulAt_of_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/PerfectOverBase.lean, line 310. The attribute's comment: “the intermediate scheme is Koszul over the base at every point of the image”.

Stacks 09RL, the conclusion on the base. In the same situation, g : Y ⟶ S is Koszul at the image of every point of X.

theorem koszulAt_of_perfect {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S) {h : X ⟶ S}
    (hcomm : f ≫ g = h) [IsLocallyNoetherian S] [LocallyOfFiniteType g]
    [AlgebraicGeometry.Perfect f] (hh : IsLocalCompleteIntersectionMorphism h) (x : X) :
    KoszulAt g (f.base x)

Tag 0FJ2, a lemma

Tag 0FJ2 in the Stacks Project.

AlgebraicGeometry.isLocalCompleteIntersectionMorphism_of_isRegular_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/RegularTarget.lean, line 54. The attribute's comment: “f is a local complete intersection morphism”.

Let X ⟶ Y ⟶ S be a commutative triangle of morphisms of schemes with S locally Noetherian, Y ⟶ S locally of finite type and Y regular. If X ⟶ S is a local complete intersection morphism, then so is f : X ⟶ Y.

theorem isLocalCompleteIntersectionMorphism_of_isRegular_target {X Y S : Scheme.{u}} (f : X ⟶ Y)
    (g : Y ⟶ S) {h : X ⟶ S} (hcomm : f ≫ g = h) [IsLocallyNoetherian S] [LocallyOfFiniteType g]
    (hY : IsRegular Y) (hh : IsLocalCompleteIntersectionMorphism h) :
    IsLocalCompleteIntersectionMorphism f

AlgebraicGeometry.koszulAt_of_isRegular_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/RegularTarget.lean, line 66. The attribute's comment: “Y ⟶ S is Koszul at the image of every point of X”.

Let X ⟶ Y ⟶ S be a commutative triangle of morphisms of schemes with S locally Noetherian, Y ⟶ S locally of finite type and Y regular. If X ⟶ S is a local complete intersection morphism, then g : Y ⟶ S is Koszul at the image of every point of X.

theorem koszulAt_of_isRegular_target {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S) {h : X ⟶ S}
    (hcomm : f ≫ g = h) [IsLocallyNoetherian S] [LocallyOfFiniteType g] (hY : IsRegular Y)
    (hh : IsLocalCompleteIntersectionMorphism h) (x : X) : KoszulAt g (f.base x)

Tag 0FK1, a lemma

Tag 0FK1 in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.isRegularImmersion_of_perfect_of_conormalSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/PerfectLocallyFreeConormal.lean, line 354.

Stacks tag 0FK1. An immersion i : X ⟶ Y which is perfect, whose target is locally Noetherian and whose conormal sheaf is finite locally free, is a regular immersion.

theorem isRegularImmersion_of_perfect_of_conormalSheaf (i : X ⟶ Y) [IsImmersion i]
    [AlgebraicGeometry.Perfect i] [IsLocallyNoetherian Y]
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u}
      (Stacks.Conormal.conormalSheaf i)] :
    IsRegularImmersion i

Tag 0FV6, a lemma

Tag 0FV6 in the Stacks Project.

AlgebraicGeometry.isPerfect_and_hasTorAmplitude_naiveCotangentComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/NaiveCotangent.lean, line 454. The attribute's comment: “both halves: NL_{X/Y} of a local complete intersection morphism is perfect and has tor-amplitude in [-1,0]”. References: SGA 6 VIII (2.4), “more general”; SGA 6 XIV (2.1).

Stacks 0FV6. The naive cotangent complex of a local complete intersection morphism is a perfect object of D(𝒪_X) of Tor amplitude in [-1, 0].

Near a point of the source the morphism restricts to a morphism of affine schemes whose map on sections is a local complete intersection homomorphism, and there NL_{X/Y} is the derived pullback of the derived sheafification of the naive cotangent complex of that homomorphism; both conditions hold on it by Stacks 0FV0 and descend to the restriction by Stacks 08E9 and Stacks 08EB. Both conditions are local on the source, so they hold on X.

theorem isPerfect_and_hasTorAmplitude_naiveCotangentComplex {X Y : Scheme.{u}} (f : X ⟶ Y)
    (hf : IsLocalCompleteIntersectionMorphism f) :
    Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace)
        (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) ∧
      Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
        (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) (-1) 0

Tag 0FK2, a lemma

Tag 0FK2 in the Stacks Project.

AlgebraicGeometry.hasTorAmplitude_naiveCotangentComplex_of_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/NaiveCotangent.lean, line 500. The attribute's comment: “(1) ⇒ (2): for a perfect morphism of locally Noetherian schemes which is a local complete intersection morphism, NL_{X/Y} has tor-amplitude in [-1,0]”.

Stacks 0FK2, the implication (1) ⇒ (2). If a perfect morphism of locally Noetherian schemes is a local complete intersection morphism, then NL_{X/Y} has Tor amplitude in [-1, 0].

The three standing hypotheses are not used: Tor amplitude in [-1, 0] holds for the naive cotangent complex of any local complete intersection morphism.

theorem hasTorAmplitude_naiveCotangentComplex_of_perfect {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsLocallyNoetherian X] [IsLocallyNoetherian Y] [Perfect f]
    (hf : IsLocalCompleteIntersectionMorphism f) :
    Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
      (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) (-1) 0

AlgebraicGeometry.isPerfect_and_hasTorAmplitude_naiveCotangentComplex_of_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/NaiveCotangent.lean, line 517. The attribute's comment: “(1) ⇒ (3): for a perfect morphism of locally Noetherian schemes which is a local complete intersection morphism, NL_{X/Y} is perfect with tor-amplitude in [-1,0]”. References: SGA 6 VIII (2.4), “partial”; SGA 6 XIV (2.1), “special case”.

Stacks 0FK2, the implication (1) ⇒ (3). If a perfect morphism of locally Noetherian schemes is a local complete intersection morphism, then NL_{X/Y} is perfect with Tor amplitude in [-1, 0].

The three standing hypotheses are not used: both conditions hold for the naive cotangent complex of any local complete intersection morphism.

theorem isPerfect_and_hasTorAmplitude_naiveCotangentComplex_of_perfect {X Y : Scheme.{u}}
    (f : X ⟶ Y) [IsLocallyNoetherian X] [IsLocallyNoetherian Y] [Perfect f]
    (hf : IsLocalCompleteIntersectionMorphism f) :
    Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace)
        (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) ∧
      Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
        (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) (-1) 0

AlgebraicGeometry.naiveCotangentComplex_tfae_isLocalCompleteIntersectionMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/NaiveCotangentConverse.lean, line 225. References: SGA 6 VIII (2.4), “partial”; SGA 6 XIV (2.1), “(1) ⇒ (3), special case”.

Stacks 0FK2. Let f : X ⟶ Y be a perfect morphism of locally Noetherian schemes. The following are equivalent:

f is a local complete intersection morphism;

NL_{X/Y} has Tor amplitude in [-1, 0];

NL_{X/Y} is perfect with Tor amplitude in [-1, 0].

Here NL_{X/Y} is AlgebraicGeometry.Scheme.naiveCotangentComplex, Stacks 0D0H, read at its class in D(𝒪_X); Tor amplitude is Stacks.Cohomology.TorAmplitude.HasTorAmplitude, Stacks 08CG, taken against the canonical derived tensor product of a ringed space, and perfectness is Stacks.Cohomology.PerfectComplexes.IsPerfect, Stacks 08CM. Both are stated at the underlying ringed space of X, with the standard derived category, as they are for Stacks 08E9 and Stacks 08EB.

Rendered on sections over a compatible pair of affine opens the statement is Stacks 0FJT; the translation is Stacks 07DB and Stacks 0D0I together with Stacks 08E9 and Stacks 08EB.

theorem naiveCotangentComplex_tfae_isLocalCompleteIntersectionMorphism {X Y : Scheme.{u}}
    (f : X ⟶ Y) [IsLocallyNoetherian X] [IsLocallyNoetherian Y] [Perfect f] :
    List.TFAE
      [IsLocalCompleteIntersectionMorphism f,
        Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
          (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) (-1) 0,
        Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace)
            (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) ∧
          Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
            (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) (-1) 0]

Tag 0FK3, a lemma

Tag 0FK3 in the Stacks Project.

AlgebraicGeometry.isLocalCompleteIntersectionMorphism_iff_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/NaiveCotangent.lean, line 132. The attribute's comment: “(1) ⇔ (2): a flat morphism of finite presentation is a local complete intersection morphism iff it is syntomic”.

Stacks 0FK3, the equivalence of (1) and (2). A flat morphism of finite presentation is a local complete intersection morphism exactly when it is syntomic.

Finite presentation is a standing hypothesis of the source and is not used: the equivalence holds for any flat morphism, by Stacks 069K.

theorem isLocalCompleteIntersectionMorphism_iff_syntomic {X Y : Scheme.{u}} (f : X ⟶ Y)
    [Flat f] (_hfp : FinitePresentation f) :
    IsLocalCompleteIntersectionMorphism f ↔ Syntomic f

AlgebraicGeometry.hasTorAmplitude_naiveCotangentComplex_of_isPerfect_of_hasTorAmplitude, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/NaiveCotangent.lean, line 149. The attribute's comment: “(4) ⇒ (3), which is a projection: NL_{X/Y} perfect with tor-amplitude in [-1,0] has tor-amplitude in [-1,0]. Fixes which library predicates conditions (3) and (4) are read at”.

Stacks 0FK3, the implication (4) ⇒ (3). If NL_{X/Y} is perfect with Tor amplitude in [-1, 0], then it has Tor amplitude in [-1, 0].

The implication is a projection, as it is in the source. The declaration's purpose is to pin conditions (3) and (4) of the tag to Stacks.Cohomology.TorAmplitude.HasTorAmplitude of Stacks 08CG, taken against the canonical derived tensor product of Stacks 06YU, and to Stacks.Cohomology.PerfectComplexes.IsPerfect of Stacks 08CM; the tree carries several further spellings of each. The tag's standing hypotheses are not needed, so the statement is made for an arbitrary morphism of schemes.

theorem hasTorAmplitude_naiveCotangentComplex_of_isPerfect_of_hasTorAmplitude
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    (hf : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace)
        (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) ∧
      Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
        (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) (-1) 0) :
    Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
      (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) (-1) 0

AlgebraicGeometry.hasTorAmplitude_naiveCotangentComplex_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/NaiveCotangent.lean, line 470. The attribute's comment: “(1) ⇒ (3): for a flat morphism of finite presentation which is a local complete intersection morphism, NL_{X/Y} has tor-amplitude in [-1,0]”.

Stacks 0FK3, the implication (1) ⇒ (3). If a flat morphism of finite presentation is a local complete intersection morphism, then NL_{X/Y} has Tor amplitude in [-1, 0].

The two standing hypotheses are not used: Tor amplitude in [-1, 0] holds for the naive cotangent complex of any local complete intersection morphism.

theorem hasTorAmplitude_naiveCotangentComplex_of_flat {X Y : Scheme.{u}} (f : X ⟶ Y)
    [Flat f] (_hfp : FinitePresentation f) (hf : IsLocalCompleteIntersectionMorphism f) :
    Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
      (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) (-1) 0

AlgebraicGeometry.isPerfect_and_hasTorAmplitude_naiveCotangentComplex_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/NaiveCotangent.lean, line 483. The attribute's comment: “(1) ⇒ (4): for a flat morphism of finite presentation which is a local complete intersection morphism, NL_{X/Y} is perfect with tor-amplitude in [-1,0]”.

Stacks 0FK3, the implication (1) ⇒ (4). If a flat morphism of finite presentation is a local complete intersection morphism, then NL_{X/Y} is perfect with Tor amplitude in [-1, 0].

The two standing hypotheses are not used: both conditions hold for the naive cotangent complex of any local complete intersection morphism.

theorem isPerfect_and_hasTorAmplitude_naiveCotangentComplex_of_flat {X Y : Scheme.{u}}
    (f : X ⟶ Y) [Flat f] (_hfp : FinitePresentation f)
    (hf : IsLocalCompleteIntersectionMorphism f) :
    Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace)
        (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) ∧
      Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
        (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) (-1) 0

AlgebraicGeometry.syntomic_of_hasTorAmplitude_naiveCotangentComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/NaiveCotangent.lean, line 536. The attribute's comment: “(3) ⇒ (2): a flat morphism of finite presentation whose naive cotangent complex has tor-amplitude in [-1,0] is syntomic”.

Stacks 0FK3, the implication (3) ⇒ (2). A flat morphism of finite presentation whose naive cotangent complex has Tor amplitude in [-1, 0] is syntomic.

Syntomicity is a condition at each point of the source, asking for affine opens V ∋ x of X and U of Y with V ⊆ f⁻¹(U) over which the morphism is syntomic on sections. On such a pair the hypothesis descends to Tor amplitude in [-1, 0] of NL_{Γ(X, V)/Γ(Y, U)} in D(Γ(X, V)), and Γ(Y, U) → Γ(X, V) is flat of finite presentation, so Stacks 0FJV makes it syntomic. Quasi-compactness and quasi-separatedness are not used.

theorem syntomic_of_hasTorAmplitude_naiveCotangentComplex {X Y : Scheme.{u}} (f : X ⟶ Y)
    [Flat f] (hfp : FinitePresentation f)
    (hamp : Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
      (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) (-1) 0) :
    Syntomic f

AlgebraicGeometry.isLocalCompleteIntersectionMorphism_of_hasTorAmplitude_naiveCotangentComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/NaiveCotangent.lean, line 560. The attribute's comment: “(3) ⇒ (1): a flat morphism of finite presentation whose naive cotangent complex has tor-amplitude in [-1,0] is a local complete intersection morphism”.

Stacks 0FK3, the implication (3) ⇒ (1). A flat morphism of finite presentation whose naive cotangent complex has Tor amplitude in [-1, 0] is a local complete intersection morphism: it is syntomic, and a syntomic morphism is Koszul by Stacks 069K.

theorem isLocalCompleteIntersectionMorphism_of_hasTorAmplitude_naiveCotangentComplex
    {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] (hfp : FinitePresentation f)
    (hamp : Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
      (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) (-1) 0) :
    IsLocalCompleteIntersectionMorphism f

AlgebraicGeometry.naiveCotangentComplex_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/NaiveCotangent.lean, line 572.

Stacks 0FK3. For a flat morphism of finite presentation f : X ⟶ Y the following are equivalent: f is a local complete intersection morphism; f is syntomic; NL_{X/Y} has Tor amplitude in [-1, 0]; NL_{X/Y} is perfect with Tor amplitude in [-1, 0].

theorem naiveCotangentComplex_tfae {X Y : Scheme.{u}} (f : X ⟶ Y)
    [Flat f] (hfp : FinitePresentation f) :
    List.TFAE
      [IsLocalCompleteIntersectionMorphism f,
        Syntomic f,
        Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
          (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) (-1) 0,
        Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace)
            (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) ∧
          Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
            (DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) (-1) 0]

Tag 0FDP, a lemma

Tag 0FDP in the Stacks Project.

AlgebraicGeometry.smooth_tfae_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/SmoothDiagonal.lean, line 331. References: SGA 1 II (4.18), “(1) ⇒ (2), special case”; SGA 6 VII (1.10), “special case”.

Stacks 0FDP. Let f : X ⟶ Y be a morphism of finite type between locally Noetherian schemes and let Δ : X ⟶ X ×_Y X be its diagonal. The following are equivalent:

f is smooth;

f is flat and Δ is a regular immersion;

f is flat and Δ is a local complete intersection morphism;

f is flat and Δ is perfect.

A smooth morphism is flat and its diagonal is a section of the smooth first projection, hence a regular immersion by Stacks 067R; a regular immersion is a local complete intersection morphism by Stacks 069L; such a morphism is perfect by Stacks 069H; and the interesting implication back to smoothness is AlgebraicGeometry.smooth_of_flat_of_perfect_diagonal, which runs Stacks 0FCX on affine charts.

theorem smooth_tfae_diagonal {X Y : Scheme.{u}} (f : X ⟶ Y) [IsLocallyNoetherian X]
    [IsLocallyNoetherian Y] [LocallyOfFiniteType f] [QuasiCompact f] :
    List.TFAE
      [Smooth f,
        Flat f ∧ Stacks.AlgebraicGeometry.RegularIdealSheaf.IsRegularImmersion
          (pullback.diagonal f),
        Flat f ∧ IsLocalCompleteIntersectionMorphism (pullback.diagonal f),
        Flat f ∧ Perfect (pullback.diagonal f)]

Tag 069N, a lemma

Tag 069N in the Stacks Project.

AlgebraicGeometry.isLocalCompleteIntersectionMorphism_isLocalAtTarget_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/FpqcLocalAtTarget.lean, line 118. References: SGA 2 XII (4.10), “partial”.

Stacks 069N. Being a local complete intersection morphism of schemes is fpqc local on the target: a morphism is Koszul if and only if its base change along every member of an fpqc covering of its target is Koszul.

theorem isLocalCompleteIntersectionMorphism_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      (@IsLocalCompleteIntersectionMorphism : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 069P, a lemma

Tag 069P in the Stacks Project.

AlgebraicGeometry.isLocalAtSource_syntomic_isLocalCompleteIntersectionMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/LocalCompleteIntersectionAffine.lean, line 1044.

Stacks 069P. The property of being a local complete intersection morphism of schemes is syntomic local on the source: a morphism is Koszul exactly when its composites with the members of a syntomic covering of its source are.

All four inputs of the syntomic case of Stacks 036H are supplied: Zariski locality on the source and on the target and preservation under precomposition with a syntomic morphism come from StacksFrontier.AlgebraicGeometry.Descent.LocalOnSourceTopologies.LocalCompleteIntersection, and the affine descent is AlgebraicGeometry.isLocalCompleteIntersectionMorphism_of_surjective_syntomic_of_isAffine.

theorem isLocalAtSource_syntomic_isLocalCompleteIntersectionMorphism :
    MorphismProperty.IsLocalAtSource
      (@IsLocalCompleteIntersectionMorphism.{u} : MorphismProperty Scheme.{u})
      (Scheme.precoverage (@Syntomic.{u}))

AlgebraicGeometry.isLocalCompleteIntersectionMorphism_isLocalAtSource_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/LocalCompleteIntersectionEtale.lean, line 163. The attribute's comment: “the étale case, unconditionally: the Koszul property of morphisms of schemes is local on the source for the étale topology. The syntomic statement of the tag is not claimed here”.

Stacks 069P, restricted to étale coverings. The property of being a local complete intersection morphism of schemes is local on the source for the étale topology: a morphism is Koszul exactly when its composites with the members of an étale covering of its source are.

All four inputs of the étale case of Stacks 036H are available: Zariski locality on the source and on the target come from StacksFrontier.AlgebraicGeometry.Descent.LocalOnSourceTopologies.LocalCompleteIntersection, preservation under precomposition with an étale morphism is AlgebraicGeometry.respectsLeft_etale_isLocalCompleteIntersectionMorphism, and the affine descent is AlgebraicGeometry.isLocalCompleteIntersectionMorphism_of_surjective_smooth_of_isAffine read at an étale g.

theorem isLocalCompleteIntersectionMorphism_isLocalAtSource_etale :
    MorphismProperty.IsLocalAtSource
      (@IsLocalCompleteIntersectionMorphism.{u} : MorphismProperty Scheme.{u})
      Scheme.etalePrecoverage

Tag 06B8, a lemma

Tag 06B8 in the Stacks Project.

AlgebraicGeometry.isOpen_koszulAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/KoszulLocus.lean, line 868. The attribute's comment: “the Koszul locus is open”.

The Koszul locus is open. A witness for KoszulAt f x — an open U ∋ x on which f factors through a Koszul-regular immersion into a scheme smooth over the target — witnesses KoszulAt f z for every z in U, because Koszul-regularity is a condition on the immersion and not on the point. Intersecting U with the affine open witnessing finite type at x gives a neighbourhood of x inside the locus.

public theorem isOpen_koszulAt {X Y : Scheme.{u}} (f : X ⟶ Y) :
    IsOpen {x : X | KoszulAt f x}

AlgebraicGeometry.koszulAt_baseChange_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/KoszulLocus.lean, line 882. The attribute's comment: “formation of the Koszul locus commutes with arbitrary base change”.

The formation of the Koszul locus commutes with arbitrary base change. Let f : X ⟶ Y be a morphism of schemes over S with X and Y both flat and locally of finite presentation over S. For any g : S' ⟶ S, the base change of f is Koszul at a point of X ×_S S' exactly when f is Koszul at its image in X.

public theorem koszulAt_baseChange_iff {X Y S S' : Scheme.{u}} (f : X ⟶ Y) (p : X ⟶ S)
    (q : Y ⟶ S) (h : f ≫ q = p) [Flat p] [Flat q] [LocallyOfFinitePresentation p]
    [LocallyOfFinitePresentation q] (g : S' ⟶ S) (x' : (pullback p g : Scheme.{u})) :
    KoszulAt (pullback.map p g q g f (𝟙 _) (𝟙 _)
        (by simpa only [Category.comp_id] using h.symm) (by simp)) x' ↔
      KoszulAt f ((pullback.fst p g).base x')

Tag 06B9, a lemma

Tag 06B9 in the Stacks Project.

AlgebraicGeometry.unramified_iff_formallyUnramified_of_isLocalCompleteIntersectionMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/UnramifiedConormal.lean, line 84. The attribute's comment: “the equivalence: a local complete intersection morphism is unramified if and only if it is formally unramified”.

A local complete intersection morphism of schemes is unramified if and only if it is formally unramified.

theorem unramified_iff_formallyUnramified_of_isLocalCompleteIntersectionMorphism
    {X S : Scheme.{u}} {f : X ⟶ S} (hf : IsLocalCompleteIntersectionMorphism f) :
    Unramified f ↔ FormallyUnramified f

AlgebraicGeometry.isFiniteLocallyFree_universalConormalSheaf_of_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/UnramifiedConormal.lean, line 158. The attribute's comment: “finite local freeness of the conormal sheaf of a local complete intersection morphism. Tag 063H is NOT needed: the Koszul-regular factor is quasi-regular, and condition (2) of Tag 063M is available for those”.

The conormal sheaf of a formally unramified local complete intersection morphism of schemes is finite locally free.

theorem isFiniteLocallyFree_universalConormalSheaf_of_isLocalCompleteIntersection
    {X S : Scheme.{u}} (f : X ⟶ S) [FormallyUnramified f]
    (hf : IsLocalCompleteIntersectionMorphism f) :
    SheafOfModules.IsFiniteLocallyFree.{u, u, u} (universalConormalSheaf f)

Tag 06BA, a lemma

Tag 06BA in the Stacks Project.

Stacks.Thickenings.mono_transitivityConormalLeftMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/TransitivityConormalShortExact.lean, line 200. The attribute's comment: “the left arrow of the sequence of Stacks 06AE is a monomorphism”.

The first arrow of the conormal sequence of part (2) of [Stacks Project, Tag 06AE] is a monomorphism when Z ⟶ Y is a local complete intersection morphism.

theorem mono_transitivityConormalLeftMap (hi : IsLocalCompleteIntersectionMorphism i) :
    Mono (transitivityConormalLeftMap i p tZ tY)

Stacks.Thickenings.transitivityConormalShortComplex_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/TransitivityConormalShortExact.lean, line 241. The attribute's comment: “the conormal sequence of Stacks 06AE is short exact”. References: SGA 6 VIII (2.6), “partial”.

Let Z --i--→ Y --p--→ X be morphisms of schemes with universal first-order thickenings Z ⊂ Z' of Z over X and Y ⊂ Y' of Y over X, and assume i is a local complete intersection morphism. Then the conormal sequence
0 ⟶ i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} ⟶ 0
of part (2) of [Stacks Project, Tag 06AE] is short exact: its left arrow is a monomorphism, it is exact at the middle term, and its right arrow is an epimorphism.

theorem transitivityConormalShortComplex_shortExact
    (hi : IsLocalCompleteIntersectionMorphism i) :
    (transitivityConormalShortComplex i p tZ tY).ShortExact

Sources

LeanStacks.AlgebraicGeometry.RegularIdealSheaf.exists_opens_isKoszulRegularImmersion_comp_iff · AlgebraicGeometry.KoszulAt · AlgebraicGeometry.IsLocalCompleteIntersectionMorphism · AlgebraicGeometry.isKoszulRegularImmersion_of_koszul · AlgebraicGeometry.perfect_of_isLocalCompleteIntersectionMorphism · AlgebraicGeometry.pseudoCoherent_of_isLocalCompleteIntersectionMorphism · AlgebraicGeometry.locallyOfFinitePresentation_of_isLocalCompleteIntersectionMorphism · AlgebraicGeometry.isLocalCompleteIntersectionMorphism_iff_appTop

Section37.64 Weakly étale morphisms #

Section 37.64 of the Stacks Project, Tag 094N. 13 tags here are carried by 14 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 094Q, a lemma

Tag 094Q in the Stacks Project.

AlgebraicGeometry.weaklyEtale_iff_stalkMap_weaklyEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/Stalks.lean, line 170.

A morphism of schemes is weakly étale if and only if all of its maps on local rings are weakly étale.

theorem weaklyEtale_iff_stalkMap_weaklyEtale
    {X Y : AlgebraicGeometry.Scheme.{u}} (f : X ⟶ Y) :
    AlgebraicGeometry.WeaklyEtale f ↔
      ∀ x : X,
        letI := (f.stalkMap x).hom.toAlgebra
        Algebra.WeaklyEtale (Y.presheaf.stalk (f x)) (X.presheaf.stalk x)

Tag 094R, a lemma

Tag 094R in the Stacks Project.

AlgebraicGeometry.isFlatOver_self_of_flat_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/Flat.lean, line 84.

If the diagonal of a scheme morphism is flat, every module flat over the target is flat over the source.

theorem isFlatOver_self_of_flat_diagonal
    {X Y : Scheme.{u}} (f : X ⟶ Y) (F : X.Modules)
    [Flat (pullback.diagonal f)]
    (hF : IsFlatOver f.toLRSHom.toShHom F) :
    IsFlatOver ((𝟙 X : X ⟶ X).toLRSHom.toShHom) F

Tag 094S, a lemma

Tag 094S in the Stacks Project.

AlgebraicGeometry.weaklyEtale_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/Characterization.lean, line 110. The attribute's comment: “equivalent conditions”.

Stacks Project, Tag 094S. For a morphism of schemes, weak étaleness is equivalent to weak étaleness of every induced map on affine-open sections, to admitting compatible open coverings on which the restricted morphisms are weakly étale, and to the analogous condition for affine-open coverings and their induced maps on sections.

theorem weaklyEtale_tfae {X S : Scheme.{u}} (f : X ⟶ S) :
    let weaklyEtaleOn := fun (V : S.Opens) (U : X.Opens) (e : U ≤ f ⁻¹ᵁ V) ↦
      @Algebra.WeaklyEtale Γ(S, V) Γ(X, U) _ _ (f.appLE V U e).hom.toAlgebra
    List.TFAE [
      WeaklyEtale f,
      ∀ (U : X.Opens), IsAffineOpen U →
        ∀ (V : S.Opens), IsAffineOpen V →
          ∀ (e : U ≤ f ⁻¹ᵁ V), weaklyEtaleOn V U e,
      ∃ (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, WeaklyEtale
              (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, weaklyEtaleOn (V j) (U i) ((le_iSup U i).trans hU.le)]

Declarations registered for the tag:

AlgebraicGeometry.WeaklyEtale.instResLE registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/Characterization.lean, line 173 (StacksFrontier): “restriction to open subschemes”.

Tag 094T, a lemma

Tag 094T in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.MorphismProperty.diagonal_isStableUnderComposition registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 43 (StacksFrontier): “(1), for P = @AlgebraicGeometry.Flat on schemes: flat diagonals compose”.
AlgebraicGeometry.WeaklyEtale.instCompScheme registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 46 (StacksFrontier): “(2)”.

Tag 094U, a lemma

Tag 094U in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.MorphismProperty.IsStableUnderBaseChange.diagonal registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 49 (StacksFrontier): “(1), for P = @AlgebraicGeometry.Flat on schemes: flat diagonals base change”.
AlgebraicGeometry.WeaklyEtale.instIsStableUnderBaseChangeScheme registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 52 (StacksFrontier): “(2)”.

Tag 094V, a lemma

Tag 094V in the Stacks Project.

AlgebraicGeometry.flat_diagonal_of_surjective_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/WeaklyEtale/DiagonalDescent.lean, line 37.

Flatness of the relative diagonal descends along a surjective flat morphism.

theorem flat_diagonal_of_surjective_flat {X Y Z : Scheme.{u}}
    (f : X ⟶ Y) (g : Y ⟶ Z) [Flat f] [Surjective f]
    [Flat (pullback.diagonal (f ≫ g))] :
    Flat (pullback.diagonal g)

Tag 094W, a lemma

Tag 094W in the Stacks Project.

AlgebraicGeometry.instFormallyUnramified, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/Characterization.lean, line 179.

Stacks Project, Tag 094W. A weakly étale morphism of schemes is formally unramified.

instance instFormallyUnramified
    {X Y : AlgebraicGeometry.Scheme.{u}} (f : X ⟶ Y)
    [AlgebraicGeometry.WeaklyEtale f] :
    AlgebraicGeometry.FormallyUnramified f

Tag 094X, a lemma

Tag 094X in the Stacks Project.

AlgebraicGeometry.WeaklyEtale.of_flat_of_mono, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/Examples.lean, line 50. The attribute's comment: “(1) flat monomorphism”.

A flat monomorphism of schemes is weakly étale: its diagonal is an isomorphism.

instance (priority := 900) of_flat_of_mono [Flat f] [Mono f] : WeaklyEtale f

AlgebraicGeometry.WeaklyEtale.of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/Examples.lean, line 54. The attribute's comment: “(2) open immersion”.

An open immersion of schemes is weakly étale.

theorem of_isOpenImmersion [IsOpenImmersion f] : WeaklyEtale f

AlgebraicGeometry.WeaklyEtale.of_flat_of_formallyUnramified, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/Examples.lean, line 59. The attribute's comment: “(3) flat and unramified”.

A flat unramified morphism of schemes is weakly étale: its diagonal is an open immersion.

instance (priority := 900) of_flat_of_formallyUnramified [Flat f] [FormallyUnramified f]
    [LocallyOfFiniteType f] : WeaklyEtale f

AlgebraicGeometry.WeaklyEtale.of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/Examples.lean, line 64. The attribute's comment: “(4) étale”.

An étale morphism of schemes is weakly étale.

theorem of_etale [Etale f] : WeaklyEtale f

Tag 094Y, a lemma

Tag 094Y in the Stacks Project.

AlgebraicGeometry.isReduced_of_weaklyEtale, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/Characterization.lean, line 190.

The source of a weakly étale morphism with reduced target is reduced.

lemma isReduced_of_weaklyEtale
    {X Y : AlgebraicGeometry.Scheme.{u}} (f : X ⟶ Y)
    [AlgebraicGeometry.IsReduced Y] [AlgebraicGeometry.WeaklyEtale f] :
    AlgebraicGeometry.IsReduced X

Tag 094Z, a lemma

Tag 094Z in the Stacks Project.

AlgebraicGeometry.weaklyEtale_iff_strictHenselizationMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/Stalks.lean, line 351.

A morphism of schemes is weakly étale if and only if every map that it induces between compatible strict henselizations of its local rings is an isomorphism.

theorem weaklyEtale_iff_strictHenselizationMap_bijective
    {X Y : AlgebraicGeometry.Scheme.{u}} (f : X ⟶ Y) :
    AlgebraicGeometry.WeaklyEtale f ↔
      ∀ (x : X) (Ysh Xsh : Type u)
        [CommRing Ysh] [IsLocalRing Ysh]
        [CommRing Xsh] [IsLocalRing Xsh]
        [Algebra (Y.presheaf.stalk (f x)) Ysh]
        [Algebra (IsLocalRing.ResidueField (Y.presheaf.stalk (f x)))
          (IsLocalRing.ResidueField Ysh)]
        [IsSepClosure (IsLocalRing.ResidueField (Y.presheaf.stalk (f x)))
          (IsLocalRing.ResidueField Ysh)]
        [IsLocalRing.IsHenselization (Y.presheaf.stalk (f x))
          (IsLocalRing.ResidueField Ysh) Ysh]
        [Algebra (X.presheaf.stalk x) Xsh]
        [Algebra (IsLocalRing.ResidueField (X.presheaf.stalk x))
          (IsLocalRing.ResidueField Xsh)]
        [IsSepClosure (IsLocalRing.ResidueField (X.presheaf.stalk x))
          (IsLocalRing.ResidueField Xsh)]
        [IsLocalRing.IsHenselization (X.presheaf.stalk x)
          (IsLocalRing.ResidueField Xsh) Xsh]
        (φ : IsLocalRing.ResidueField Ysh →+* IsLocalRing.ResidueField Xsh)
        (g : Ysh →+* Xsh),
        IsLocalHom g →
          g.comp (algebraMap (Y.presheaf.stalk (f x)) Ysh) =
            (algebraMap (X.presheaf.stalk x) Xsh).comp (f.stalkMap x).hom →
          (IsLocalRing.residue Xsh).comp g =
              φ.comp (IsLocalRing.residue Ysh) →
            Function.Bijective g

Tag 0950, a lemma

Tag 0950 in the Stacks Project.

AlgebraicGeometry.isNormal_of_weaklyEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/Normal.lean, line 63.

Stacks Project, Tag 0950. A weakly étale morphism with normal target has normal source.

theorem isNormal_of_weaklyEtale {X Y : Scheme.{u}} (f : X ⟶ Y) [IsNormal Y] [WeaklyEtale f] :
    IsNormal X

Tag 0F6V, a lemma

Tag 0F6V in the Stacks Project.

AlgebraicGeometry.isIso_of_weaklyEtale_of_universalHomeomorphism, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/Isomorphism.lean, line 40.

A weakly étale universal homeomorphism of schemes is an isomorphism.

instance isIso_of_weaklyEtale_of_universalHomeomorphism
    {X Y : Scheme.{u}} (f : X ⟶ Y) [WeaklyEtale f]
    [UniversalHomeomorphism f] : IsIso f

Tag 0F6W, a lemma

Tag 0F6W in the Stacks Project.

AlgebraicGeometry.isIso_relativeFrobenius_of_weaklyEtale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/Isomorphism.lean, line 67. References: SGA 4½ Fonctions L (3.4), “more general”; SGA 4½ Rapport (1.2), “special case”; SGA 5 XV (1.Proposition2), “more general”.

The relative Frobenius of a weakly étale scheme is an isomorphism.

instance isIso_relativeFrobenius_of_weaklyEtale (X : Scheme.{u}) (p : ℕ)
    [Fact p.Prime] (hX : IsInCharacteristic X p) (U : Over X) [WeaklyEtale U.hom] :
    IsIso (relativeFrobenius X p hX U)

Sources

LeanAlgebraicGeometry.weaklyEtale_iff_stalkMap_weaklyEtale · AlgebraicGeometry.isFlatOver_self_of_flat_diagonal · AlgebraicGeometry.weaklyEtale_tfae · AlgebraicGeometry.WeaklyEtale.instResLE · CategoryTheory.MorphismProperty.diagonal_isStableUnderComposition · AlgebraicGeometry.WeaklyEtale.instCompScheme · CategoryTheory.MorphismProperty.IsStableUnderBaseChange.diagonal · AlgebraicGeometry.WeaklyEtale.instIsStableUnderBaseChangeScheme

Section37.65 Reduced fibre theorem #

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

Tag 09IK, an equation

Tag 09IK in the Stacks Project.

AlgebraicGeometry.normalizedBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/NormalizedBaseChange.lean, line 49. The attribute's comment: “the normalization morphism to the base change”.

The normalized pullback of a finite-type scheme over a Dedekind domain along the integral closure in a finite fraction-field extension, as a scheme over the pullback.

noncomputable def normalizedBaseChange
    (A K L B : Type u)
    [CommRing A] [IsDedekindDomain A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra K L] [FiniteDimensional K L]
    [Algebra A L] [IsScalarTower A K L]
    [CommRing B] [Algebra A B] [Algebra B L]
    [IsScalarTower A B L] [IsIntegralClosure B A L]
    (X : Scheme.{u}) (p : X ⟶ Spec (.of A))
    [Flat p] [LocallyOfFiniteType p] [QuasiCompact p] :
    let g : Spec (.of B) ⟶ Spec (.of A) :=
      Spec.map (CommRingCat.ofHom (algebraMap A B))
    Over (pullback p g)

AlgebraicGeometry.normalizedBaseChangeOverIntegralClosure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/NormalizedBaseChange.lean, line 79. The attribute's comment: “the morphism to the integral closure”.

The structure morphism to the integral closure in the normalized base-change diagram.

noncomputable def normalizedBaseChangeOverIntegralClosure
    (A K L B : Type u)
    [CommRing A] [IsDedekindDomain A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra K L] [FiniteDimensional K L]
    [Algebra A L] [IsScalarTower A K L]
    [CommRing B] [Algebra A B] [Algebra B L]
    [IsScalarTower A B L] [IsIntegralClosure B A L]
    (X : Scheme.{u}) (p : X ⟶ Spec (.of A))
    [Flat p] [LocallyOfFiniteType p] [QuasiCompact p] :
    Over (Spec (.of B))

Tag 09IL, a theorem

Tag 09IL in the Stacks Project.

AlgebraicGeometry.exists_finiteExtension_smoothAt_genericPoints_fiber_normalization_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ReducedFibreTheorem.lean, line 379.

Stacks Project, Tag 09IL (the reduced fibre theorem). Let A be a Nagata Dedekind domain with fraction field K and let f : X ⟶ Spec A be flat, quasi-compact and locally of finite type. Then there is a finite extension L / K such that, with B the integral closure of A in L, the normalization Y of X ×_{Spec A} Spec B is smooth over Spec B at every generic point of every one of the fibres of Y ⟶ Spec B.

X is assumed neither reduced nor normal nor affine, and A is not assumed excellent; the smoothness is at all generic points of all fibres.

The fraction field is allowed its own universe: the statement is the one in the scheme's universe transported along the A-algebra isomorphism K ≃ₐ[A] FractionRing A, which carries the K-algebra structure of the extension and its finite dimensionality while leaving the extension, the integral closure and the whole conclusion where they are.

theorem exists_finiteExtension_smoothAt_genericPoints_fiber_normalization_pullback
    {A : Type u} [CommRing A] [IsDedekindDomain A] (K : Type v) [Field K]
    [Algebra A K] [IsFractionRing A K] (hA : IsNagataRing A) {X : Scheme.{u}}
    (f : X ⟶ Spec (.of A)) [Flat f] [LocallyOfFiniteType f] [QuasiCompact f] :
    ∃ (L : Type u) (_ : Field L) (_ : Algebra K L) (_ : FiniteDimensional K L)
      (_ : Algebra A L) (_ : IsScalarTower A K L),
      ∃ hW : ∀ U : (pullback f (Spec.map (CommRingCat.ofHom
          (algebraMap A ↥(integralClosure A L)))) : Scheme.{u}).Opens,
        IsCompact (U : Set (pullback f (Spec.map (CommRingCat.ofHom
          (algebraMap A ↥(integralClosure A L)))) : Scheme.{u})) →
        (irreducibleComponents U).Finite,
      ∀ b : Spec (.of ↥(integralClosure A L)),
      ∀ y : (Scheme.normalization _ hW ≫ pullback.snd f (Spec.map (CommRingCat.ofHom
        (algebraMap A ↥(integralClosure A L))))).fiber b,
      y ∈ genericPoints ↥((Scheme.normalization _ hW ≫ pullback.snd f (Spec.map
        (CommRingCat.ofHom (algebraMap A ↥(integralClosure A L))))).fiber b) →
      InfinitesimalLifting.SmoothAt (Scheme.normalization _ hW ≫ pullback.snd f
          (Spec.map (CommRingCat.ofHom (algebraMap A ↥(integralClosure A L)))))
        ((Scheme.normalization _ hW ≫ pullback.snd f (Spec.map (CommRingCat.ofHom
          (algebraMap A ↥(integralClosure A L))))).fiberι b y)

Tag 0BRQ, a lemma

Tag 0BRQ in the Stacks Project.

AlgebraicGeometry.exists_finiteExtension_smoothAt_genericPoints_fiber_normalization_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ReducedFibreCurve.lean, line 835. The attribute's comment: “corrected statement: the source omits quasi-compactness and is false without it (not_forall_exists_finiteExtension_smoothAt_genericPoints_fiber_normalization); stated here with X quasi-compact, which is implied by S quasi-compact (see the _of_compactSpace corollary)”.

Stacks Project, Tag 0BRQ (variant of the reduced fibre theorem over curves), corrected: the source omits quasi-compactness, and the statement is false without it. Let f : X ⟶ S be flat and of finite type with X quasi-compact. Assume S is Nagata, integral with function field K, and regular of dimension 1. Then there is a finite extension L / K such that, with T the normalization of S in Spec L ((S.genericExtensionHom L).normalization, Tag 035H) and ν : Y ⟶ X ×_S T the normalization, the morphism g = ν ≫ pr₂ : Y ⟶ T is smooth at every generic point of every fibre.

The finiteness witness hW is the one the normalization of a scheme takes as an argument; it is a theorem here (X ×_S T is locally Noetherian), not a hypothesis.

Correction. The source states the lemma for arbitrary S, and its proof begins "choose a finite affine open covering of S". Without quasi-compactness the statement is false: this is AlgebraicGeometry.not_forall_exists_finiteExtension_smoothAt_genericPoints_fiber_normalization, the negation of the statement exactly as the source writes it, in the vocabulary of this theorem. There S is the affine line over a field k with infinitely many origins (countably many copies of Spec k[t] glued along Spec k[t, t⁻¹]), integral, regular of dimension one and Nagata but not quasi-compact, and X is glued from countably many copies of the plane Spec k[x, y] along the torus Spec k[x, t, (xt)⁻¹], the n-th copy lying over the n-th copy of the line by t = x ^ (n + 1) y; f is flat, affine and of finite type. Over the n-th origin the fibre contains the line x = 0 with multiplicity n + 1, and smoothness of g at the generic points of the fibres over the points of T above it forces n + 1 ≤ [L : K]; no L serves every n. Quasi-compactness of S repairs the statement, and it is enough that X be quasi-compact, since then only the finitely many affine opens of S covering the image of X matter; with S quasi-compact this is AlgebraicGeometry.exists_finiteExtension_smoothAt_genericPoints_normalization_of_compactSpace.

The proof is the source's: cover the image of X by finitely many affine opens Spec A_i with A_i a Nagata Dedekind domain with fraction field K, apply Tag 09IL (AlgebraicGeometry.exists_finiteExtension_smoothAt_genericPoints_fiber_normalization_pullback) over each, and take L dominating the resulting extensions; this is AlgebraicGeometry.exists_finiteExtension_smoothAt_normalization_of_forall_affine with the trivial property.

theorem exists_finiteExtension_smoothAt_genericPoints_fiber_normalization_of_isRegular
    {X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFiniteType f] [QuasiCompact f]
    [CompactSpace X] [IsIntegral S] (hN : IsNagataScheme S) (hR : IsRegular S)
    (hdim : topologicalKrullDim S = 1) :
    ∃ (L : Type u) (_ : Field L) (_ : Algebra S.functionField L)
      (_ : FiniteDimensional S.functionField L),
      ∃ hW : ∀ V : (pullback f (S.genericExtensionHom L).fromNormalization : Scheme.{u}).Opens,
        IsCompact (V : Set (pullback f (S.genericExtensionHom L).fromNormalization :
          Scheme.{u})) → (irreducibleComponents V).Finite,
      ∀ b : (S.genericExtensionHom L).normalization,
      ∀ y : (Scheme.normalization _ hW ≫
        pullback.snd f (S.genericExtensionHom L).fromNormalization).fiber b,
      y ∈ genericPoints ↥((Scheme.normalization _ hW ≫
        pullback.snd f (S.genericExtensionHom L).fromNormalization).fiber b) →
      InfinitesimalLifting.SmoothAt (Scheme.normalization _ hW ≫
          pullback.snd f (S.genericExtensionHom L).fromNormalization)
        ((Scheme.normalization _ hW ≫
          pullback.snd f (S.genericExtensionHom L).fromNormalization).fiberι b y)

Tag 0BRR, a lemma

Tag 0BRR in the Stacks Project.

AlgebraicGeometry.exists_finiteSeparableExtension_smoothAt_genericPoints_fiber_normalization_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ReducedFibreSeparableTheorem.lean, line 411.

Stacks Project, Tag 0BRR (the reduced fibre theorem with a separable extension). Let A be a Dedekind domain with fraction field K and let f : X ⟶ Spec A be flat, quasi-compact and locally of finite type. Assume A is a Nagata ring and that for every generic point η of an irreducible component of X the residue field κ(η) is a separable extension of K. Then there is a finite separable extension L / K such that, with B the integral closure of A in L, the normalization Y of X ×_{Spec A} Spec B is smooth over Spec B at every generic point of every one of the fibres of Y ⟶ Spec B.

The separability hypothesis is stated over the residue field of Spec A at f η, through the residue field map of f: since f is flat, f η is the generic point of Spec A, whose residue field is the fraction field K, so this is the separability of κ(η) / K of the source, for the notion of separability of Tag 030O which does not require κ(η) / K to be algebraic.

The fraction field is allowed its own universe: the statement is the one in the scheme's universe transported along the A-algebra isomorphism K ≃ₐ[A] FractionRing A, as for Tag 09IL.

theorem exists_finiteSeparableExtension_smoothAt_genericPoints_fiber_normalization_pullback
    {A : Type u} [CommRing A] [IsDedekindDomain A] (K : Type v) [Field K]
    [Algebra A K] [IsFractionRing A K] (hA : IsNagataRing A) {X : Scheme.{u}}
    (f : X ⟶ Spec (.of A)) [Flat f] [LocallyOfFiniteType f] [QuasiCompact f]
    (hsep : ∀ x : X, x ∈ genericPoints X →
      letI : Algebra ((Spec (.of A)).residueField (f x)) (X.residueField x) :=
        (f.residueFieldMap x).hom.toAlgebra
      Algebra.IsSeparableExtension ((Spec (.of A)).residueField (f x)) (X.residueField x)) :
    ∃ (L : Type u) (_ : Field L) (_ : Algebra K L) (_ : FiniteDimensional K L)
      (_ : Algebra.IsSeparable K L) (_ : Algebra A L) (_ : IsScalarTower A K L),
      ∃ hW : ∀ U : (pullback f (Spec.map (CommRingCat.ofHom
          (algebraMap A ↥(integralClosure A L)))) : Scheme.{u}).Opens,
        IsCompact (U : Set (pullback f (Spec.map (CommRingCat.ofHom
          (algebraMap A ↥(integralClosure A L)))) : Scheme.{u})) →
        (irreducibleComponents U).Finite,
      ∀ b : Spec (.of ↥(integralClosure A L)),
      ∀ y : (Scheme.normalization _ hW ≫ pullback.snd f (Spec.map (CommRingCat.ofHom
        (algebraMap A ↥(integralClosure A L))))).fiber b,
      y ∈ genericPoints ↥((Scheme.normalization _ hW ≫ pullback.snd f (Spec.map
        (CommRingCat.ofHom (algebraMap A ↥(integralClosure A L))))).fiber b) →
      InfinitesimalLifting.SmoothAt (Scheme.normalization _ hW ≫ pullback.snd f
          (Spec.map (CommRingCat.ofHom (algebraMap A ↥(integralClosure A L)))))
        ((Scheme.normalization _ hW ≫ pullback.snd f (Spec.map (CommRingCat.ofHom
          (algebraMap A ↥(integralClosure A L))))).fiberι b y)

Tag 0BRS, a lemma

Tag 0BRS in the Stacks Project.

AlgebraicGeometry.exists_finiteSeparableExtension_smoothAt_genericPoints_fiber_normalization_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ReducedFibreCurveSeparable.lean, line 143. The attribute's comment: “corrected statement: the source omits quasi-compactness and is false without it (not_forall_exists_finiteSeparableExtension_smoothAt_genericPoints_fiber_normalization); stated here with X quasi-compact, which is implied by S quasi-compact (see the _of_compactSpace corollary)”.

Stacks Project, Tag 0BRS (variant with separable extensions over curves), corrected: the source omits quasi-compactness, and the statement is false without it. Let f : X ⟶ S be flat and of finite type with X quasi-compact. Assume S is Nagata, integral with function field K, and regular of dimension 1, and that the field extension κ(η) / K is separable for every generic point η of an irreducible component of X. Then there is a finite separable extension L / K such that, with T the normalization of S in Spec L ((S.genericExtensionHom L).normalization) and ν : Y ⟶ X ×_S T the normalization, the morphism g = ν ≫ pr₂ : Y ⟶ T is smooth at every generic point of every fibre.

The separability hypothesis is that of κ(η) over κ(f η); flatness puts f η at the generic point of S, whose residue field is K. The finiteness witness hW is the argument the normalization of a scheme takes; it is a theorem (X ×_S T is locally Noetherian), not a hypothesis.

Correction. The source's proof is that of Tag 0BRQ, which begins with a finite affine open covering of S; without quasi-compactness the statement is false: this is not_forall_exists_finiteSeparableExtension_smoothAt_genericPoints_fiber_normalization, the negation of the statement exactly as the source writes it, in the vocabulary of this theorem. The counterexample is that of Tag 0BRQ (AlgebraicGeometry.not_forall_exists_finiteExtension_smoothAt_genericPoints_fiber_normalization) over ℚ, where the separability hypothesis holds because every extension of a field of characteristic zero is separable, and the conclusion of Tag 0BRS contains that of Tag 0BRQ. Quasi-compactness of X repairs the statement (only the finitely many affine opens covering the image of X matter), and it is implied by that of S (AlgebraicGeometry.exists\_finiteSeparableExtension\_smoothAt\_genericPoints\_normalization\_of\_\ compactSpace).

theorem exists_finiteSeparableExtension_smoothAt_genericPoints_fiber_normalization_of_isRegular
    {X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFiniteType f] [QuasiCompact f]
    [CompactSpace X] [IsIntegral S] (hN : IsNagataScheme S) (hR : IsRegular S)
    (hdim : topologicalKrullDim S = 1)
    (hsep : ∀ x : X, x ∈ genericPoints X →
      letI : Algebra (S.residueField (f.base x)) (X.residueField x) :=
        (f.residueFieldMap x).hom.toAlgebra
      Algebra.IsSeparableExtension (S.residueField (f.base x)) (X.residueField x)) :
    ∃ (L : Type u) (_ : Field L) (_ : Algebra S.functionField L)
      (_ : FiniteDimensional S.functionField L) (_ : Algebra.IsSeparable S.functionField L),
      ∃ hW : ∀ V : (pullback f (S.genericExtensionHom L).fromNormalization : Scheme.{u}).Opens,
        IsCompact (V : Set (pullback f (S.genericExtensionHom L).fromNormalization :
          Scheme.{u})) → (irreducibleComponents V).Finite,
      ∀ b : (S.genericExtensionHom L).normalization,
      ∀ y : (Scheme.normalization _ hW ≫
        pullback.snd f (S.genericExtensionHom L).fromNormalization).fiber b,
      y ∈ genericPoints ↥((Scheme.normalization _ hW ≫
        pullback.snd f (S.genericExtensionHom L).fromNormalization).fiber b) →
      InfinitesimalLifting.SmoothAt (Scheme.normalization _ hW ≫
          pullback.snd f (S.genericExtensionHom L).fromNormalization)
        ((Scheme.normalization _ hW ≫
          pullback.snd f (S.genericExtensionHom L).fromNormalization).fiberι b y)

Sources

LeanAlgebraicGeometry.normalizedBaseChange · AlgebraicGeometry.normalizedBaseChangeOverIntegralClosure · AlgebraicGeometry.exists_finiteExtension_smoothAt_genericPoints_fiber_normalization_pullback · AlgebraicGeometry.exists_finiteExtension_smoothAt_genericPoints_fiber_normalization_of_isRegular · AlgebraicGeometry.exists_finiteSeparableExtension_smoothAt_genericPoints_fiber_normalization_pullback · AlgebraicGeometry.exists_finiteSeparableExtension_smoothAt_genericPoints_fiber_normalization_of_isRegular

Section37.66 Ind-quasi-affine morphisms #

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

Tag 0AP6, a definition

Tag 0AP6 in the Stacks Project.

AlgebraicGeometry.IsIndQuasiAffine, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/IndQuasiAffine.lean, line 39. The attribute's comment: “schemes”.

A scheme is ind-quasi-affine if each quasi-compact open subscheme is quasi-affine.

class IsIndQuasiAffine (X : Scheme.{u}) : Prop

AlgebraicGeometry.IsIndQuasiAffineHom, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/IndQuasiAffine.lean, line 48. The attribute's comment: “morphisms”.

A morphism of schemes is ind-quasi-affine if the inverse image of every affine open subscheme of its target is an ind-quasi-affine scheme.

class IsIndQuasiAffineHom {X Y : Scheme.{u}} (f : X ⟶ Y) : Prop

Tag 0F1U, a lemma

Tag 0F1U in the Stacks Project.

AlgebraicGeometry.isIndQuasiAffineHom_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/IndQuasiAffine/Characterization.lean, line 106. The attribute's comment: “equivalent characterizations”.

Ind-quasi-affineness of a morphism of schemes can be tested on the quasi-compact open subschemes above the affine opens of the target, above the members of one cover of the target by quasi-compact quasi-separated opens, or above all quasi-compact quasi-separated opens of the target.

theorem isIndQuasiAffineHom_tfae {X Y : Scheme.{u}} (f : X ⟶ Y) :
    List.TFAE [
      IsIndQuasiAffineHom f,
      ∀ (V : Y.Opens), IsAffineOpen V →
        ∀ (U : (f ⁻¹ᵁ V).toScheme.Opens), IsCompact (U : Set (f ⁻¹ᵁ V).toScheme) →
          IsQuasiAffineHom (U.ι ≫ f ∣_ V),
      ∃ (ι : Type u) (V : ι → Y.Opens),
        (iSup V = ⊤) ∧
          (∀ j, IsCompact (V j : Set Y)) ∧
          (∀ j, IsQuasiSeparated (V j : Set Y)) ∧
          (∀ j (U : (f ⁻¹ᵁ V j).toScheme.Opens),
              IsCompact (U : Set (f ⁻¹ᵁ V j).toScheme) →
                IsQuasiAffineHom (U.ι ≫ f ∣_ (V j))),
      ∀ (V : Y.Opens), IsCompact (V : Set Y) → IsQuasiSeparated (V : Set Y) →
        ∀ (U : (f ⁻¹ᵁ V).toScheme.Opens), IsCompact (U : Set (f ⁻¹ᵁ V).toScheme) →
          IsQuasiAffineHom (U.ι ≫ f ∣_ V)]

AlgebraicGeometry.isIndQuasiAffineHom_isZariskiLocalAtTarget, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/IndQuasiAffine/Characterization.lean, line 242. The attribute's comment: “Zariski locality on the base”.

Being an ind-quasi-affine morphism is Zariski local on the base.

instance isIndQuasiAffineHom_isZariskiLocalAtTarget :
    IsZariskiLocalAtTarget (@IsIndQuasiAffineHom : MorphismProperty Scheme.{u})

Tag 0F1V, a lemma

Tag 0F1V in the Stacks Project.

AlgebraicGeometry.isIndQuasiAffineHom_isStableUnderComposition, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/IndQuasiAffine/Comp.lean, line 71.

Being an ind-quasi-affine morphism of schemes is stable under composition.

instance isIndQuasiAffineHom_isStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsIndQuasiAffineHom : MorphismProperty Scheme.{u})

Tag 0F1W, a lemma

Tag 0F1W in the Stacks Project.

AlgebraicGeometry.isIndQuasiAffineHom_of_isQuasiAffineHom, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/IndQuasiAffine/QuasiAffineAndImmersion.lean, line 36. The attribute's comment: “quasi-affine morphisms”.

A quasi-affine morphism of schemes is ind-quasi-affine.

instance isIndQuasiAffineHom_of_isQuasiAffineHom {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsQuasiAffineHom f] : IsIndQuasiAffineHom f

AlgebraicGeometry.isIndQuasiAffineHom_of_isImmersion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/IndQuasiAffine/QuasiAffineAndImmersion.lean, line 45. The attribute's comment: “immersions”.

An immersion of schemes is ind-quasi-affine.

instance isIndQuasiAffineHom_of_isImmersion {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsImmersion f] : IsIndQuasiAffineHom f

Tag 0F1X, a lemma

Tag 0F1X in the Stacks Project.

AlgebraicGeometry.isIndQuasiAffineHom_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/IndQuasiAffine/Comp.lean, line 79.

If the composite f ≫ g of two morphisms of schemes is ind-quasi-affine, then f is ind-quasi-affine.

theorem isIndQuasiAffineHom_of_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    [IsIndQuasiAffineHom (f ≫ g)] : IsIndQuasiAffineHom f

Tag 0AP7, a lemma

Tag 0AP7 in the Stacks Project.

AlgebraicGeometry.isIndQuasiAffineHom_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/IndQuasiAffine/BaseChange.lean, line 41.

Ind-quasi-affine morphisms of schemes are stable under arbitrary base change.

instance isIndQuasiAffineHom_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      (@IsIndQuasiAffineHom : MorphismProperty Scheme.{u})

Tag 0AP8, a lemma

Tag 0AP8 in the Stacks Project.

AlgebraicGeometry.isIndQuasiAffineHom_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/IndQuasiAffine/FpqcDescent.lean, line 55.

Being an ind-quasi-affine morphism of schemes is fpqc local on the base.

instance isIndQuasiAffineHom_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@IsIndQuasiAffineHom : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 0AP9, a lemma

Tag 0AP9 in the Stacks Project.

AlgebraicGeometry.isIndQuasiAffineHom_of_isSeparated_of_locallyQuasiFinite, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/IndQuasiAffineSeparated.lean, line 59.

A separated morphism of schemes which is locally quasi-finite and locally of finite type is ind-quasi-affine.

instance isIndQuasiAffineHom_of_isSeparated_of_locallyQuasiFinite {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsSeparated f] [LocallyQuasiFinite f] [LocallyOfFiniteType f] :
    IsIndQuasiAffineHom f

Sources

LeanAlgebraicGeometry.IsIndQuasiAffine · AlgebraicGeometry.IsIndQuasiAffineHom · AlgebraicGeometry.isIndQuasiAffineHom_tfae · AlgebraicGeometry.isIndQuasiAffineHom_isZariskiLocalAtTarget · AlgebraicGeometry.isIndQuasiAffineHom_isStableUnderComposition · AlgebraicGeometry.isIndQuasiAffineHom_of_isQuasiAffineHom · AlgebraicGeometry.isIndQuasiAffineHom_of_isImmersion · AlgebraicGeometry.isIndQuasiAffineHom_of_comp

Section37.67 Pushouts in the category of schemes, II #

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

Tag 0ECI, a situation

Tag 0ECI in the Stacks Project.

AlgebraicGeometry.PushoutAlongClosedImmersionAndIntegralSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/PushoutSituation.lean, line 40.

Stacks Project, Tag 0ECI. The standing situation for a pushout along a closed immersion and an integral morphism.

structure PushoutAlongClosedImmersionAndIntegralSituation

Tag 0ECJ, a lemma

Tag 0ECJ in the Stacks Project.

Stacks.Pushout.exists_affineOpens_preimage_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/CompatibleAffines.lean, line 164.

Stacks Project, Tag 0ECJ. Let i : Z ⟶ X be a closed immersion and j : Z ⟶ Y an integral morphism such that every fibre of j maps under i into an affine open of X. Then every y : Y has an affine open neighbourhood V whose preimage under j is the preimage under i of an affine open U of X.

The argument of the source, run twice. Shrinking Y around y makes j ⁻¹ᵁ V₀ land inside i ⁻¹ᵁ U₀; separating the fibre by a basic open of U₀ inside the open W with i ⁻¹ᵁ W ≤ j ⁻¹ᵁ V₀ reverses that inclusion. Shrinking a second time and pulling the resulting function on V₀ back along the closed immersion makes the two preimages equal, because the basic open of the pullback of g is cut out of i ⁻¹ᵁ U₁ by j ⁻¹ᵁ (Y.basicOpen g).

theorem exists_affineOpens_preimage_eq (i : Z ⟶ X) (j : Z ⟶ Y) [IsClosedImmersion i]
    [IsIntegralHom j]
    (hfib : ∀ y : Y, ∃ U : X.Opens, IsAffineOpen U ∧ ∀ z : Z, j z = y → i z ∈ U) (y : Y) :
    ∃ (U : X.Opens) (V : Y.Opens), IsAffineOpen U ∧ IsAffineOpen V ∧ y ∈ V ∧
      i ⁻¹ᵁ U = j ⁻¹ᵁ V

Tag 0E25, a proposition

Tag 0E25 in the Stacks Project.

AlgebraicGeometry.pushoutAlongClosedImmersionAndIntegral, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/Gluing.lean, line 302. The attribute's comment: “the pushout”.

Stacks Project, Tag 0E25. The pushout along a closed immersion and an integral morphism exists as a scheme.

noncomputable def pushoutAlongClosedImmersionAndIntegral
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u}) :
    PushoutAlongClosedImmersionAndIntegral s

AlgebraicGeometry.pushoutSquare_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/Gluing.lean, line 333. The attribute's comment: “the diagram is a fibre square”.

Stacks Project, Tag 0E25. The pushout square is also a pullback square.

theorem pushoutSquare_isPullback
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u}) :
    IsPullback s.i s.j (pushoutInl s) (pushoutInr s)

AlgebraicGeometry.pushoutInl_isIntegralHom, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/Gluing.lean, line 340. The attribute's comment: “the morphism a is integral”.

Stacks Project, Tag 0E25. The canonical map from X to the pushout is integral.

instance pushoutInl_isIntegralHom
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u}) :
    IsIntegralHom (pushoutInl s)

AlgebraicGeometry.pushoutInr_isClosedImmersion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/Gluing.lean, line 351. The attribute's comment: “the morphism b is a closed immersion”.

Stacks Project, Tag 0E25. The canonical map from Y to the pushout is a closed immersion.

instance pushoutInr_isClosedImmersion
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u}) :
    IsClosedImmersion (pushoutInr s)

AlgebraicGeometry.pushoutStructureSheaf_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/Gluing.lean, line 366. The attribute's comment: “the structure sheaf”.

Stacks Project, Tag 0E25. On every open of the pushout, its ring of sections is the fibre product of the rings of sections on Y and X over the corresponding ring on Z.

These are the component squares, after applying CategoryTheory.sheafToPresheaf, of the source's square of sheaves of rings: its natural transformations have components b.app U, a.app U, j.app (b ⁻¹ᵁ U), and the transported map i.app (a ⁻¹ᵁ U) occurring below. The equivalence with the sheaf-level pullback is CategoryTheory.IsPullback.iff_app together with reflection of limits along the fully faithful CategoryTheory.sheafToPresheaf.

theorem pushoutStructureSheaf_isPullback
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u})
    (U : (pushoutScheme s).Opens) :
    let e : s.i ⁻¹ᵁ (pushoutInl s ⁻¹ᵁ U) =
        s.j ⁻¹ᵁ (pushoutInr s ⁻¹ᵁ U) :=
      congrArg (fun f : s.Z ⟶ pushoutScheme s ↦ f ⁻¹ᵁ U)
        (pushoutAlongClosedImmersionAndIntegral s).isPushout.w
    IsPullback (pushoutInr s |>.app U) (pushoutInl s |>.app U)
      (s.j.app (pushoutInr s ⁻¹ᵁ U))
      (s.i.app (pushoutInl s ⁻¹ᵁ U) ≫
        eqToHom (congrArg (fun V ↦ Γ(s.Z, V)) e))

Tag 0E26, a lemma

Tag 0E26 in the Stacks Project.

AlgebraicGeometry.pushoutScheme_isSeparated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/Separation.lean, line 61. The attribute's comment: “separated”.

Stacks Project, Tag 0E26. If both schemes being glued are separated, then the pushout along a closed immersion and an integral morphism is separated.

instance pushoutScheme_isSeparated
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u})
    [s.X.IsSeparated] [s.Y.IsSeparated] :
    (pushoutScheme s).IsSeparated

AlgebraicGeometry.pushoutToBase_isSeparated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/Separation.lean, line 81. The attribute's comment: “separated_over_s”.

Stacks Project, Tag 0E26. If both schemes being glued are separated over the base, then the pushout along a closed immersion and an integral morphism is separated over the base.

instance pushoutToBase_isSeparated
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u})
    [IsSeparated s.pX] [IsSeparated s.pY] :
    IsSeparated (pushoutToBase s)

AlgebraicGeometry.pushoutScheme_quasiSeparatedSpace, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/Separation.lean, line 118. The attribute's comment: “quasi_separated”.

Stacks Project, Tag 0E26. If both schemes being glued are quasi-separated, then the pushout along a closed immersion and an integral morphism is quasi-separated.

instance pushoutScheme_quasiSeparatedSpace
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u})
    [QuasiSeparatedSpace s.X] [QuasiSeparatedSpace s.Y] :
    QuasiSeparatedSpace (pushoutScheme s)

AlgebraicGeometry.pushoutToBase_quasiSeparated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/Separation.lean, line 131. The attribute's comment: “quasi_separated_over_s”.

Stacks Project, Tag 0E26. If both schemes being glued are quasi-separated over the base, then the pushout along a closed immersion and an integral morphism is quasi-separated over the base.

instance pushoutToBase_quasiSeparated
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u})
    [QuasiSeparated s.pX] [QuasiSeparated s.pY] :
    QuasiSeparated (pushoutToBase s)

Tag 0E27, a lemma

Tag 0E27 in the Stacks Project.

AlgebraicGeometry.pushoutToBase_locallyOfFiniteType, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/FiniteType.lean, line 152.

Stacks Project, Tag 0E27. In the standing situation of [Stacks Project, Tag 0ECI], if the base is locally Noetherian and X, Y and Z are locally of finite type over it, then the pushout Y ⨿_Z X of [Stacks Project, Tag 0E25] is locally of finite type over the base.

instance pushoutToBase_locallyOfFiniteType
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u})
    [IsLocallyNoetherian s.S]
    [LocallyOfFiniteType s.pX]
    [LocallyOfFiniteType s.pY]
    [LocallyOfFiniteType s.pZ] :
    LocallyOfFiniteType (pushoutToBase s)

Tag 0ECK, a lemma

Tag 0ECK in the Stacks Project.

AlgebraicGeometry.primedFiber_preimage_subset_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/CartesianDiagram.lean, line 142. The attribute's comment: “part (1)”.

The primed span of a cartesian diagram satisfies the fibrewise affineness condition of a pushout situation: every fibre of j' maps under i' into a single affine open of X'.

theorem primedFiber_preimage_subset_affine
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u}) (d : CartesianDiagram s) :
    ∀ y : d.Y', ∃ U : d.X'.Opens, IsAffineOpen U ∧
      ∀ z : d.Z', d.j' z = y → d.i' z ∈ U

AlgebraicGeometry.pushoutMap_left_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/QuasiFiniteFunctoriality.lean, line 491. The attribute's comment: “part (3), the X square”.

Stacks Project, Tag 0ECK, part (3). The square relating the two canonical maps from X and X' to the two pushouts is cartesian.

theorem pushoutMap_left_isPullback
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u}) (d : CartesianDiagram s) :
    IsPullback (pushoutInl (inducedSituation s d)) d.f (pushoutMap s d) (pushoutInl s)

AlgebraicGeometry.pushoutMap_right_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/QuasiFiniteFunctoriality.lean, line 502. The attribute's comment: “part (3), the Y square”.

Stacks Project, Tag 0ECK, part (3). The square relating the two canonical maps from Y and Y' to the two pushouts is cartesian.

theorem pushoutMap_right_isPullback
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u}) (d : CartesianDiagram s) :
    IsPullback (pushoutInr (inducedSituation s d)) d.g (pushoutMap s d) (pushoutInr s)

AlgebraicGeometry.pushoutMap_isSeparated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/QuasiFiniteFunctoriality.lean, line 512. The attribute's comment: “part (2), separated”.

Stacks Project, Tag 0ECK, part (2). The induced morphism of pushouts is separated.

instance pushoutMap_isSeparated
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u}) (d : CartesianDiagram s) :
    IsSeparated (pushoutMap s d)

AlgebraicGeometry.pushoutMap_locallyOfFiniteType, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/QuasiFiniteFunctoriality.lean, line 537. The attribute's comment: “part (2), locally of finite type”.

Stacks Project, Tag 0ECK, part (2). The induced morphism of pushouts is locally of finite type.

instance pushoutMap_locallyOfFiniteType
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u}) (d : CartesianDiagram s) :
    LocallyOfFiniteType (pushoutMap s d)

AlgebraicGeometry.pushoutMap_locallyQuasiFinite, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/QuasiFiniteFunctoriality.lean, line 556. The attribute's comment: “part (2), locally quasi-finite fibres”.

Stacks Project, Tag 0ECK, part (2). The induced morphism of pushouts has locally quasi-finite fibres.

instance pushoutMap_locallyQuasiFinite
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u}) (d : CartesianDiagram s) :
    LocallyQuasiFinite (pushoutMap s d)

Tag 0ECL, a lemma

Tag 0ECL in the Stacks Project.

AlgebraicGeometry.flat_pushoutMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/FlatQuasiFiniteDescent.lean, line 302. The attribute's comment: “flatness of the pushout map”.

Stacks Project, Tag 0ECL. The morphism of pushouts induced by a cartesian triple whose three vertical morphisms are flat is flat.

theorem flat_pushoutMap (s : PushoutAlongClosedImmersionAndIntegralSituation.{u})
    (d : CartesianDiagram s) [Flat d.f] [Flat d.g] [Flat d.h] :
    Flat (pushoutMap s d)

AlgebraicGeometry.etale_pushoutMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/FlatQuasiFiniteDescent.lean, line 319. The attribute's comment: “étaleness of the pushout map”.

Stacks Project, Tag 0ECL. The morphism of pushouts induced by a cartesian triple whose three vertical morphisms are étale is étale.

theorem etale_pushoutMap (s : PushoutAlongClosedImmersionAndIntegralSituation.{u})
    (d : CartesianDiagram s) [Etale d.f] [Etale d.g] [Etale d.h] :
    Etale (pushoutMap s d)

AlgebraicGeometry.flatTriple_pushout_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/FlatQuasiFiniteDescent.lean, line 815. The attribute's comment: “flat equivalence”.

Stacks Project, Tag 0ECL. The pushout construction is an equivalence from the cartesian triples with flat vertical morphisms to the flat, separated, locally quasi-finite schemes over the pushout. On objects it is the pushout of the triple together with its canonical morphism to Y ⨿_Z X, and on morphisms it is the morphism of pushouts induced by the three components.

theorem flatTriple_pushout_equivalence
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u}) :
    ∃ F : FlatCartesianTriple s ⥤ flatSchemesOver s,
      F.IsEquivalence ∧
      (∀ d, (F.obj d).1 = Over.mk (pushoutMap s d.1)) ∧
      (∀ (d e : FlatCartesianTriple s) (m : CartesianTripleHom d.1 e.1),
        ∃ k : pushoutScheme (inducedSituation s d.1) ⟶
            pushoutScheme (inducedSituation s e.1),
          HEq (((F.map m).1).left) k ∧
          (pushoutInl (inducedSituation s d.1) ≫ k =
            m.x ≫ pushoutInl (inducedSituation s e.1)) ∧
          (pushoutInr (inducedSituation s d.1) ≫ k =
            m.y ≫ pushoutInr (inducedSituation s e.1)))

AlgebraicGeometry.etaleTriple_pushout_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/FlatQuasiFiniteDescent.lean, line 846. The attribute's comment: “étale equivalence”.

Stacks Project, Tag 0ECL. The pushout construction is an equivalence from the cartesian triples with étale vertical morphisms to the étale, separated, locally quasi-finite schemes over the pushout. On objects it is the pushout of the triple together with its canonical morphism to Y ⨿_Z X, and on morphisms it is the morphism of pushouts induced by the three components.

theorem etaleTriple_pushout_equivalence
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u}) :
    ∃ F : EtaleCartesianTriple s ⥤ etaleSchemesOver s,
      F.IsEquivalence ∧
      (∀ d, (F.obj d).1 = Over.mk (pushoutMap s d.1)) ∧
      (∀ (d e : EtaleCartesianTriple s) (m : CartesianTripleHom d.1 e.1),
        ∃ k : pushoutScheme (inducedSituation s d.1) ⟶
            pushoutScheme (inducedSituation s e.1),
          HEq (((F.map m).1).left) k ∧
          (pushoutInl (inducedSituation s d.1) ≫ k =
            m.x ≫ pushoutInl (inducedSituation s e.1)) ∧
          (pushoutInr (inducedSituation s d.1) ≫ k =
            m.y ≫ pushoutInr (inducedSituation s e.1)))

Tag 0B7M, a lemma

Tag 0B7M in the Stacks Project.

AlgebraicGeometry.hasPushout_of_isClosedImmersion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/ClosedImmersions.lean, line 111. The attribute's comment: “the pushout exists”.

[Stacks, Tag 0B7M]. The pushout of two closed immersions of schemes exists in the category of schemes.

instance hasPushout_of_isClosedImmersion {Z X Y : Scheme.{u}} (i : Z ⟶ X) (j : Z ⟶ Y)
    [IsClosedImmersion i] [IsClosedImmersion j] : HasPushout i j

AlgebraicGeometry.isPullback_pushout_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/ClosedImmersions.lean, line 119. The attribute's comment: “the diagram is a fibre square”.

[Stacks, Tag 0B7M]. The defining pushout square of two closed immersions of schemes is also a fibre square.

theorem isPullback_pushout_of_isClosedImmersion {Z X Y : Scheme.{u}} (i : Z ⟶ X) (j : Z ⟶ Y)
    [IsClosedImmersion i] [IsClosedImmersion j] :
    IsPullback i j (pushout.inl i j) (pushout.inr i j)

AlgebraicGeometry.pushout_inl_isClosedImmersion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/ClosedImmersions.lean, line 142. The attribute's comment: “the morphism a is a closed immersion”.

[Stacks, Tag 0B7M]. The canonical map a : X ⟶ Y ⨿_Z X out of the first scheme is a closed immersion.

instance pushout_inl_isClosedImmersion {Z X Y : Scheme.{u}} (i : Z ⟶ X) (j : Z ⟶ Y)
    [IsClosedImmersion i] [IsClosedImmersion j] : IsClosedImmersion (pushout.inl i j)

AlgebraicGeometry.pushout_inr_isClosedImmersion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/ClosedImmersions.lean, line 157. The attribute's comment: “the morphism b is a closed immersion”.

[Stacks, Tag 0B7M]. The canonical map b : Y ⟶ Y ⨿_Z X out of the second scheme is a closed immersion.

instance pushout_inr_isClosedImmersion {Z X Y : Scheme.{u}} (i : Z ⟶ X) (j : Z ⟶ Y)
    [IsClosedImmersion i] [IsClosedImmersion j] : IsClosedImmersion (pushout.inr i j)

AlgebraicGeometry.pushout_structureSheafModule_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/ClosedImmersions.lean, line 321. The attribute's comment: “the short exact sequence”.

[Stacks, Tag 0B7M]. For two closed immersions i : Z ⟶ X and j : Z ⟶ Y, the canonical sequence

0 ⟶ 𝒪_(Y ⨿_Z X) ⟶ a_* 𝒪_X ⊕ b_* 𝒪_Y ⟶ c_* 𝒪_Z ⟶ 0

of modules over the structure sheaf of the pushout is short exact, where a and b are the two canonical maps into the pushout and c = a ∘ i = b ∘ j.

theorem pushout_structureSheafModule_shortExact {Z X Y : Scheme.{u}} (i : Z ⟶ X) (j : Z ⟶ Y)
    [IsClosedImmersion i] [IsClosedImmersion j] :
    ∃ zero : pushoutStructureSheafModuleToBiprod i j ≫ pushoutBiprodToIntersection i j = 0,
      (ShortComplex.mk (pushoutStructureSheafModuleToBiprod i j)
        (pushoutBiprodToIntersection i j) zero).ShortExact

Tag 0CYY, a lemma

Tag 0CYY in the Stacks Project.

AlgebraicGeometry.induced_locallyOfFiniteType_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/InducedFiniteType.lean, line 287. The attribute's comment: “locally_of_finite_type”.

In the situation of two closed immersions i : Z ⟶ X and j : Z ⟶ Y, morphisms f : X' ⟶ X and g : Y' ⟶ Y, and an isomorphism over Z between the two inverse images of Z, the induced morphism from the glued scheme X' ⨿_{X' ×_X Z} Y' to the pushout Y ⨿_Z X is locally of finite type if and only if f and g are locally of finite type.

theorem induced_locallyOfFiniteType_iff (S : CompatiblePushoutMorphismSituation.{u}) :
    LocallyOfFiniteType S.induced ↔
      LocallyOfFiniteType S.f ∧ LocallyOfFiniteType S.g

AlgebraicGeometry.flat_induced_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/InducedFlat.lean, line 261. The attribute's comment: “flat”.

In the situation of AlgebraicGeometry.CompatiblePushoutMorphismSituation, the induced morphism between the two pushouts is flat if and only if both morphisms on the pieces are flat.

theorem flat_induced_iff (S : CompatiblePushoutMorphismSituation.{u}) :
    Flat S.induced ↔ Flat S.f ∧ Flat S.g

AlgebraicGeometry.flat_locallyOfFinitePresentation_induced_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/InducedFlat.lean, line 280. The attribute's comment: “flat_locally_of_finite_presentation”.

In the situation of AlgebraicGeometry.CompatiblePushoutMorphismSituation, the induced morphism between the two pushouts is flat and locally of finite presentation if and only if both morphisms on the pieces are flat and locally of finite presentation.

theorem flat_locallyOfFinitePresentation_induced_iff
    (S : CompatiblePushoutMorphismSituation.{u}) :
    (Flat S.induced ∧ LocallyOfFinitePresentation S.induced) ↔
      ((Flat S.f ∧ LocallyOfFinitePresentation S.f) ∧
        (Flat S.g ∧ LocallyOfFinitePresentation S.g))

AlgebraicGeometry.etale_induced_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/InducedSmooth.lean, line 329. The attribute's comment: “etale”.

In a compatible morphism of pushouts along closed immersions, the induced morphism is étale if and only if the morphisms on both pieces are étale.

theorem etale_induced_iff (S : CompatiblePushoutMorphismSituation.{u}) :
    Etale S.induced ↔ (Etale S.f ∧ Etale S.g)

AlgebraicGeometry.smooth_induced_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/InducedSmooth.lean, line 340. The attribute's comment: “smooth”.

In a compatible morphism of pushouts along closed immersions, the induced morphism is smooth if and only if the morphisms on both pieces are smooth.

theorem smooth_induced_iff (S : CompatiblePushoutMorphismSituation.{u}) :
    Smooth S.induced ↔ (Smooth S.f ∧ Smooth S.g)

Sources

LeanAlgebraicGeometry.PushoutAlongClosedImmersionAndIntegralSituation · Stacks.Pushout.exists_affineOpens_preimage_eq · AlgebraicGeometry.pushoutAlongClosedImmersionAndIntegral · AlgebraicGeometry.pushoutSquare_isPullback · AlgebraicGeometry.pushoutInl_isIntegralHom · AlgebraicGeometry.pushoutInr_isClosedImmersion · AlgebraicGeometry.pushoutStructureSheaf_isPullback · AlgebraicGeometry.pushoutScheme_isSeparated

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

37.53 Stein factorization to 37.67 Pushouts in the category…

Section37.53 Stein factorization#

Tag 03GY, a lemma

Tag 0E0M, a lemma

Tag 03GZ, a lemma

Tag 03H0, a theorem

Tag 03H2, a theorem

Tag 0AY8, a lemma

Tag 0BUI, a lemma

Tag 0E0N, a lemma

Tag 0CT9, a lemma

Sources

Section37.54 Generic flatness stratification#

Tag 0ASY, a lemma

Tag 0H3Z, a lemma

Tag 0H89, a lemma

Tag 0H40, a lemma

Tag 0H41, a lemma

Sources

Section37.55 Stratifying a morphism#

Tag 0H43, a lemma

Tag 0H44, a lemma

Sources

Section37.56 Improving morphisms of relative dimension one#

Tag 0GK7, a lemma

Sources

Section37.57 Descending separated locally quasi-finite morphisms#

Tag 02W8, a lemma

Sources

Section37.58 Relative finite presentation#

Tag 05H1, a definition

Tag 09T7, a lemma

Tag 09T8, a lemma

Tag 09T9, a lemma

Tag 09TA, a lemma

Tag 09TB, a lemma

Tag 09TC, a lemma

Tag 09TD, a lemma

Tag 09TE, a lemma

Sources

Section37.59 Relative pseudo-coherence#

Tag 09VC, a lemma

Tag 09UI, a definition

Tag 0CSU, a lemma

Tag 09VD, a lemma

Tag 09VE, a lemma

Tag 09UJ, a lemma

Tag 09VF, a lemma

Tag 09VG, a lemma

Tag 09UK, a lemma

Tag 09UL, a lemma

Tag 09UM, a lemma

Tag 09UN, a lemma

Tag 09UP, a lemma

Tag 09UQ, a lemma

Tag 09UR, a lemma

Tag 09US, a lemma

Tag 09UT, a lemma

Tag 09UU, a lemma

Sources

Section37.60 Pseudo-coherent morphisms#

Tag 067Y, a lemma

Tag 067Z, a definition

Tag 0680, a lemma

Tag 0681, a lemma

Tag 0682, a lemma

Tag 0695, a lemma

Tag 0683, a lemma

Tag 0AVX, a lemma

Tag 0684, a lemma

Tag 0696, a lemma

Tag 0697, a lemma

Tag 0698, a lemma

Tag 0699, a lemma

Sources

Section37.61 Perfect morphisms#

Tag 0685, the section

Tag 0686, a lemma

Tag 0687, a definition

Tag 0688, a lemma

Section37.53 Stein factorization #

Section37.54 Generic flatness stratification #

Section37.55 Stratifying a morphism #

Section37.56 Improving morphisms of relative dimension one #

Section37.57 Descending separated locally quasi-finite morphisms #

Section37.58 Relative finite presentation #

Section37.59 Relative pseudo-coherence #

Section37.60 Pseudo-coherent morphisms #

Section37.61 Perfect morphisms #

Section37.62 Local complete intersection morphisms #

Section37.64 Weakly étale morphisms #

Section37.65 Reduced fibre theorem #

Section37.66 Ind-quasi-affine morphisms #

Section37.67 Pushouts in the category of schemes, II #