Flat

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

Statistics

Metric	Count
Definitions Flat, pushoutSection	2
Theorems comp, epi_of_flat_of_surjective, flat_and_surjective_iff_faithfullyFlat_of_isAffine, flat_appLE, flat_of_affine_subset, iff_flat_stalkMap, instDescScheme, instFstScheme, instHasRingHomPropertyFlat, instIsMultiplicativeScheme, instIsStableUnderCompositionScheme, instMorphismRestrict, instOfIsOpenImmersion, instOfSubsingletonCarrierCarrierCommRingCatOfIsIntegral, instResLE, instSndScheme, isQuotientMap_of_surjective, isStableUnderBaseChange, of_stalkMap, stalkMap, flat_appLE, flat_and_surjective_SpecMap_iff, flat_iff, isIso_pushoutSection_iff, isIso_pushoutSection_of_iSup_eq, isIso_pushoutSection_of_isAffineOpen, isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, isIso_pushoutSection_of_isQuasiSeparated_of_flat_left, isIso_pushoutSection_of_isQuasiSeparated_of_flat_right, mono_pushoutSection_of_iSup_eq, mono_pushoutSection_of_isCompact_of_flat_left, mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat, mono_pushoutSection_of_isCompact_of_flat_right, mono_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat	34
Total	36

AlgebraicGeometry

Definitions

