RingHomProperties

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

Statistics

Metric	Count
Definitions `HasRingHomProperty`, `affineLocally`, `sourceAffineLocally`	3
Theorems `HasAffineProperty`, `Spec_iff`, `appLE`, `appTop`, `comp_of_isOpenImmersion`, `containsIdentities`, `copy`, `eq_affineLocally`, `eq_affineLocally'`, `ext`, `iff_appLE`, `iff_exists_appLE`, `iff_exists_appLE_locally`, `iff_of_iSup_eq_top`, `iff_of_isAffine`, `iff_of_source_openCover`, `inf`, `instIsZariskiLocalAtSource`, `instIsZariskiLocalAtTarget`, `isLocal_ringHomProperty`, `isLocal_ringHomProperty_of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget`, `isMultiplicative`, `isStableUnderBaseChange`, `locally_of_iff`, `of_comp`, `of_iSup_eq_top`, `of_isLocalAtSource_of_isLocalAtTarget`, `of_isOpenImmersion`, `of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget`, `of_source_openCover`, `of_stalkMap`, `respects_isOpenImmersion`, `stableUnderComposition`, `stalkMap`, `stalkMap_of_respectsIso`, `stalkwise`, `affineLocally_iff_affineOpens_le`, `affineLocally_iff_forall_isAffineOpen`, `affineLocally_le`, `affineLocally_respectsIso`, `exists_affineOpens_le_appLE_of_appLE`, `exists_basicOpen_le_appLE_of_appLE_of_isAffine`, `sourceAffineLocally_isLocal`, `sourceAffineLocally_morphismRestrict`, `sourceAffineLocally_respectsIso`, `pullback_fst_appTop`	46
Total	49

AlgebraicGeometry

Definitions

Name	Category	Theorems
`HasRingHomProperty` 📖	CompData	15 math math: `SurjectiveOnStalks.instHasRingHomPropertySurjectiveOnStalks`, `Flat.instHasRingHomPropertyFlat`, `instHasRingHomPropertySmoothOfRelativeDimensionLocallyIsStandardSmoothOfRelativeDimension`, `HasRingHomProperty.stalkwise`, `instHasRingHomPropertyLocallyOfFiniteTypeFiniteType`, `HasRingHomProperty.inf`, `instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation`, `HasRingHomProperty.copy`, `FormallyUnramified.instHasRingHomPropertyFormallyUnramified`, `HasRingHomProperty.of_isLocalAtSource_of_isLocalAtTarget`, `Etale.instHasRingHomPropertyEtale`, `HasRingHomProperty.locally_of_iff`, `instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite`, `instHasRingHomPropertySmoothSmooth`, `HasRingHomProperty.of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget`
`affineLocally` 📖	CompOp	8 math math: `affineLocally_iff_forall_isAffineOpen`, `HasRingHomProperty.eq_affineLocally'`, `affineLocally_iff_affineOpens_le`, `affineLocally_respectsIso`, `HasRingHomProperty.eq_affineLocally`, `targetAffineLocally_affineAnd_eq_affineLocally`, `targetAffineLocally_affineAnd_iff_affineLocally`, `affineLocally_le`
`sourceAffineLocally` 📖	CompOp	4 math math: `HasRingHomProperty.HasAffineProperty`, `sourceAffineLocally_isLocal`, `sourceAffineLocally_respectsIso`, `sourceAffineLocally_morphismRestrict`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineLocally_iff_affineOpens_le` 📖	mathematical	—	`affineLocally` `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` `Set` `Set.instMembership` `Scheme.affineOpens` `CommRingCat.commRing` `CommRingCat.Hom.hom` `Scheme.Hom.appLE`	—	`instIsAffineToSchemeValOpensMemSetAffineOpens` `sourceAffineLocally_morphismRestrict`
`affineLocally_iff_forall_isAffineOpen` 📖	mathematical	—	`affineLocally` `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`	—	—
`affineLocally_le` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `affineLocally`	—	—
`affineLocally_respectsIso` 📖	mathematical	`RingHom.RespectsIso`	`CategoryTheory.MorphismProperty.RespectsIso` `Scheme` `Scheme.instCategory` `affineLocally`	—	`instRespectsIsoSchemeTargetAffineLocallyOfToProperty` `sourceAffineLocally_respectsIso`
`exists_affineOpens_le_appLE_of_appLE` 📖	—	`RingHom.StableUnderCompositionWithLocalizationAwayTarget` `RingHom.LocalizationAwayPreserves` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Scheme.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set` `Set.instMembership` `Scheme.affineOpens` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `CommRingCat.carrier` `Opposite` `CategoryTheory.Category.opposite` `PresheafedSpace.presheaf` `Opposite.op` `CommRingCat.commRing` `CommRingCat.Hom.hom` `Scheme.Hom.appLE` `TopologicalSpace.Opens.carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier`	—	—	`IsAffineOpen.exists_basicOpen_le` `IsAffineOpen.basicOpen` `exists_basicOpen_le_appLE_of_appLE_of_isAffine` `le_trans` `Scheme.basicOpen_le`
`exists_basicOpen_le_appLE_of_appLE_of_isAffine` 📖	mathematical	`RingHom.StableUnderCompositionWithLocalizationAwayTarget` `RingHom.LocalizationAwayPreserves` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Scheme.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set` `Set.instMembership` `Scheme.affineOpens` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `CommRingCat.carrier` `Opposite` `CategoryTheory.Category.opposite` `PresheafedSpace.presheaf` `Opposite.op` `CommRingCat.commRing` `CommRingCat.Hom.hom` `Scheme.Hom.appLE` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier`	`Scheme.basicOpen`	—	`exists_basicOpen_le_affine_inter` `IsAffineOpen.basicOpen` `Scheme.basicOpen_res` `le_trans` `Scheme.basicOpen_le` `Scheme.preimage_basicOpen` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `Scheme.Hom.appLE_congr` `IsAffineOpen.isLocalization_basicOpen` `IsAffineOpen.appLE_eq_away_map`
`sourceAffineLocally_isLocal` 📖	mathematical	`RingHom.RespectsIso` `RingHom.LocalizationAwayPreserves` `RingHom.OfLocalizationSpan`	`AffineTargetMorphismProperty.IsLocal` `sourceAffineLocally`	—	`sourceAffineLocally_respectsIso` `IsAffineOpen.instIsAffineToSchemeBasicOpen` `sourceAffineLocally_morphismRestrict` `CommRingCat.comp_apply` `Scheme.basicOpen_res` `Scheme.preimage_basicOpen` `Scheme.Hom.appLE_congr` `IsAffineOpen.isLocalization_basicOpen` `isAffineOpen_top` `IsAffineOpen.appLE_eq_away_map` `le_top` `IsAffineOpen.basicOpen` `RingHom.RespectsIso.isLocalization_away_iff` `CommRingCat.hom_ofHom`
`sourceAffineLocally_morphismRestrict` 📖	mathematical	—	`sourceAffineLocally` `Scheme.Opens.toScheme` `CategoryTheory.Functor.obj` `Scheme.Opens` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `TopCat.str` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `morphismRestrict` `CommRingCat.carrier` `Opposite` `CategoryTheory.Category.opposite` `PresheafedSpace.presheaf` `Opposite.op` `Set` `Set.instMembership` `Scheme.affineOpens` `CommRingCat.commRing` `CommRingCat.Hom.hom` `Scheme.Hom.appLE`	—	`Scheme.Opens.instIsOpenImmersionι` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.image_mono` `Eq.le` `image_morphismRestrict_preimage` `morphismRestrict_appLE` `Equiv.forall_congr_left` `Equiv.apply_symm_apply` `Scheme.Hom.appLE_congr` `Scheme.Opens.ι_image_top`
`sourceAffineLocally_respectsIso` 📖	mathematical	`RingHom.RespectsIso`	`CategoryTheory.MorphismProperty.RespectsIso` `Scheme` `Scheme.instCategory` `AffineTargetMorphismProperty.toProperty` `sourceAffineLocally`	—	`IsOpenImmersion.of_isIso` `CategoryTheory.Iso.isIso_hom` `Eq.ge` `Scheme.Hom.preimage_image_eq` `CategoryTheory.IsIso.comp_isIso` `Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor` `CategoryTheory.Functor.map_isIso` `CategoryTheory.isIso_op` `CategoryTheory.instIsIsoEqToHom` `le_top` `LE.le.trans` `Scheme.Hom.appLE_comp_appLE` `CommRingCat.hom_comp` `RingHom.RespectsIso.cancel_right_isIso` `IsAffineOpen.image_of_isOpenImmersion` `Subtype.prop` `Scheme.Hom.comp_appLE` `RingHom.RespectsIso.cancel_left_isIso` `Scheme.Hom.instIsIsoCommRingCatApp`

AlgebraicGeometry.HasRingHomProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`HasAffineProperty` 📖	mathematical	—	`AlgebraicGeometry.HasAffineProperty` `AlgebraicGeometry.sourceAffineLocally`	—	`AlgebraicGeometry.sourceAffineLocally_isLocal` `RingHom.PropertyIsLocal.respectsIso` `isLocal_ringHomProperty` `RingHom.PropertyIsLocal.localizationAwayPreserves` `RingHom.PropertyIsLocal.ofLocalizationSpan` `eq_affineLocally`
`Spec_iff` 📖	mathematical	—	`AlgebraicGeometry.Spec` `AlgebraicGeometry.Spec.map` `CommRingCat.carrier` `CommRingCat.commRing` `CommRingCat.Hom.hom`	—	`RingHom.PropertyIsLocal.respectsIso` `isLocal_ringHomProperty` `iff_of_isAffine` `AlgebraicGeometry.isAffine_Spec` `RingHom.RespectsIso.cancel_right_isIso` `CategoryTheory.Iso.isIso_hom` `CommRingCat.hom_comp` `AlgebraicGeometry.Scheme.ΓSpecIso_naturality` `RingHom.RespectsIso.cancel_left_isIso`
`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` `Set` `Set.instMembership` `AlgebraicGeometry.Scheme.affineOpens` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'`	`CommRingCat.carrier` `Opposite` `CategoryTheory.Category.opposite` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.appLE`	—	`AlgebraicGeometry.affineLocally_iff_affineOpens_le` `eq_affineLocally`
`appTop` 📖	mathematical	—	`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`	—	`AlgebraicGeometry.Scheme.Hom.appTop.eq_1` `le_rfl` `AlgebraicGeometry.Scheme.Hom.app_eq_appLE` `appLE` `AlgebraicGeometry.isAffineOpen_top`
`comp_of_isOpenImmersion` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	`eq_affineLocally` `AlgebraicGeometry.affineLocally_iff_affineOpens_le` `Eq.ge` `AlgebraicGeometry.Scheme.Hom.preimage_image_eq` `CategoryTheory.IsIso.comp_isIso` `AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor` `CategoryTheory.Functor.map_isIso` `CategoryTheory.isIso_op` `CategoryTheory.instIsIsoEqToHom` `Set.image_subset_iff` `LE.le.trans` `AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE` `CommRingCat.hom_comp` `RingHom.RespectsIso.cancel_right_isIso` `RingHom.PropertyIsLocal.respectsIso` `isLocal_ringHomProperty` `AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion`
`containsIdentities` 📖	mathematical	`RingHom.ContainsIdentities`	`CategoryTheory.MorphismProperty.ContainsIdentities` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	—	`AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top` `instIsZariskiLocalAtTarget` `AlgebraicGeometry.iSup_affineOpens_eq_top` `AlgebraicGeometry.morphismRestrict_id` `iff_of_isAffine` `AlgebraicGeometry.instIsAffineToSchemeValOpensMemSetAffineOpens` `AlgebraicGeometry.Scheme.Hom.id_appTop`
`copy` 📖	mathematical	—	`AlgebraicGeometry.HasRingHomProperty`	—	—
`eq_affineLocally` 📖	mathematical	—	`AlgebraicGeometry.affineLocally`	—	`eq_affineLocally'`
`eq_affineLocally'` 📖	mathematical	—	`AlgebraicGeometry.affineLocally`	—	—
`ext` 📖	—	—	—	—	`CategoryTheory.MorphismProperty.ext` `eq_affineLocally` `AlgebraicGeometry.affineLocally_iff_affineOpens_le`
`iff_appLE` 📖	mathematical	—	`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` `Set` `Set.instMembership` `AlgebraicGeometry.Scheme.affineOpens` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.appLE`	—	`eq_affineLocally` `AlgebraicGeometry.affineLocally_iff_affineOpens_le`
`iff_exists_appLE` 📖	mathematical	`RingHom.StableUnderCompositionWithLocalizationAwaySource`	`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` `Set` `Set.instMembership` `AlgebraicGeometry.Scheme.affineOpens` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.appLE`	—	`iff_exists_appLE_locally` `RingHom.PropertyIsLocal.respectsIso` `isLocal_ringHomProperty` `copy` `RingHom.locally_iff_of_localizationSpanTarget` `RingHom.PropertyIsLocal.ofLocalizationSpanTarget`
`iff_exists_appLE_locally` 📖	mathematical	`RingHom.StableUnderCompositionWithLocalizationAwaySource` `RingHom.RespectsIso`	`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` `Set` `Set.instMembership` `AlgebraicGeometry.Scheme.affineOpens` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.appLE`	—	`respects_isOpenImmersion` `RingHom.locally_StableUnderCompositionWithLocalizationAwaySource` `TopologicalSpace.Opens.isBasis_iff_nbhd` `AlgebraicGeometry.Scheme.isBasis_affineOpens` `TopologicalSpace.Opens.mem_top` `RingHom.locally_iff_isLocalization` `iff_appLE` `AlgebraicGeometry.iSup_basicOpen_of_span_eq_top` `isOpen_iUnion` `TopologicalSpace.Opens.is_open'` `Set.iUnion_congr_Prop` `iSup_congr_Prop` `AlgebraicGeometry.IsAffineOpen.basicOpen` `LE.le.trans` `AlgebraicGeometry.Scheme.basicOpen_le` `AlgebraicGeometry.Scheme.Hom.appLE_map` `AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen` `AlgebraicGeometry.IsZariskiLocalAtSource.iff_exists_resLE` `instIsZariskiLocalAtSource` `instIsZariskiLocalAtTarget` `CategoryTheory.MorphismProperty.Respects.toRespectsRight` `iff_of_isAffine` `AlgebraicGeometry.instIsAffineToSchemeValOpensMemSetAffineOpens` `CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `RingHom.toMorphismProperty_respectsIso_iff` `RingHom.PropertyIsLocal.respectsIso` `isLocal_ringHomProperty` `RingHom.locally_of`
`iff_of_iSup_eq_top` 📖	mathematical	`iSup` `AlgebraicGeometry.Scheme.Opens` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set` `Set.instMembership` `AlgebraicGeometry.Scheme.affineOpens` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.appLE` `le_top`	—	`le_top` `appLE` `AlgebraicGeometry.isAffineOpen_top` `of_iSup_eq_top`
`iff_of_isAffine` 📖	mathematical	—	`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`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities` `AlgebraicGeometry.isOpenImmersion_isMultiplicative` `AlgebraicGeometry.isOpenImmersion_respectsIso` `CategoryTheory.IsIso.id` `iff_of_source_openCover` `AlgebraicGeometry.instIsAffineXSchemeCoverOfIsIsoIsOpenImmersionId` `CategoryTheory.Category.id_comp`
`iff_of_source_openCover` 📖	mathematical	`AlgebraicGeometry.IsAffine` `CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.IsOpenImmersion`	`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` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.PreZeroHypercover.f`	—	`appTop` `comp_of_isOpenImmersion` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `of_source_openCover`
`inf` 📖	mathematical	—	`AlgebraicGeometry.HasRingHomProperty` `CategoryTheory.MorphismProperty` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	`RingHom.PropertyIsLocal.and` `isLocal_ringHomProperty` `eq_affineLocally` `CategoryTheory.MorphismProperty.ext`
`instIsZariskiLocalAtSource` 📖	mathematical	—	`AlgebraicGeometry.IsZariskiLocalAtSource`	—	`AlgebraicGeometry.HasAffineProperty.isZariskiLocalAtSource` `HasAffineProperty` `AlgebraicGeometry.HasAffineProperty.iff_of_isAffine` `iff_of_source_openCover` `AlgebraicGeometry.Scheme.isAffine_affineOpenCover` `AlgebraicGeometry.Scheme.isAffine_affineCover` `CategoryTheory.Category.assoc`
`instIsZariskiLocalAtTarget` 📖	mathematical	—	`AlgebraicGeometry.IsZariskiLocalAtTarget`	—	`AlgebraicGeometry.HasAffineProperty.instIsZariskiLocalAtTarget` `HasAffineProperty`
`isLocal_ringHomProperty` 📖	mathematical	—	`RingHom.PropertyIsLocal`	—	—
`isLocal_ringHomProperty_of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget` 📖	mathematical	—	`RingHom.PropertyIsLocal` `AlgebraicGeometry.Spec` `CommRingCat.of` `AlgebraicGeometry.Spec.map` `CommRingCat.ofHom`	—	`RingHom.toMorphismProperty_respectsIso_iff` `CategoryTheory.MorphismProperty.RespectsIso.unop` `CategoryTheory.MorphismProperty.RespectsIso.inverseImage` `CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects` `RingHom.RespectsIso.isLocalization_away_iff` `CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `AlgebraicGeometry.IsZariskiLocalAtTarget.restrict` `AlgebraicGeometry.IsZariskiLocalAtSource.of_openCover` `Subtype.range_coe_subtype` `AlgebraicGeometry.IsZariskiLocalAtTarget.of_iSup_eq_top` `PrimeSpectrum.iSup_basicOpen_eq_top_iff` `AlgebraicGeometry.IsOpenImmersion.of_isLocalization` `AlgebraicGeometry.Spec.map_comp` `AlgebraicGeometry.IsZariskiLocalAtSource.comp`
`isMultiplicative` 📖	mathematical	`RingHom.StableUnderComposition` `RingHom.ContainsIdentities`	`CategoryTheory.MorphismProperty.IsMultiplicative` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	—	`containsIdentities` `CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem` `stableUnderComposition`
`isStableUnderBaseChange` 📖	mathematical	`RingHom.IsStableUnderBaseChange`	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	—	`AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChange` `HasAffineProperty` `AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.respectsIso` `AlgebraicGeometry.HasAffineProperty.isLocal_affineProperty` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.HasAffineProperty.iff_of_isAffine` `iff_of_isAffine` `AlgebraicGeometry.Scheme.Pullback.isAffine_of_isAffine_isAffine_isAffine` `RingHom.IsStableUnderBaseChange.pullback_fst_appTop` `RingHom.PropertyIsLocal.respectsIso` `isLocal_ringHomProperty` `AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover` `instIsZariskiLocalAtSource` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.Category.comp_id` `comp_of_isOpenImmersion` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `AlgebraicGeometry.Scheme.isAffine_affineCover`
`locally_of_iff` 📖	mathematical	`RingHom.LocalizationAwayPreserves` `RingHom.StableUnderCompositionWithLocalizationAway` `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` `Set` `Set.instMembership` `AlgebraicGeometry.Scheme.affineOpens` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.appLE`	`AlgebraicGeometry.HasRingHomProperty` `RingHom.Locally`	—	`RingHom.locally_propertyIsLocal` `CategoryTheory.MorphismProperty.ext` `iff_exists_appLE_locally` `RingHom.StableUnderCompositionWithLocalizationAway.respectsIso`
`of_comp` 📖	—	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	—	`iff_of_isAffine` `AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_iSup_eq_top` `instIsZariskiLocalAtSource` `AlgebraicGeometry.iSup_affineOpens_eq_top` `comp_of_isOpenImmersion` `AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι` `CategoryTheory.Category.assoc` `AlgebraicGeometry.instIsAffineToSchemeValOpensMemSetAffineOpens` `AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top` `instIsZariskiLocalAtTarget` `AlgebraicGeometry.morphismRestrict_ι_assoc` `AlgebraicGeometry.Scheme.Hom.iSup_preimage_eq_top` `AlgebraicGeometry.IsZariskiLocalAtTarget.restrict` `AlgebraicGeometry.morphismRestrict_comp`
`of_iSup_eq_top` 📖	—	`iSup` `AlgebraicGeometry.Scheme.Opens` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set` `Set.instMembership` `AlgebraicGeometry.Scheme.affineOpens` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.appLE` `le_top`	—	—	`le_top` `of_source_openCover` `AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι` `LE.le.trans` `Set.image_subset_iff` `le_rfl` `AlgebraicGeometry.Scheme.Hom.app_eq_appLE` `AlgebraicGeometry.Scheme.Hom.comp_appLE` `AlgebraicGeometry.Scheme.Opens.ι_appLE` `AlgebraicGeometry.Scheme.Hom.appLE_map` `AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange` `AlgebraicGeometry.Scheme.Opens.opensRange_ι` `AlgebraicGeometry.Scheme.Hom.appLE_congr`
`of_isLocalAtSource_of_isLocalAtTarget` 📖	mathematical	—	`AlgebraicGeometry.HasRingHomProperty` `AlgebraicGeometry.Spec` `CommRingCat.of` `AlgebraicGeometry.Spec.map` `CommRingCat.ofHom`	—	`of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget`
`of_isOpenImmersion` 📖	—	`RingHom.ContainsIdentities`	—	—	`AlgebraicGeometry.IsZariskiLocalAtSource.of_isOpenImmersion` `instIsZariskiLocalAtSource` `containsIdentities`
`of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget` 📖	mathematical	—	`AlgebraicGeometry.HasRingHomProperty` `AlgebraicGeometry.Spec` `CommRingCat.of` `AlgebraicGeometry.Spec.map` `CommRingCat.ofHom`	—	`isLocal_ringHomProperty_of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget` `CategoryTheory.MorphismProperty.ext` `AlgebraicGeometry.Spec.map_preimage` `Spec_iff` `AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover` `instIsZariskiLocalAtSource` `AlgebraicGeometry.Scheme.local_affine` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover` `instIsZariskiLocalAtTarget`
`of_source_openCover` 📖	—	`AlgebraicGeometry.IsAffine` `CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.IsOpenImmersion` `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` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.PreZeroHypercover.f`	—	—	`AlgebraicGeometry.HasAffineProperty.iff_of_isAffine` `HasAffineProperty` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `AlgebraicGeometry.isAffineOpen_opensRange` `AlgebraicGeometry.of_affine_open_cover` `AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange` `le_top` `AlgebraicGeometry.Scheme.basicOpen_le` `LE.le.trans` `AlgebraicGeometry.Scheme.Hom.appLE_map` `AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen` `RingHom.PropertyIsLocal.StableUnderCompositionWithLocalizationAwayTarget` `isLocal_ringHomProperty` `RingHom.OfLocalizationSpanTarget.ofIsLocalization` `RingHom.PropertyIsLocal.ofLocalizationSpanTarget` `RingHom.PropertyIsLocal.respectsIso` `RingHom.algebraMap_toAlgebra` `CommRingCat.hom_comp` `AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι` `le_rfl` `AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange` `AlgebraicGeometry.Scheme.Opens.opensRange_ι` `AlgebraicGeometry.Scheme.Hom.appLE_congr` `Subtype.range_coe` `AlgebraicGeometry.Scheme.Hom.app_eq_appLE` `AlgebraicGeometry.Scheme.Hom.appTop.eq_1` `AlgebraicGeometry.Scheme.Opens.ι_appTop` `AlgebraicGeometry.Scheme.Hom.comp_appTop` `AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac_assoc` `RingHom.RespectsIso.cancel_right_isIso` `AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatApp` `CategoryTheory.Iso.isIso_inv`
`of_stalkMap` 📖	—	`RingHom.OfLocalizationPrime` `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` `RingHom.PropertyIsLocal.respectsIso` `isLocal_ringHomProperty` `AlgebraicGeometry.Spec.map_surjective` `Spec_iff` `PrimeSpectrum.isPrime` `RingHom.RespectsIso.arrow_mk_iso_iff` `CategoryTheory.MorphismProperty.cancel_right_of_respectsIso` `CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects` `instIsZariskiLocalAtSource` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.MorphismProperty.cancel_left_of_respectsIso` `CategoryTheory.Iso.isIso_inv` `AlgebraicGeometry.isAffine_Spec` `AlgebraicGeometry.Scheme.Hom.stalkMap_comp` `CommRingCat.hom_comp` `RingHom.RespectsIso.cancel_right_isIso` `AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `RingHom.RespectsIso.cancel_left_isIso` `AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_iSup_eq_top` `AlgebraicGeometry.iSup_affineOpens_eq_top` `AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι` `AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top` `instIsZariskiLocalAtTarget`
`respects_isOpenImmersion` 📖	mathematical	`RingHom.StableUnderCompositionWithLocalizationAwaySource`	`CategoryTheory.MorphismProperty.Respects` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion`	—	`AlgebraicGeometry.IsZariskiLocalAtSource.respectsLeft_isOpenImmersion` `instIsZariskiLocalAtSource` `AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι` `AlgebraicGeometry.Scheme.Opens.range_ι` `AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac` `CategoryTheory.Category.assoc` `CategoryTheory.MorphismProperty.cancel_right_of_respectsIso` `CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects` `CategoryTheory.Iso.isIso_hom` `AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top` `instIsZariskiLocalAtTarget` `AlgebraicGeometry.iSup_affineOpens_eq_top` `AlgebraicGeometry.morphismRestrict_comp` `AlgebraicGeometry.instIsOpenImmersionMorphismRestrict` `AlgebraicGeometry.IsZariskiLocalAtTarget.restrict`
`stableUnderComposition` 📖	mathematical	`RingHom.StableUnderComposition`	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	—	`iff_of_isAffine` `AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover` `instIsZariskiLocalAtSource` `CategoryTheory.Category.assoc` `comp_of_isOpenImmersion` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `AlgebraicGeometry.Scheme.isAffine_affineCover` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.Scheme.Cover.pullbackHom_map_assoc` `AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback` `instIsZariskiLocalAtTarget` `CategoryTheory.IsPullback.of_hasPullback` `AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top` `AlgebraicGeometry.iSup_affineOpens_eq_top` `AlgebraicGeometry.morphismRestrict_comp` `AlgebraicGeometry.IsZariskiLocalAtTarget.restrict`
`stalkMap` 📖	mathematical	`Localization.AtPrime` `CommRing.toCommSemiring` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Localization.localRingHom` `Ideal`	`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`	—	`RingHom.instRingHomClass` `Ideal.IsPrime.comap` `stalkMap_of_respectsIso` `RingHom.PropertyIsLocal.respectsIso` `isLocal_ringHomProperty`
`stalkMap_of_respectsIso` 📖	mathematical	`RingHom.RespectsIso` `Localization.AtPrime` `CommRing.toCommSemiring` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Localization.localRingHom` `Ideal`	`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`	—	`RingHom.instRingHomClass` `Ideal.IsPrime.comap` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.Spec.map_surjective` `PrimeSpectrum.isPrime` `RingHom.RespectsIso.arrow_mk_iso_iff` `Spec_iff` `CategoryTheory.MorphismProperty.cancel_left_of_respectsIso` `CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects` `instIsZariskiLocalAtSource` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.MorphismProperty.cancel_right_of_respectsIso` `CategoryTheory.Iso.isIso_hom` `AlgebraicGeometry.isAffine_Spec` `AlgebraicGeometry.Scheme.hom_inv_apply` `RingHom.RespectsIso.cancel_left_isIso` `AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CommRingCat.hom_comp` `RingHom.RespectsIso.cancel_right_isIso` `AlgebraicGeometry.Scheme.Hom.stalkMap_comp` `TopologicalSpace.Opens.isBasis_iff_nbhd` `AlgebraicGeometry.Scheme.isBasis_affineOpens` `TopologicalSpace.Opens.mem_top` `AlgebraicGeometry.IsZariskiLocalAtSource.resLE` `instIsZariskiLocalAtTarget`
`stalkwise` 📖	mathematical	`RingHom.RespectsIso`	`AlgebraicGeometry.HasRingHomProperty` `AlgebraicGeometry.stalkwise`	—	`AlgebraicGeometry.stalkwiseIsZariskiLocalAtTarget_of_respectsIso` `AlgebraicGeometry.stalkwise_isZariskiLocalAtSource_of_respectsIso` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `AlgebraicGeometry.stalkwise_SpecMap_iff` `of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget`

RingHom.IsStableUnderBaseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pullback_fst_appTop` 📖	mathematical	`RingHom.IsStableUnderBaseChange` `RingHom.RespectsIso` `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`	`CategoryTheory.Limits.pullback` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.fst`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasLimits` `AlgebraicGeometry.AffineScheme.hasLimits` `CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit` `AlgebraicGeometry.Scheme.Pullback.instHasPullbacks` `CategoryTheory.Limits.PreservesPullback.iso_inv_fst` `AlgebraicGeometry.Scheme.Hom.comp_appTop` `CommRingCat.hom_comp` `RingHom.RespectsIso.cancel_right_isIso` `AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatApp` `CategoryTheory.Iso.isIso_inv` `AlgebraicGeometry.AffineScheme.forgetToScheme_map` `CategoryTheory.Limits.hasPullbacks_opposite` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.AffineScheme.instIsEquivalenceOppositeCommRingCatRightOpΓ` `CategoryTheory.Limits.PreservesPullback.iso_hom_fst` `CategoryTheory.isIso_unop` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom` `pushout_inl`

---

← Back to Index