FlatDescent

📁 Source: Mathlib/AlgebraicGeometry/Morphisms/FlatDescent.lean

Statistics

Metric	Count
Definitions	0
Theorems surjective_descendsAlong_surjective_inf_flat_inf_quasicompact, descendsAlong_isOpenImmersion_surjective_inf_flat_inf_quasicompact', descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact, descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact, descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact, descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact, instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget, instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfLocallyOfFinitePresentation, instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfQuasiCompact	9
Total	9

AlgebraicGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
descendsAlong_isOpenImmersion_surjective_inf_flat_inf_quasicompact' 📖	mathematical	—	CategoryTheory.MorphismProperty.DescendsAlong Scheme Scheme.instCategory IsOpenImmersion CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra Surjective Flat QuasiCompact	—	CategoryTheory.MorphismProperty.DescendsAlong.mk' isOpenImmersion_respectsIso CategoryTheory.MorphismProperty.of_pullback_fst_of_descendsAlong descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact UniversallyOpen.instOfIsOpenImmersion IsOpenMap.isOpen_range Scheme.Hom.isOpenMap Scheme.Pullback.instHasPullback Scheme.Opens.instIsOpenImmersionι Scheme.Opens.range_ι Set.instReflSubset Scheme.Hom.injective instUniversallyInjectiveOfMonoScheme IsOpenImmersion.mono IsOpenImmersion.lift_fac isIso_iff_isOpenImmersion_and_surjective CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_fst IsOpenImmersion.comp IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_hom IsOpenImmersion.of_comp IsOpenImmersion.instFstScheme Surjective.instFstScheme descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact CategoryTheory.MorphismProperty.pullback_snd CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf Surjective.instIsStableUnderBaseChangeScheme Flat.isStableUnderBaseChange quasiCompact_isStableUnderBaseChange
descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact 📖	mathematical	—	CategoryTheory.MorphismProperty.DescendsAlong Scheme Scheme.instCategory CategoryTheory.MorphismProperty.isomorphisms CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra Surjective Flat QuasiCompact	—	IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf Surjective.instIsStableUnderBaseChangeScheme Flat.isStableUnderBaseChange CategoryTheory.MorphismProperty.IsStableUnderComposition.inf CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition instIsMultiplicativeSchemeSurjective Flat.instIsStableUnderCompositionScheme CategoryTheory.MorphismProperty.IsStableUnderBaseChange.isomorphisms inf_comm inf_le_inf le_rfl IsLocalIso.le_of_isZariskiLocalAtSource CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities Flat.instIsMultiplicativeScheme HasRingHomProperty.instIsZariskiLocalAtSource Flat.instHasRingHomPropertyFlat Scheme.instIsLocalAtTargetIsomorphismsZariskiPrecoverage Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.of_pullback_fst_of_descendsAlong descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact instQuasiCompactOfIsAffineHom isAffineHom_of_isAffine isAffine_Spec instUniversallyInjectiveOfMonoScheme IsOpenImmersion.mono IsOpenImmersion.of_isIso Flat.surjective_descendsAlong_surjective_inf_flat_inf_quasicompact instSurjectiveOfIsIsoScheme descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact UniversallyOpen.instOfIsOpenImmersion Scheme.Hom.continuous Scheme.Hom.isOpenMap Scheme.Hom.injective Scheme.Hom.surjective isAffineHom_of_isInducing IsHomeomorph.isInducing Topology.IsClosedEmbedding.isClosed_range IsHomeomorph.isClosedEmbedding isAffine_of_isAffineHom Spec.map_surjective of_pullback_fst_Spec_of_codescendsAlong CategoryTheory.MorphismProperty.RespectsIso.isomorphisms RingHom.FaithfullyFlat.codescendsAlong_bijective flat_and_surjective_SpecMap_iff CategoryTheory.MorphismProperty.cancel_left_of_respectsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Limits.pullback.lift_fst CategoryTheory.Limits.pullback.map_isIso CategoryTheory.IsIso.id
descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact 📖	mathematical	—	CategoryTheory.MorphismProperty.DescendsAlong Scheme Scheme.instCategory UniversallyClosed CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra Surjective Flat QuasiCompact	—	IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf Surjective.instIsStableUnderBaseChangeScheme Flat.isStableUnderBaseChange CategoryTheory.MorphismProperty.IsStableUnderComposition.inf CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition instIsMultiplicativeSchemeSurjective Flat.instIsStableUnderCompositionScheme universallyClosed_isStableUnderBaseChange inf_comm inf_le_inf le_rfl IsLocalIso.le_of_isZariskiLocalAtSource CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities Flat.instIsMultiplicativeScheme HasRingHomProperty.instIsZariskiLocalAtSource Flat.instHasRingHomPropertyFlat universallyClosed_isZariskiLocalAtTarget Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.universally_mk' instRespectsIsoSchemeTopologicallyIsClosedMap CategoryTheory.Limits.pullback.condition CategoryTheory.Limits.hasLimitOfHasLimitsOfShape Scheme.Pullback.instHasPullbacks CategoryTheory.IsPullback.instHasPullbackFst Scheme.image_preimage_eq_of_isPullback CategoryTheory.Limits.isPullback_map_snd_snd Scheme.Hom.isClosedMap universallyClosed_fst IsClosed.preimage Scheme.Hom.continuous Topology.IsQuotientMap.isClosed_preimage Flat.isQuotientMap_of_surjective Flat.instSndScheme instQuasiCompactSndScheme instQuasiCompactOfIsAffineHom isAffineHom_of_isAffine isAffine_Spec Surjective.instSndScheme
descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact 📖	mathematical	—	CategoryTheory.MorphismProperty.DescendsAlong Scheme Scheme.instCategory UniversallyInjective CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra Surjective Flat QuasiCompact	—	Scheme.Pullback.instHasPullbacks universallyInjective_eq_diagonal CategoryTheory.MorphismProperty.instDescendsAlongDiagonalOfRespectsIsoOfIsStableUnderBaseChange Flat.surjective_descendsAlong_surjective_inf_flat_inf_quasicompact instRespectsIsoSchemeSurjective CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf Surjective.instIsStableUnderBaseChangeScheme Flat.isStableUnderBaseChange quasiCompact_isStableUnderBaseChange
descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact 📖	mathematical	—	CategoryTheory.MorphismProperty.DescendsAlong Scheme Scheme.instCategory UniversallyOpen CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra Surjective Flat QuasiCompact	—	IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf Surjective.instIsStableUnderBaseChangeScheme Flat.isStableUnderBaseChange CategoryTheory.MorphismProperty.IsStableUnderComposition.inf CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition instIsMultiplicativeSchemeSurjective Flat.instIsStableUnderCompositionScheme UniversallyOpen.instIsStableUnderBaseChangeScheme inf_comm inf_le_inf le_rfl IsLocalIso.le_of_isZariskiLocalAtSource CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities Flat.instIsMultiplicativeScheme HasRingHomProperty.instIsZariskiLocalAtSource Flat.instHasRingHomPropertyFlat UniversallyOpen.instIsZariskiLocalAtTarget Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.universally_mk' instRespectsIsoSchemeTopologicallyIsOpenMap CategoryTheory.Limits.pullback.condition CategoryTheory.Limits.hasLimitOfHasLimitsOfShape Scheme.Pullback.instHasPullbacks CategoryTheory.IsPullback.instHasPullbackFst Scheme.image_preimage_eq_of_isPullback CategoryTheory.Limits.isPullback_map_snd_snd Scheme.Hom.isOpenMap UniversallyOpen.fst IsOpen.preimage Scheme.Hom.continuous Topology.IsQuotientMap.isOpen_preimage Flat.isQuotientMap_of_surjective Flat.instSndScheme instQuasiCompactSndScheme instQuasiCompactOfIsAffineHom isAffineHom_of_isAffine isAffine_Spec Surjective.instSndScheme
instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget 📖	mathematical	—	CategoryTheory.MorphismProperty.DescendsAlong Scheme Scheme.instCategory CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra Surjective Flat LocallyOfFinitePresentation	—	IsZariskiLocalAtTarget.descendsAlong CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf Surjective.instIsStableUnderBaseChangeScheme Flat.isStableUnderBaseChange locallyOfFinitePresentation_isStableUnderBaseChange Scheme.Pullback.instHasPullback IsOpenMap.exists_opens_image_eq_of_prespectralSpace instPrespectralSpaceCarrierCarrierCommRingCat Scheme.Hom.continuous Scheme.Hom.isOpenMap UniversallyOpen.of_flat range_eq_univ Set.instReflSubset isOpen_univ isCompact_univ Scheme.compactSpace_of_isAffine isAffine_Spec CategoryTheory.MorphismProperty.of_isPullback_of_descendsAlong CategoryTheory.IsPullback.paste_vert CategoryTheory.IsPullback.of_hasPullback Eq.ge Set.mem_univ Flat.comp Flat.instOfIsOpenImmersion Scheme.Opens.instIsOpenImmersionι quasiCompact_iff_compactSpace quasiSeparatedSpace_of_isAffine isCompact_iff_compactSpace IsZariskiLocalAtTarget.of_isPullback CategoryTheory.IsPullback.flip
instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfLocallyOfFinitePresentation 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Over Scheme Scheme.instCategory CategoryTheory.instCategoryOver CategoryTheory.Over.pullback Scheme.Pullback.instHasPullback	—	CategoryTheory.MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact Scheme.instIsLocalAtTargetIsomorphismsZariskiPrecoverage CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf Surjective.instIsStableUnderBaseChangeScheme Flat.isStableUnderBaseChange locallyOfFinitePresentation_isStableUnderBaseChange Scheme.Pullback.instHasPullbacks CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits instHasFiniteLimitsScheme
instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfQuasiCompact 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Over Scheme Scheme.instCategory CategoryTheory.instCategoryOver CategoryTheory.Over.pullback Scheme.Pullback.instHasPullback	—	CategoryTheory.MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf Surjective.instIsStableUnderBaseChangeScheme Flat.isStableUnderBaseChange quasiCompact_isStableUnderBaseChange Scheme.Pullback.instHasPullbacks CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits instHasFiniteLimitsScheme

AlgebraicGeometry.Flat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
surjective_descendsAlong_surjective_inf_flat_inf_quasicompact 📖	mathematical	—	CategoryTheory.MorphismProperty.DescendsAlong AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Surjective CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra AlgebraicGeometry.Flat AlgebraicGeometry.QuasiCompact	—	CategoryTheory.MorphismProperty.DescendsAlong.of_le CategoryTheory.MorphismProperty.instDescendsAlongOfIsStableUnderBaseChangeOfHasOfPrecompPropertyOfRespectsRight AlgebraicGeometry.Surjective.instIsStableUnderBaseChangeScheme AlgebraicGeometry.instHasOfPrecompPropertySchemeSurjective CategoryTheory.MorphismProperty.Respects.toRespectsRight CategoryTheory.MorphismProperty.instRespectsOfIsStableUnderComposition CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition AlgebraicGeometry.instIsMultiplicativeSchemeSurjective le_of_inf_eq'

---

← Back to Index