Name	Category	Theorems
Flat 📖	CompData	24 math math: descendsAlong_isOpenImmersion_surjective_inf_flat_inf_quasicompact', descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact, instFlatOfSmooth, descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact, Flat.instMorphismRestrict, Flat.of_stalkMap, Flat.instFstScheme, instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget, Flat.instIsMultiplicativeScheme, Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, Flat.instHasRingHomPropertyFlat, Flat.instResLE, Flat.comp, Flat.instOfIsOpenImmersion, Flat.surjective_descendsAlong_surjective_inf_flat_inf_quasicompact, Flat.instOfSubsingletonCarrierCarrierCommRingCatOfIsIntegral, Flat.iff_flat_stalkMap, Flat.instIsStableUnderCompositionScheme, flat_and_surjective_SpecMap_iff, Flat.isStableUnderBaseChange, Flat.instSndScheme, flat_iff, descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact, descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact
pushoutSection 📖	CompOp	9 math math: isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat, mono_pushoutSection_of_isCompact_of_flat_right, mono_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, isIso_pushoutSection_of_isQuasiSeparated_of_flat_left, isIso_pushoutSection_iff, mono_pushoutSection_of_isCompact_of_flat_left, isIso_pushoutSection_of_isQuasiSeparated_of_flat_right, isIso_pushoutSection_of_isAffineOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flat_and_surjective_SpecMap_iff 📖	mathematical	—	Flat Spec Spec.map Surjective RingHom.FaithfullyFlat CommRingCat.carrier CommRingCat.commRing CommRingCat.Hom.hom	—	HasRingHomProperty.Spec_iff Flat.instHasRingHomPropertyFlat RingHom.FaithfullyFlat.iff_flat_and_comap_surjective surjective_iff
flat_iff 📖	mathematical	—	Flat RingHom.Flat CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op Scheme.Opens CommRingCat.commRing CommRingCat.Hom.hom Scheme.Hom.appLE	—	—
isIso_pushoutSection_iff 📖	mathematical	CategoryTheory.IsPullback Scheme Scheme.instCategory Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice	CategoryTheory.IsIso CategoryTheory.Limits.pushout Opposite CategoryTheory.Category.opposite PresheafedSpace.presheaf Opposite.op Scheme.Hom.appLE CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.span pushoutSection CategoryTheory.IsPushout	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.IsPushout.of_iso CategoryTheory.IsPushout.of_hasPushout CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Iso.isIso_inv
isIso_pushoutSection_of_iSup_eq 📖	—	CategoryTheory.IsPullback Scheme Scheme.instCategory Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CategoryTheory.IsIso CategoryTheory.Limits.pushout Opposite CategoryTheory.Category.opposite PresheafedSpace.presheaf Opposite.op Scheme.Hom.appLE CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.span pushoutSection CategoryTheory.Mono	—	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat LE.le.trans inf_le_left le_antisymm iSup_le_iff le_iSup CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.CompleteLattice.hasColimits_of_completeLattice CategoryTheory.Limits.CompleteLattice.colimit_eq_iSup inf_le_inf Scheme.Hom.preimage_mono le_refl le_imp_le_of_le_of_le Scheme.Hom.appLE_map CategoryTheory.Category.assoc CategoryTheory.Limits.pushout.hom_ext CommRingCat.hom_ext RingHom.ext CategoryTheory.Limits.colimit.ι_desc_assoc CategoryTheory.Category.id_comp CategoryTheory.Limits.colimit.ι_desc Scheme.Hom.map_appLE CommRingCat.Under.preservesFiniteLimits_of_flat nonempty_fintype CategoryTheory.Limits.PreservesLimit.preserves TopCat.Presheaf.isSheaf_iff_isSheafPreservesLimitPairwiseIntersections SheafedSpace.IsSheaf CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.comp_preservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.preservesLimitsOfShapeOfPreservesFiniteLimits CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit CommRingCat.hasLimit small_subtype small_Pi Opposite.small UnivLE.small UnivLE.self CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits CategoryTheory.Limits.CompleteLattice.hasFiniteColimits_of_semilatticeSup_orderBot iSup_inf_eq Scheme.Hom.preimage_iSup Scheme.Hom.preimage_inf inf_inf_distrib_right CategoryTheory.eqToHom_op CategoryTheory.Functor.map_comp CategoryTheory.mono_comp CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.IsIso.comp_isIso Equiv.surjective CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.cancel_mono CategoryTheory.NatTrans.naturality CategoryTheory.IsIso.inv_hom_id_assoc CategoryTheory.Limits.Cone.w CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.Limits.IsLimit.fac CategoryTheory.Limits.IsLimit.fac_assoc CategoryTheory.IsIso.hom_inv_id CategoryTheory.IsIso.hom_inv_id_assoc CategoryTheory.IsIso.inv_hom_id CategoryTheory.Limits.pushout.desc.congr_simp CategoryTheory.Under.homMk.congr_simp
isIso_pushoutSection_of_isAffineOpen 📖	mathematical	CategoryTheory.IsPullback Scheme Scheme.instCategory Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice	CategoryTheory.IsIso CategoryTheory.Limits.pushout Opposite CategoryTheory.Category.opposite PresheafedSpace.presheaf Opposite.op Scheme.Hom.appLE CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.span pushoutSection	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat isIso_pushoutSection_iff CategoryTheory.IsPullback.unop CategoryTheory.IsPullback.of_map_of_faithful CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape CategoryTheory.Limits.ReflectsFiniteLimits.reflects CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms CategoryTheory.reflectsIsomorphisms_of_full_and_faithful Spec.full Spec.faithful CategoryTheory.Limits.hasFiniteLimits_opposite CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint IsAffine.of_isIso Scheme.Pullback.instHasPullback Scheme.Hom.isPullback_resLE CategoryTheory.Iso.isIso_hom instIsAffinePullbackSchemeOfIsAffineHom_1 isAffineHom_of_isAffine CategoryTheory.IsPullback.of_iso CategoryTheory.IsPullback.flip LE.le.trans le_rfl Spec.map_comp Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc Scheme.Opens.toSpecΓ_naturality Scheme.Hom.map_resLE_assoc
isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat 📖	mathematical	CategoryTheory.IsPullback Scheme Scheme.instCategory Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice IsCompact SetLike.coe TopologicalSpace.Opens.instSetLike IsQuasiSeparated	CategoryTheory.IsIso CategoryTheory.Limits.pushout Opposite CategoryTheory.Category.opposite PresheafedSpace.presheaf Opposite.op Scheme.Hom.appLE CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.span pushoutSection	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.IsPullback.flip inf_comm isCompact_iff_finite_and_eq_biUnion_affineOpens isOpen_iUnion TopologicalSpace.Opens.is_open' Set.iUnion_congr_Prop Set.iUnion_coe_set Set.Finite.to_subtype isIso_pushoutSection_of_iSup_eq iSup_subtype isIso_pushoutSection_of_isQuasiSeparated_of_flat_left mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat LE.le.trans inf_le_left IsAffineOpen.isCompact CategoryTheory.Limits.hasPushout_symmetry CategoryTheory.isIso_comp_left_iff CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.pushout.hom_ext CommRingCat.hom_ext RingHom.ext CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom_assoc CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom_assoc
isIso_pushoutSection_of_isQuasiSeparated_of_flat_left 📖	mathematical	CategoryTheory.IsPullback Scheme Scheme.instCategory Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice IsCompact SetLike.coe TopologicalSpace.Opens.instSetLike IsQuasiSeparated	CategoryTheory.IsIso CategoryTheory.Limits.pushout Opposite CategoryTheory.Category.opposite PresheafedSpace.presheaf Opposite.op Scheme.Hom.appLE CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.span pushoutSection	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.IsPullback.flip inf_comm isIso_pushoutSection_of_isQuasiSeparated_of_flat_right CategoryTheory.Limits.hasPushout_symmetry CategoryTheory.isIso_comp_left_iff CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.pushout.hom_ext CommRingCat.hom_ext RingHom.ext CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom_assoc CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom_assoc
isIso_pushoutSection_of_isQuasiSeparated_of_flat_right 📖	mathematical	CategoryTheory.IsPullback Scheme Scheme.instCategory Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice IsCompact SetLike.coe TopologicalSpace.Opens.instSetLike IsQuasiSeparated	CategoryTheory.IsIso CategoryTheory.Limits.pushout Opposite CategoryTheory.Category.opposite PresheafedSpace.presheaf Opposite.op Scheme.Hom.appLE CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.span pushoutSection	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat isCompact_iff_finite_and_eq_biUnion_affineOpens isOpen_iUnion TopologicalSpace.Opens.is_open' Set.iUnion_congr_Prop Set.iUnion_coe_set Set.Finite.to_subtype isIso_pushoutSection_of_iSup_eq iSup_subtype isIso_pushoutSection_of_isAffineOpen mono_pushoutSection_of_isCompact_of_flat_right LE.le.trans inf_le_left IsAffineOpen.isCompact Scheme.Hom.flat_appLE
mono_pushoutSection_of_iSup_eq 📖	—	CategoryTheory.IsPullback Scheme Scheme.instCategory Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CategoryTheory.Mono CategoryTheory.Limits.pushout Opposite CategoryTheory.Category.opposite PresheafedSpace.presheaf Opposite.op Scheme.Hom.appLE CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.span pushoutSection	—	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat inf_le_inf Scheme.Hom.preimage_mono le_iSup le_refl LE.le.trans Scheme.Hom.appLE_map TopCat.Presheaf.IsSheaf.section_ext CommRingCat.hasLimits CommRingCat.forget_preservesLimits CommRingCat.forgetReflectIsos SheafedSpace.IsSheaf IsScalarTower.to_smulCommClass IsScalarTower.right Module.Flat.lTensor_preserves_injective_linearMap CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits nonempty_fintype Algebra.to_smulCommClass CategoryTheory.IsPushout.flip CommRingCat.isPushout_tensorProduct IsScalarTower.left AlgHomClass.toRingHomClass AlgHom.algHomClass Function.Injective.piMap RingEquiv.injective AlgEquiv.injective Algebra.TensorProduct.ringHom_ext CategoryTheory.IsPushout.inr_isoPushout_hom RingHom.ext CategoryTheory.Limits.colimit.ι_desc map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass CategoryTheory.IsPushout.inl_isoPushout_hom CategoryTheory.Category.assoc Scheme.Hom.map_appLE Function.Injective.of_comp CategoryTheory.Iso.hom_inv_id_apply
mono_pushoutSection_of_isCompact_of_flat_left 📖	mathematical	CategoryTheory.IsPullback Scheme Scheme.instCategory Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice IsCompact SetLike.coe TopologicalSpace.Opens.instSetLike	CategoryTheory.Mono CategoryTheory.Limits.pushout Opposite CategoryTheory.Category.opposite PresheafedSpace.presheaf Opposite.op Scheme.Hom.appLE CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.span pushoutSection	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.IsPullback.flip inf_comm mono_pushoutSection_of_isCompact_of_flat_right CategoryTheory.Limits.hasPushout_symmetry CategoryTheory.mono_comp_iff_of_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.pushout.hom_ext CommRingCat.hom_ext RingHom.ext CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom_assoc CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom_assoc
mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat 📖	mathematical	CategoryTheory.IsPullback Scheme Scheme.instCategory Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice IsCompact SetLike.coe TopologicalSpace.Opens.instSetLike	CategoryTheory.Mono CategoryTheory.Limits.pushout Opposite CategoryTheory.Category.opposite PresheafedSpace.presheaf Opposite.op Scheme.Hom.appLE CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.span pushoutSection	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat isCompact_iff_finite_and_eq_biUnion_affineOpens Set.Finite.to_subtype mono_pushoutSection_of_iSup_eq iSup_subtype mono_pushoutSection_of_isCompact_of_flat_left
mono_pushoutSection_of_isCompact_of_flat_right 📖	mathematical	CategoryTheory.IsPullback Scheme Scheme.instCategory Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice IsCompact SetLike.coe TopologicalSpace.Opens.instSetLike	CategoryTheory.Mono CategoryTheory.Limits.pushout Opposite CategoryTheory.Category.opposite PresheafedSpace.presheaf Opposite.op Scheme.Hom.appLE CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.span pushoutSection	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat isCompact_iff_finite_and_eq_biUnion_affineOpens Set.Finite.to_subtype mono_pushoutSection_of_iSup_eq iSup_subtype isIso_pushoutSection_of_isAffineOpen CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso Scheme.Hom.flat_appLE
mono_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat 📖	mathematical	CategoryTheory.IsPullback Scheme Scheme.instCategory Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice IsCompact SetLike.coe TopologicalSpace.Opens.instSetLike	CategoryTheory.Mono CategoryTheory.Limits.pushout Opposite CategoryTheory.Category.opposite PresheafedSpace.presheaf Opposite.op Scheme.Hom.appLE CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.span pushoutSection	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.IsPullback.flip inf_comm mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat CategoryTheory.Limits.hasPushout_symmetry CategoryTheory.mono_comp_iff_of_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.pushout.hom_ext CommRingCat.hom_ext RingHom.ext CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom_assoc CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom_assoc

