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]
: