Constructors

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

Statistics

Metric	Count
Definitions `diagonal`, `stalkwise`, `topologically`	3
Theorems `diagonal_of_openCover_source`, `diagonal_respectsIso`, `isStableUnderBaseChange_of_isStableUnderBaseChangeOnAffine_of_isZariskiLocalAtTarget`, `diagonal_affineProperty_isLocal`, `diagonal_iff`, `diagonal_of_diagonal_of_isPullback`, `diagonal_of_openCover`, `diagonal_of_openCover_diagonal`, `instHasAffinePropertyDiagonalSchemeDiagonal`, `instIsZariskiLocalAtSourceDiagonalSchemeOfHasOfPostcompPropertyOfRespectsRightIsOpenImmersion`, `instIsZariskiLocalAtTargetDiagonalScheme`, `stalkwiseIsLocalAtTarget_of_respectsIso`, `stalkwiseIsZariskiLocalAtTarget_of_respectsIso`, `stalkwise_SpecMap_iff`, `stalkwise_Spec_map_iff`, `stalkwise_isLocalAtSource_of_respectsIso`, `stalkwise_isZariskiLocalAtSource_of_respectsIso`, `stalkwise_respectsIso`, `topologically_isLocalAtSource`, `topologically_isLocalAtSource'`, `topologically_isLocalAtTarget`, `topologically_isLocalAtTarget'`, `topologically_isStableUnderComposition`, `topologically_isZariskiLocalAtSource`, `topologically_isZariskiLocalAtSource'`, `topologically_isZariskiLocalAtTarget`, `topologically_isZariskiLocalAtTarget'`, `topologically_iso_le`, `topologically_respectsIso`, `universally_isLocalAtSource`, `universally_isLocalAtTarget`, `universally_isZariskiLocalAtSource`, `universally_isZariskiLocalAtTarget`	33
Total	36

AlgebraicGeometry

Definitions