AlgebraicGeometry.Flat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	AlgebraicGeometry.Flat CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	CategoryTheory.MorphismProperty.comp_mem instIsStableUnderCompositionScheme
epi_of_flat_of_surjective 📖	mathematical	—	CategoryTheory.Epi AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory	—	CategoryTheory.Functor.epi_of_epi_map CategoryTheory.reflectsEpimorphisms_of_reflectsColimitsOfShape CategoryTheory.Limits.ReflectsFiniteColimits.reflects CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimits CategoryTheory.Limits.fullyFaithful_reflectsColimits AlgebraicGeometry.Scheme.instFullLocallyRingedSpaceForgetToLocallyRingedSpace AlgebraicGeometry.Scheme.instFaithfulLocallyRingedSpaceForgetToLocallyRingedSpace CategoryTheory.Limits.reflectsFiniteColimitsOfReflectsIsomorphisms AlgebraicGeometry.LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace CategoryTheory.Limits.hasFiniteColimits_of_hasColimits AlgebraicGeometry.LocallyRingedSpace.instHasColimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits AlgebraicGeometry.LocallyRingedSpace.preservesColimits_forgetToSheafedSpace AlgebraicGeometry.SheafedSpace.epi_of_base_surjective_of_stalk_mono CommRingCat.Colimits.hasColimits_commRingCat CommRingCat.hasLimits CommRingCat.forget_preservesLimits CommRingCat.FilteredColimits.forget_preservesFilteredColimits CommRingCat.forgetReflectIsos AlgebraicGeometry.Surjective.surj CategoryTheory.ConcreteCategory.mono_of_injective Module.FaithfullyFlat.of_flat_of_isLocalHom AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf stalkMap AlgebraicGeometry.LocallyRingedSpace.Hom.prop RingHom.FaithfullyFlat.injective
flat_and_surjective_iff_faithfullyFlat_of_isAffine 📖	mathematical	—	AlgebraicGeometry.Flat AlgebraicGeometry.Surjective RingHom.FaithfullyFlat CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommRingCat.commRing CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.appTop	—	RingHom.FaithfullyFlat.iff_flat_and_comap_surjective CategoryTheory.MorphismProperty.arrow_mk_iso_iff AlgebraicGeometry.instRespectsIsoSchemeSurjective CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource instHasRingHomPropertyFlat AlgebraicGeometry.HasRingHomProperty.Spec_iff AlgebraicGeometry.surjective_iff
flat_appLE 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	RingHom.Flat CommRingCat.carrier Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommRingCat.commRing CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.appLE	—	—
flat_of_affine_subset 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	RingHom.Flat CommRingCat.carrier Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommRingCat.commRing CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.appLE	—	AlgebraicGeometry.Scheme.Hom.flat_appLE
iff_flat_stalkMap 📖	mathematical	—	AlgebraicGeometry.Flat RingHom.Flat CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CommRingCat.commRing CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.stalkMap	—	CommRingCat.Colimits.hasColimits_commRingCat stalkMap of_stalkMap
instDescScheme 📖	mathematical	AlgebraicGeometry.Flat	CategoryTheory.Limits.sigmaObj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete CategoryTheory.Limits.Sigma.desc	—	AlgebraicGeometry.IsZariskiLocalAtSource.sigmaDesc AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource instHasRingHomPropertyFlat
instFstScheme 📖	mathematical	—	AlgebraicGeometry.Flat CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.fst	—	CategoryTheory.MorphismProperty.pullback_fst AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange isStableUnderBaseChange
instHasRingHomPropertyFlat 📖	mathematical	—	AlgebraicGeometry.HasRingHomProperty AlgebraicGeometry.Flat RingHom.Flat	—	RingHom.Flat.propertyIsLocal CategoryTheory.MorphismProperty.ext AlgebraicGeometry.flat_iff AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen
instIsMultiplicativeScheme 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Flat	—	instOfIsOpenImmersion AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.IsIso.id instIsStableUnderCompositionScheme
instIsStableUnderCompositionScheme 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderComposition AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Flat	—	AlgebraicGeometry.HasRingHomProperty.stableUnderComposition instHasRingHomPropertyFlat RingHom.Flat.stableUnderComposition
instMorphismRestrict 📖	mathematical	—	AlgebraicGeometry.Flat AlgebraicGeometry.Scheme.Opens.toScheme CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' AlgebraicGeometry.morphismRestrict	—	AlgebraicGeometry.IsZariskiLocalAtTarget.restrict AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtTarget instHasRingHomPropertyFlat
instOfIsOpenImmersion 📖	mathematical	—	AlgebraicGeometry.Flat	—	AlgebraicGeometry.HasRingHomProperty.of_isOpenImmersion instHasRingHomPropertyFlat RingHom.Flat.containsIdentities
instOfSubsingletonCarrierCarrierCommRingCatOfIsIntegral 📖	mathematical	—	AlgebraicGeometry.Flat	—	AlgebraicGeometry.instIsAffineOfFiniteOfDiscreteTopologyCarrierCarrierCommRingCat Finite.of_subsingleton Subsingleton.discreteTopology CategoryTheory.MorphismProperty.cancel_right_of_respectsIso CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource instHasRingHomPropertyFlat CategoryTheory.Iso.isIso_hom AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover AlgebraicGeometry.Scheme.local_affine AlgebraicGeometry.Spec.map_preimage AlgebraicGeometry.HasRingHomProperty.Spec_iff RingHom.Flat.of_isField AlgebraicGeometry.isField_of_isIntegral_of_subsingleton
instResLE 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	AlgebraicGeometry.Flat AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Hom.resLE	—	comp instOfIsOpenImmersion AlgebraicGeometry.instIsOpenImmersionHomOfLE instMorphismRestrict
instSndScheme 📖	mathematical	—	AlgebraicGeometry.Flat CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.snd	—	CategoryTheory.MorphismProperty.pullback_snd AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange isStableUnderBaseChange
isQuotientMap_of_surjective 📖	mathematical	—	Topology.IsQuotientMap TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	—	Topology.isQuotientMap_iff AlgebraicGeometry.Scheme.Hom.surjective IsOpen.preimage AlgebraicGeometry.Scheme.Hom.continuous AlgebraicGeometry.Spec.map_surjective Topology.IsQuotientMap.isOpen_preimage PrimeSpectrum.isQuotientMap_of_generalizingMap AlgebraicGeometry.surjective_iff RingHom.Flat.generalizingMap_comap AlgebraicGeometry.HasRingHomProperty.Spec_iff instHasRingHomPropertyFlat AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace AlgebraicGeometry.Scheme.compactSpace_of_isAffine AlgebraicGeometry.isAffine_Spec AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self AlgebraicGeometry.instIsAffineSigmaObjScheme Finite.of_fintype AlgebraicGeometry.instIsAffineXSchemeFiniteSubcover AlgebraicGeometry.Scheme.isAffine_affineCover comp instOfIsOpenImmersion CategoryTheory.Iso.isIso_inv instDescScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.instQuasiCompactOfIsAffineHom AlgebraicGeometry.instIsAffineHomOfIsIsoScheme AlgebraicGeometry.isAffineHom_of_isAffine AlgebraicGeometry.instSurjectiveCompScheme AlgebraicGeometry.instSurjectiveOfIsIsoScheme AlgebraicGeometry.instSurjectiveDescI₀SchemeF CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.Hom.comp_base TopCat.coe_comp Set.preimage_comp TopologicalSpace.IsOpenCover.isOpen_iff_inter AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange AlgebraicGeometry.Scheme.Hom.coe_opensRange Set.image_preimage_eq_inter_range Topology.IsOpenEmbedding.isOpenMap AlgebraicGeometry.Scheme.Hom.isOpenEmbedding AlgebraicGeometry.Scheme.Pullback.instHasPullback instFstScheme AlgebraicGeometry.instQuasiCompactFstScheme AlgebraicGeometry.Surjective.instFstScheme CategoryTheory.Limits.pullback.condition AlgebraicGeometry.Scheme.local_affine
isStableUnderBaseChange 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Flat	—	AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange instHasRingHomPropertyFlat RingHom.Flat.isStableUnderBaseChange
of_stalkMap 📖	mathematical	RingHom.Flat CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CommRingCat.commRing CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.stalkMap	AlgebraicGeometry.Flat	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.HasRingHomProperty.of_stalkMap instHasRingHomPropertyFlat RingHom.Flat.ofLocalizationPrime
stalkMap 📖	mathematical	—	RingHom.Flat CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CommRingCat.commRing CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.stalkMap	—	AlgebraicGeometry.HasRingHomProperty.stalkMap instHasRingHomPropertyFlat RingHom.Flat.localRingHom RingHom.instRingHomClass Ideal.IsPrime.comap

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flat_appLE 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	RingHom.Flat CommRingCat.carrier Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommRingCat.commRing CommRingCat.Hom.hom appLE	—	AlgebraicGeometry.Flat.flat_appLE

---

← Back to Index