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)

instance AlgebraicGeometry.Flat.surjective_descendsAlong_surjective_inf_flat_inf_quasicompact : CategoryTheory.MorphismProperty.DescendsAlong (@Surjective) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Surjective satisfies fpqc descent.

instance AlgebraicGeometry.descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact : CategoryTheory.MorphismProperty.DescendsAlong (@UniversallyClosed) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Universally closed satisfies fpqc descent.

instance AlgebraicGeometry.descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact : CategoryTheory.MorphismProperty.DescendsAlong (@UniversallyOpen) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Universally open satisfies fpqc descent.

instance AlgebraicGeometry.descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact : CategoryTheory.MorphismProperty.DescendsAlong (@UniversallyInjective) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Universally injective satisfies fpqc descent.

instance AlgebraicGeometry.descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact : (CategoryTheory.MorphismProperty.isomorphisms Scheme).DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Being an isomorphism satisfies fpqc descent.

instance AlgebraicGeometry.descendsAlong_isOpenImmersion_surjective_inf_flat_inf_quasicompact' : IsOpenImmersion.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Being an open immersion satisfies fpqc descent.