Name	Category	Theorems
`stalkwise` 📖	CompOp	12 math math: `SurjectiveOnStalks.eq_stalkwise`, `stalkwiseIsLocalAtTarget_of_respectsIso`, `stalkwise_SpecMap_iff`, `stalkwise_isZariskiLocalAtSource_of_respectsIso`, `stalkwiseIsZariskiLocalAtTarget_of_respectsIso`, `stalkwise_respectsIso`, `HasRingHomProperty.stalkwise`, `isOpenImmersion_eq_inf`, `instIsZariskiLocalAtTargetStalkwiseBijectiveCoeRingHom`, `stalkwise_Spec_map_iff`, `isomorphisms_eq_stalkwise`, `stalkwise_isLocalAtSource_of_respectsIso`
`topologically` 📖	CompOp	51 math math: `injective_isStableUnderComposition`, `isClosedEmbedding_isZariskiLocalAtTarget`, `topologically_isZariskiLocalAtTarget'`, `topologically_isZariskiLocalAtTarget`, `isImmersion_eq_inf`, `UniversallyOpen.out`, `isOpenMap_isZariskiLocalAtTarget`, `instIsZariskiLocalAtSourceTopologicallyGeneralizingMap`, `isOpenEmbedding_isZariskiLocalAtTarget`, `injective_isZariskiLocalAtTarget`, `topologically_isLocalAtSource`, `specializingMap_isZariskiLocalAtTarget`, `universallyInjective_iff`, `ValuativeCriterion.Existence.eq`, `instRespectsIsoSchemeTopologicallyIsOpenEmbedding`, `topologically_iso_le`, `instRespectsIsoSchemeTopologicallyIsClosedEmbedding`, `universallyInjective_eq`, `isClosedMap_isZariskiLocalAtTarget`, `specializingMap_respectsIso`, `UniversallyClosed.out`, `topologically_isZariskiLocalAtSource'`, `topologically_isZariskiLocalAtSource`, `UniversallyOpen.instIsStableUnderCompositionSchemeTopologicallyIsOpenMap`, `topologically_isLocalAtSource'`, `isOpenImmersion_eq_inf`, `IsClosedImmersion.eq_inf`, `isClosedMap_isStableUnderComposition`, `topologically_isLocalAtTarget`, `isPreimmersion_eq_inf`, `UniversallyOpen.eq`, `UniversallyOpen.universally_isOpenMap`, `universallyOpen_iff`, `UniversallyClosed.universally_isClosedMap`, `universallyClosed_eq_universallySpecializing`, `topologically_respectsIso`, `instRespectsIsoSchemeTopologicallyInjective`, `surjective_eq_topologically`, `topologically_isStableUnderComposition`, `instRespectsIsoSchemeTopologicallyIsClosedMap`, `instRespectsIsoSchemeTopologicallyGeneralizingMap`, `instIsZariskiLocalAtTargetTopologicallyGeneralizingMap`, `universallyClosed_iff`, `instIsZariskiLocalAtSourceTopologicallyIsOpenMap`, `dominant_eq_topologically`, `universallyClosed_eq`, `isEmbedding_isZariskiLocalAtTarget`, `topologically_isLocalAtTarget'`, `instRespectsIsoSchemeTopologicallyIsOpenMap`, `instRespectsIsoSchemeTopologicallyIsEmbedding`, `UniversallyInjective.universally_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasAffinePropertyDiagonalSchemeDiagonal` 📖	mathematical	—	`HasAffineProperty` `CategoryTheory.MorphismProperty.diagonal` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullbacks` `AffineTargetMorphismProperty.diagonal`	—	`Scheme.Pullback.instHasPullbacks` `HasAffineProperty.diagonal_affineProperty_isLocal` `HasAffineProperty.isLocal_affineProperty` `CategoryTheory.MorphismProperty.ext` `HasAffineProperty.diagonal_of_diagonal_of_isPullback` `instIsAffineToSchemeValOpensMemSetAffineOpens` `Scheme.Opens.instIsOpenImmersionι` `CategoryTheory.IsPullback.flip` `isPullback_morphismRestrict` `HasAffineProperty.diagonal_of_openCover_diagonal` `Scheme.isAffine_affineCover` `of_targetAffineLocally_of_isPullback` `Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `isOpenImmersion_stableUnderBaseChange` `Scheme.Pullback.instHasPullback` `Scheme.instIsOpenImmersionF` `CategoryTheory.IsPullback.of_hasPullback`
`instIsZariskiLocalAtSourceDiagonalSchemeOfHasOfPostcompPropertyOfRespectsRightIsOpenImmersion` 📖	mathematical	—	`IsZariskiLocalAtSource` `CategoryTheory.MorphismProperty.diagonal` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullbacks`	—	`Scheme.Pullback.instHasPullback` `CategoryTheory.Category.comp_id` `IsZariskiLocalAtSource.mk'` `Scheme.Pullback.instHasPullbacks` `CategoryTheory.MorphismProperty.RespectsIso.diagonal` `CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects` `CategoryTheory.MorphismProperty.of_postcomp` `Scheme.pullback_map_isOpenImmersion` `Scheme.Opens.instIsOpenImmersionι` `IsOpenImmersion.mono` `IsOpenImmersion.of_isIso` `CategoryTheory.IsIso.id` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasPullbackHorizPaste` `CategoryTheory.Limits.hasPullbackVertPaste` `CategoryTheory.IsPullback.instHasPullbackFst` `CategoryTheory.Limits.pullback.comp_diagonal` `IsZariskiLocalAtSource.comp` `IsZariskiLocalAtSource.of_iSup_eq_top` `CategoryTheory.MorphismProperty.RespectsRight.postcomp`
`instIsZariskiLocalAtTargetDiagonalScheme` 📖	mathematical	—	`IsZariskiLocalAtTarget` `CategoryTheory.MorphismProperty.diagonal` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullbacks`	—	`Scheme.Pullback.instHasPullbacks` `HasAffineProperty.instIsZariskiLocalAtTarget` `instHasAffinePropertyDiagonalSchemeDiagonal` `HasAffineProperty.of_isZariskiLocalAtTarget`
`stalkwiseIsLocalAtTarget_of_respectsIso` 📖	mathematical	`RingHom.RespectsIso`	`IsZariskiLocalAtTarget` `stalkwise`	—	`stalkwiseIsZariskiLocalAtTarget_of_respectsIso`
`stalkwiseIsZariskiLocalAtTarget_of_respectsIso` 📖	mathematical	`RingHom.RespectsIso`	`IsZariskiLocalAtTarget` `stalkwise`	—	`RingHom.toMorphismProperty_respectsIso_iff` `IsZariskiLocalAtTarget.mk'` `stalkwise_respectsIso` `CommRingCat.Colimits.hasColimits_commRingCat` `CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `TopologicalSpace.Opens.mem_iSup`
`stalkwise_SpecMap_iff` 📖	mathematical	`RingHom.RespectsIso`	`stalkwise` `Spec` `Spec.map` `Localization.AtPrime` `CommRingCat.carrier` `CommRing.toCommSemiring` `CommRingCat.commRing` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `CommRingCat.Hom.hom` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Localization.localRingHom` `Ideal`	—	`RingHom.toMorphismProperty_respectsIso_iff` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `PrimeSpectrum.isPrime` `CommRingCat.Colimits.hasColimits_commRingCat` `CategoryTheory.MorphismProperty.arrow_mk_iso_iff`
`stalkwise_Spec_map_iff` 📖	mathematical	`RingHom.RespectsIso`	`stalkwise` `Spec` `Spec.map` `Localization.AtPrime` `CommRingCat.carrier` `CommRing.toCommSemiring` `CommRingCat.commRing` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `CommRingCat.Hom.hom` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Localization.localRingHom` `Ideal`	—	`stalkwise_SpecMap_iff`
`stalkwise_isLocalAtSource_of_respectsIso` 📖	mathematical	`RingHom.RespectsIso`	`IsZariskiLocalAtSource` `stalkwise`	—	`stalkwise_isZariskiLocalAtSource_of_respectsIso`
`stalkwise_isZariskiLocalAtSource_of_respectsIso` 📖	mathematical	`RingHom.RespectsIso`	`IsZariskiLocalAtSource` `stalkwise`	—	`IsZariskiLocalAtSource.mk'` `stalkwise_respectsIso` `CommRingCat.Colimits.hasColimits_commRingCat` `Scheme.Hom.stalkMap_comp` `CommRingCat.hom_comp` `RingHom.RespectsIso.cancel_right_isIso` `IsOpenImmersion.instIsIsoCommRingCatStalkMap` `Scheme.Opens.instIsOpenImmersionι` `TopologicalSpace.Opens.mem_iSup`
`stalkwise_respectsIso` 📖	mathematical	`RingHom.RespectsIso`	`CategoryTheory.MorphismProperty.RespectsIso` `Scheme` `Scheme.instCategory` `stalkwise`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `Scheme.Hom.stalkMap_comp` `RingHom.RespectsIso.cancel_right_isIso` `IsOpenImmersion.instIsIsoCommRingCatStalkMap` `IsOpenImmersion.of_isIso` `RingHom.RespectsIso.cancel_left_isIso`
`topologically_isLocalAtSource` 📖	mathematical	`TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype`	`IsZariskiLocalAtSource` `topologically`	—	`topologically_isZariskiLocalAtSource`
`topologically_isLocalAtSource'` 📖	mathematical	`TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype`	`IsZariskiLocalAtSource` `topologically`	—	`topologically_isZariskiLocalAtSource'`
`topologically_isLocalAtTarget` 📖	mathematical	`Set.Elem` `Set.preimage` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrictPreimage`	`IsZariskiLocalAtTarget` `topologically`	—	`topologically_isZariskiLocalAtTarget`
`topologically_isLocalAtTarget'` 📖	mathematical	`Set.Elem` `Set.preimage` `TopologicalSpace.Opens.carrier` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrictPreimage`	`IsZariskiLocalAtTarget` `topologically`	—	`topologically_isZariskiLocalAtTarget'`
`topologically_isStableUnderComposition` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `Scheme` `Scheme.instCategory` `topologically`	—	—
`topologically_isZariskiLocalAtSource` 📖	mathematical	`TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype`	`IsZariskiLocalAtSource` `topologically`	—	`IsZariskiLocalAtSource.mk'` `Scheme.Hom.continuous`
`topologically_isZariskiLocalAtSource'` 📖	mathematical	`TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype`	`IsZariskiLocalAtSource` `topologically`	—	`topologically_isZariskiLocalAtSource` `TopologicalSpace.IsOpenCover.eq_1` `top_le_iff` `le_iSup`
`topologically_isZariskiLocalAtTarget` 📖	mathematical	`Set.Elem` `Set.preimage` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrictPreimage`	`IsZariskiLocalAtTarget` `topologically`	—	`IsZariskiLocalAtTarget.mk'` `morphismRestrict_base` `Scheme.Hom.continuous` `TopologicalSpace.Opens.is_open'`
`topologically_isZariskiLocalAtTarget'` 📖	mathematical	`Set.Elem` `Set.preimage` `TopologicalSpace.Opens.carrier` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrictPreimage`	`IsZariskiLocalAtTarget` `topologically`	—	`topologically_isZariskiLocalAtTarget` `TopologicalSpace.IsOpenCover.eq_1` `top_le_iff` `le_iSup`
`topologically_iso_le` 📖	mathematical	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	`CategoryTheory.MorphismProperty` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.isomorphisms` `topologically`	—	`Scheme.Hom.isIso_base`
`topologically_respectsIso` 📖	mathematical	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	`CategoryTheory.MorphismProperty.RespectsIso` `Scheme` `Scheme.instCategory` `topologically`	—	`topologically_isStableUnderComposition` `CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition` `topologically_iso_le`
`universally_isLocalAtSource` 📖	mathematical	—	`IsZariskiLocalAtSource` `CategoryTheory.MorphismProperty.universally` `Scheme` `Scheme.instCategory`	—	`universally_isZariskiLocalAtSource`
`universally_isLocalAtTarget` 📖	mathematical	—	`IsZariskiLocalAtTarget` `CategoryTheory.MorphismProperty.universally` `Scheme` `Scheme.instCategory`	—	`universally_isZariskiLocalAtTarget`
`universally_isZariskiLocalAtSource` 📖	mathematical	—	`IsZariskiLocalAtSource` `CategoryTheory.MorphismProperty.universally` `Scheme` `Scheme.instCategory`	—	`CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_iff` `CategoryTheory.MorphismProperty.universally_respectsIso` `CategoryTheory.MorphismProperty.universally_mk'` `CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects` `Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.hasPullbackVertPaste` `CategoryTheory.MorphismProperty.cancel_left_of_respectsIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_fst` `IsZariskiLocalAtSource.comp` `CategoryTheory.IsPullback.of_hasPullback` `IsOpenImmersion.instFstScheme` `Scheme.instIsOpenImmersionF` `Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `isOpenImmersion_stableUnderBaseChange` `IsZariskiLocalAtSource.iff_of_openCover`
`universally_isZariskiLocalAtTarget` 📖	mathematical	—	`IsZariskiLocalAtTarget` `CategoryTheory.MorphismProperty.universally` `Scheme` `Scheme.instCategory`	—	`IsZariskiLocalAtTarget.mk'` `CategoryTheory.MorphismProperty.universally_respectsIso` `CategoryTheory.MorphismProperty.of_isPullback` `CategoryTheory.MorphismProperty.universally_isStableUnderBaseChange` `CategoryTheory.IsPullback.flip` `isPullback_morphismRestrict` `isOpen_iUnion` `TopologicalSpace.Opens.is_open'` `CategoryTheory.CommSq.w` `CategoryTheory.IsPullback.toCommSq` `CategoryTheory.IsPullback.paste_vert_iff` `CategoryTheory.cancel_mono` `IsOpenImmersion.mono` `Scheme.Opens.instIsOpenImmersionι` `CategoryTheory.Category.assoc` `morphismRestrict_ι` `morphismRestrict_ι_assoc` `Scheme.isoOfEq_hom_ι_assoc` `CategoryTheory.IsPullback.paste_vert`

