Local properties satisfying fpqc descent

In this file we provide instances that show that the following local properties satisfy fpqc descent:

• locally of finite type
• locally of finite presentation
• smooth
• formally unramified
• étale

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

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

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

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

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