Properties of morphisms satisfying fpqc descent #
In this file we show some global properties satisfy fpqc descent.
- universally closed
(
AlgebraicGeometry.descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact) - universally open
(
AlgebraicGeometry.descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact) - universally injective
(
AlgebraicGeometry.descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact) - being an isomorphism
(
AlgebraicGeometry.descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact) - being an open immersion
(
AlgebraicGeometry.descendsAlong_isOpenImmersion_surjective_inf_flat_inf_quasicompact)
Surjective satisfies fpqc descent.
Universally closed satisfies fpqc descent.
Universally open satisfies fpqc descent.
instance AlgebraicGeometry.descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact :
Universally injective satisfies fpqc descent.
Being an isomorphism satisfies fpqc descent.
Being an open immersion satisfies fpqc descent.
theorem AlgebraicGeometry.HasRingHomProperty.descendsAlong_flat {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] => Q] (h :
RingHom.CodescendsAlong (fun {R S : Type u} [CommRing R] [CommRing S] => Q)
fun {R S : Type u} [CommRing R] [CommRing S] => RingHom.FaithfullyFlat) :
P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
instance AlgebraicGeometry.instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget (P : CategoryTheory.MorphismProperty Scheme) [P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)] [IsZariskiLocalAtTarget P] :
P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @LocallyOfFinitePresentation)
fpqc descent implies fppf descent
instance AlgebraicGeometry.instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfQuasiCompact {X Y : Scheme} (f : X ⟶ Y) [Surjective f] [Flat f] [QuasiCompact f] :
instance AlgebraicGeometry.instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfLocallyOfFinitePresentation {X Y : Scheme} (f : X ⟶ Y) [Surjective f] [Flat f] [LocallyOfFinitePresentation f] :