AlgebraicGeometry.AffineTargetMorphismProperty

Definitions

Name	Category	Theorems
`diagonal` 📖	CompOp	7 math math: `AlgebraicGeometry.HasAffineProperty.diagonal_of_diagonal_of_isPullback`, `AlgebraicGeometry.HasAffineProperty.diagonal_iff`, `AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace`, `AlgebraicGeometry.HasAffineProperty.diagonal_affineProperty_isLocal`, `diagonal_respectsIso`, `AlgebraicGeometry.instHasAffinePropertyDiagonalSchemeDiagonal`, `diagonal_of_openCover_source`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diagonal_of_openCover_source` 📖	mathematical	`AlgebraicGeometry.IsAffine` `CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Limits.pullback` `CategoryTheory.PreZeroHypercover.f` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.pullback.mapDesc` `AlgebraicGeometry.Scheme.Pullback.isAffine_of_isAffine_isAffine_isAffine`	`diagonal`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.Scheme.Pullback.isAffine_of_isAffine_isAffine_isAffine` `AlgebraicGeometry.Scheme.Pullback.instHasPullbacks` `AlgebraicGeometry.HasAffineProperty.diagonal_iff` `AlgebraicGeometry.HasAffineProperty.instTargetAffineLocallyOfIsLocal` `AlgebraicGeometry.HasAffineProperty.of_openCover` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `CategoryTheory.Category.comp_id` `CategoryTheory.IsPullback.of_iso` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasPullbackHorizPaste` `CategoryTheory.Limits.hasPullbackVertPaste` `CategoryTheory.IsPullback.instHasPullbackFst` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.pullback_fst_map_snd_isPullback` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.Limits.pullback.map_isIso` `CategoryTheory.IsIso.id` `CategoryTheory.Limits.pullback_fst_iso_of_right_iso` `CategoryTheory.Limits.limit.lift_π_assoc` `CategoryTheory.Limits.pullback.hom_ext` `CategoryTheory.Limits.pullback.map.congr_simp` `cancel_left_of_respectsIso` `IsLocal.respectsIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.IsPullback.isoPullback_hom_snd`
`diagonal_respectsIso` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `toProperty` `diagonal`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.pullback.mapDesc_comp` `cancel_left_of_respectsIso` `CategoryTheory.Limits.pullback.map_isIso` `CategoryTheory.IsIso.id` `CategoryTheory.Iso.isIso_hom` `AlgebraicGeometry.Scheme.Pullback.isAffine_of_isAffine_isAffine_isAffine` `cancel_right_of_respectsIso` `AlgebraicGeometry.IsOpenImmersion.comp` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `AlgebraicGeometry.IsAffine.of_isIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.IsIso.comp_isIso`
`isStableUnderBaseChange_of_isStableUnderBaseChangeOnAffine_of_isZariskiLocalAtTarget` 📖	mathematical	`IsStableUnderBaseChange` `of`	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	—	`AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChange` `AlgebraicGeometry.HasAffineProperty.of_isZariskiLocalAtTarget`

AlgebraicGeometry.HasAffineProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diagonal_affineProperty_isLocal` 📖	mathematical	—	`AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal` `AlgebraicGeometry.AffineTargetMorphismProperty.diagonal`	—	`AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_respectsIso` `AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.respectsIso` `diagonal_of_diagonal_of_isPullback` `instTargetAffineLocallyOfIsLocal` `AlgebraicGeometry.IsAffineOpen.instIsAffineToSchemeBasicOpen` `AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι` `CategoryTheory.IsPullback.flip` `AlgebraicGeometry.isPullback_morphismRestrict` `AlgebraicGeometry.Scheme.Pullback.instHasPullbacks` `diagonal_iff` `AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff` `AlgebraicGeometry.isAffineOpen_top` `AlgebraicGeometry.IsAffineOpen.basicOpen` `diagonal_of_openCover_diagonal` `AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `AlgebraicGeometry.IsAffine.of_isIso` `AlgebraicGeometry.Scheme.Opens.opensRange_ι` `CategoryTheory.Arrow.isIso_right` `CategoryTheory.Iso.isIso_inv` `AlgebraicGeometry.AffineTargetMorphismProperty.arrow_mk_iso_iff`
`diagonal_iff` 📖	mathematical	—	`AlgebraicGeometry.AffineTargetMorphismProperty.diagonal` `CategoryTheory.MorphismProperty.diagonal` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullbacks`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullbacks` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.isOpenImmersion_respectsIso` `CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities` `AlgebraicGeometry.isOpenImmersion_isMultiplicative` `AlgebraicGeometry.isOpenImmersion_isStableUnderComposition` `CategoryTheory.Limits.pullback_fst_iso_of_right_iso` `CategoryTheory.IsIso.id` `CategoryTheory.IsIso.inv_isIso` `AlgebraicGeometry.Scheme.isAffine_affineCover` `diagonal_of_openCover` `AlgebraicGeometry.instIsAffineXSchemeCoverOfIsIsoIsOpenImmersionId` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.pullback.condition` `AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso` `AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_respectsIso` `AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.respectsIso` `isLocal_affineProperty` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `diagonal_of_diagonal_of_isPullback` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.IsPullback.of_id_fst`
`diagonal_of_diagonal_of_isPullback` 📖	mathematical	`CategoryTheory.IsPullback` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.MorphismProperty.diagonal` `AlgebraicGeometry.Scheme.Pullback.instHasPullbacks`	`AlgebraicGeometry.AffineTargetMorphismProperty.diagonal`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullbacks` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso` `AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_respectsIso` `AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.respectsIso` `isLocal_affineProperty` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.IsPullback.isoPullback_inv_snd` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasPullbackHorizPaste` `CategoryTheory.Limits.hasPullbackVertPaste` `CategoryTheory.IsPullback.instHasPullbackFst` `CategoryTheory.Iso.isIso_hom` `AlgebraicGeometry.Scheme.Pullback.isAffine_of_isAffine_isAffine_isAffine` `CategoryTheory.Limits.pullback.hom_ext` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst` `CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd` `of_isPullback` `AlgebraicGeometry.Scheme.pullback_map_isOpenImmersion` `AlgebraicGeometry.IsOpenImmersion.comp` `AlgebraicGeometry.IsOpenImmersion.instFstScheme` `AlgebraicGeometry.IsOpenImmersion.mono` `CategoryTheory.IsPullback.of_hasPullback`
`diagonal_of_openCover` 📖	mathematical	`AlgebraicGeometry.IsAffine` `CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Limits.pullback` `CategoryTheory.PreZeroHypercover.f` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.Cover.pullbackHom` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `CategoryTheory.Limits.pullback.mapDesc` `AlgebraicGeometry.Scheme.Pullback.isAffine_of_isAffine_isAffine_isAffine`	`CategoryTheory.MorphismProperty.diagonal` `AlgebraicGeometry.Scheme.Pullback.instHasPullbacks`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.Scheme.Pullback.isAffine_of_isAffine_isAffine_isAffine` `AlgebraicGeometry.Scheme.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition` `AlgebraicGeometry.isOpenImmersion_isStableUnderComposition` `of_openCover` `AlgebraicGeometry.Scheme.Pullback.instHasPullbacks` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasPullbackHorizPaste` `CategoryTheory.Limits.hasPullbackVertPaste` `CategoryTheory.IsPullback.instHasPullbackFst` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.pullback.hom_ext` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.limit.lift_π_assoc` `AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso` `AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.respectsIso` `isLocal_affineProperty` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Limits.pullback.map_isIso` `CategoryTheory.IsIso.id` `CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst` `CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd`
`diagonal_of_openCover_diagonal` 📖	mathematical	`AlgebraicGeometry.IsAffine` `CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.IsOpenImmersion` `AlgebraicGeometry.AffineTargetMorphismProperty.diagonal` `CategoryTheory.Precoverage.ZeroHypercover.pullback₁` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.PreZeroHypercover.f` `AlgebraicGeometry.Scheme.Cover.pullbackHom`	`CategoryTheory.MorphismProperty.diagonal` `AlgebraicGeometry.Scheme.Pullback.instHasPullbacks`	—	`AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `diagonal_of_openCover` `AlgebraicGeometry.Scheme.isAffine_affineCover` `AlgebraicGeometry.Scheme.instIsOpenImmersionF`

---

← Back to Index