Documentation Verification Report

AffineAnd

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

Statistics

Metric	Count
Definitions `affineAnd`	1
Theorems `SpecMap_iff_of_affineAnd`, `affineAnd_containsIdentities`, `affineAnd_eq_of_propertyIsLocal`, `affineAnd_iff`, `affineAnd_isStableUnderBaseChange`, `affineAnd_isStableUnderComposition`, `affineAnd_le_affineAnd`, `affineAnd_le_isAffineHom`, `coprodDesc_affineAnd`, `affineAnd_apply`, `affineAnd_isLocal`, `affineAnd_isLocal_of_propertyIsLocal`, `affineAnd_isStableUnderBaseChange`, `affineAnd_respectsIso`, `targetAffineLocally_affineAnd_eq_affineLocally`, `targetAffineLocally_affineAnd_iff`, `targetAffineLocally_affineAnd_iff'`, `targetAffineLocally_affineAnd_iff_affineLocally`, `targetAffineLocally_affineAnd_le`	19
Total	20

AlgebraicGeometry

Definitions

Name	Category	Theorems
`affineAnd` 📖	CompOp	11 math math: `affineAnd_isLocal`, `affineAnd_respectsIso`, `affineAnd_isLocal_of_propertyIsLocal`, `targetAffineLocally_affineAnd_iff`, `targetAffineLocally_affineAnd_eq_affineLocally`, `HasAffineProperty.affineAnd_iff`, `affineAnd_apply`, `targetAffineLocally_affineAnd_iff'`, `targetAffineLocally_affineAnd_le`, `targetAffineLocally_affineAnd_iff_affineLocally`, `affineAnd_isStableUnderBaseChange`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineAnd_apply` 📖	mathematical	—	`affineAnd` `IsAffine` `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` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CommRingCat.commRing` `CommRingCat.Hom.hom` `Scheme.Hom.appTop`	—	—
`affineAnd_isLocal` 📖	mathematical	`RingHom.RespectsIso` `RingHom.LocalizationAwayPreserves` `RingHom.OfLocalizationSpan`	`AffineTargetMorphismProperty.IsLocal` `affineAnd`	—	`affineAnd_respectsIso` `IsAffineOpen.instIsAffineToSchemeBasicOpen` `Scheme.preimage_basicOpen` `IsAffineOpen.basicOpen` `isAffineOpen_top` `Scheme.Opens.instIsOpenImmersionι` `image_morphismRestrict_preimage` `morphismRestrict_appTop` `CommRingCat.hom_comp` `RingHom.RespectsIso.cancel_right_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.isIso_op` `CategoryTheory.instIsIsoEqToHom` `Scheme.Opens.ι_image_top` `IsAffineOpen.isLocalization_basicOpen` `IsAffineOpen.app_basicOpen_eq_away_map` `Scheme.Hom.appTop.eq_1` `isAffine_of_isAffineOpen_basicOpen` `Ideal.map_top` `RingHom.instRingHomClass` `Ideal.map_span` `RingHom.OfLocalizationSpan.ofIsLocalization'` `isLocalization_away_of_isAffine`
`affineAnd_isLocal_of_propertyIsLocal` 📖	mathematical	`RingHom.PropertyIsLocal`	`AffineTargetMorphismProperty.IsLocal` `affineAnd`	—	`affineAnd_isLocal` `RingHom.PropertyIsLocal.respectsIso` `RingHom.PropertyIsLocal.localizationAwayPreserves` `RingHom.PropertyIsLocal.ofLocalizationSpan`
`affineAnd_isStableUnderBaseChange` 📖	mathematical	`RingHom.RespectsIso` `RingHom.IsStableUnderBaseChange`	`AffineTargetMorphismProperty.IsStableUnderBaseChange` `affineAnd`	—	`affineAnd_respectsIso` `Scheme.Pullback.instHasPullback` `instIsAffinePullbackSchemeOfIsAffineHom_1` `isAffineHom_of_isAffine` `RingHom.IsStableUnderBaseChange.pullback_fst_appTop`
`affineAnd_respectsIso` 📖	mathematical	`RingHom.RespectsIso`	`CategoryTheory.MorphismProperty.RespectsIso` `Scheme` `Scheme.instCategory` `AffineTargetMorphismProperty.toProperty` `affineAnd`	—	`IsAffine.of_isIso` `CategoryTheory.Iso.isIso_hom` `RingHom.RespectsIso.cancel_right_isIso` `Scheme.Hom.instIsIsoCommRingCatApp` `RingHom.RespectsIso.cancel_left_isIso` `CategoryTheory.Iso.isIso_inv`
`targetAffineLocally_affineAnd_eq_affineLocally` 📖	mathematical	`RingHom.PropertyIsLocal`	`targetAffineLocally` `affineAnd` `CategoryTheory.MorphismProperty` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `IsAffineHom` `affineLocally`	—	`CategoryTheory.MorphismProperty.ext` `targetAffineLocally_affineAnd_iff_affineLocally`
`targetAffineLocally_affineAnd_iff` 📖	mathematical	`RingHom.RespectsIso`	`targetAffineLocally` `affineAnd` `IsAffineOpen` `CategoryTheory.Functor.obj` `Scheme.Opens` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `CommRingCat.carrier` `Opposite` `TopologicalSpace.Opens` `TopCat.str` `CategoryTheory.Category.opposite` `PresheafedSpace.presheaf` `Opposite.op` `CommRingCat.commRing` `CommRingCat.Hom.hom` `Scheme.Hom.app`	—	`Scheme.Opens.instIsOpenImmersionι` `instIsAffineToSchemeValOpensMemSetAffineOpens` `image_morphismRestrict_preimage` `morphismRestrict_app` `RingHom.RespectsIso.cancel_right_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.isIso_op` `CategoryTheory.instIsIsoEqToHom` `Scheme.Opens.ι_image_top`
`targetAffineLocally_affineAnd_iff'` 📖	mathematical	`RingHom.RespectsIso`	`targetAffineLocally` `affineAnd` `IsAffineHom` `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` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `CommRingCat.commRing` `CommRingCat.Hom.hom` `Scheme.Hom.app`	—	`targetAffineLocally_affineAnd_iff` `isAffineHom_iff`
`targetAffineLocally_affineAnd_iff_affineLocally` 📖	mathematical	`RingHom.PropertyIsLocal`	`targetAffineLocally` `affineAnd` `IsAffineHom` `affineLocally`	—	`targetAffineLocally_affineAnd_iff'` `RingHom.PropertyIsLocal.respectsIso` `isAffine_of_isAffineHom` `HasRingHomProperty.iff_of_isAffine` `isAffineOpen_top` `IsZariskiLocalAtTarget.iff_of_iSup_eq_top` `HasRingHomProperty.instIsZariskiLocalAtTarget` `iSup_affineOpens_eq_top` `IsAffineHom.isAffine_preimage` `instIsAffineToSchemeValOpensMemSetAffineOpens` `Scheme.Opens.instIsOpenImmersionι` `image_morphismRestrict_preimage` `morphismRestrict_appTop` `CommRingCat.hom_comp` `RingHom.RespectsIso.cancel_right_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.isIso_op` `CategoryTheory.instIsIsoEqToHom` `Scheme.Opens.ι_image_top` `le_rfl` `Scheme.Hom.app_eq_appLE` `affineLocally_iff_affineOpens_le`
`targetAffineLocally_affineAnd_le` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `targetAffineLocally` `affineAnd`	—	—

AlgebraicGeometry.HasAffineProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SpecMap_iff_of_affineAnd` 📖	mathematical	`RingHom.RespectsIso`	`AlgebraicGeometry.Spec` `AlgebraicGeometry.Spec.map` `CommRingCat.carrier` `CommRingCat.commRing` `CommRingCat.Hom.hom`	—	`RingHom.toMorphismProperty_respectsIso_iff` `AlgebraicGeometry.isAffine_Spec` `iff_of_isAffine` `AlgebraicGeometry.affineAnd.eq_1` `CategoryTheory.MorphismProperty.arrow_mk_iso_iff`
`affineAnd_containsIdentities` 📖	mathematical	`RingHom.RespectsIso` `RingHom.ContainsIdentities`	`CategoryTheory.MorphismProperty.ContainsIdentities` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	—	`eq_targetAffineLocally` `AlgebraicGeometry.targetAffineLocally_affineAnd_iff`
`affineAnd_eq_of_propertyIsLocal` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `AlgebraicGeometry.IsAffineHom`	—	`eq_targetAffineLocally` `AlgebraicGeometry.targetAffineLocally_affineAnd_eq_affineLocally` `AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty` `AlgebraicGeometry.HasRingHomProperty.eq_affineLocally`
`affineAnd_iff` 📖	mathematical	`RingHom.RespectsIso` `RingHom.LocalizationAwayPreserves` `RingHom.OfLocalizationSpan`	`AlgebraicGeometry.HasAffineProperty` `AlgebraicGeometry.affineAnd` `AlgebraicGeometry.IsAffineHom` `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` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.app`	—	`eq_targetAffineLocally` `AlgebraicGeometry.targetAffineLocally_affineAnd_iff` `AlgebraicGeometry.affineAnd_isLocal` `CategoryTheory.MorphismProperty.ext`
`affineAnd_isStableUnderBaseChange` 📖	mathematical	`RingHom.RespectsIso` `RingHom.IsStableUnderBaseChange`	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	—	`isStableUnderBaseChange` `AlgebraicGeometry.affineAnd_isStableUnderBaseChange`
`affineAnd_isStableUnderComposition` 📖	mathematical	`RingHom.StableUnderComposition`	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	—	`iff_of_isAffine` `AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top` `instIsZariskiLocalAtTarget` `AlgebraicGeometry.iSup_affineOpens_eq_top` `AlgebraicGeometry.morphismRestrict_comp` `AlgebraicGeometry.IsZariskiLocalAtTarget.restrict`
`affineAnd_le_affineAnd` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	`eq_targetAffineLocally` `AlgebraicGeometry.targetAffineLocally_affineAnd_le`
`affineAnd_le_isAffineHom` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `AlgebraicGeometry.IsAffineHom`	—	`iff_of_isAffine` `AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine` `AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top` `instIsZariskiLocalAtTarget` `AlgebraicGeometry.iSup_affineOpens_eq_top` `AlgebraicGeometry.IsZariskiLocalAtTarget.restrict`
`coprodDesc_affineAnd` 📖	mathematical	`RingHom.RespectsIso` `Prod.instCommRing` `RingHom.prod` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`CategoryTheory.Limits.coprod` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `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` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.coprod.desc`	—	`affineAnd_le_isAffineHom` `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_of_max` `UnivLE.self` `eq_targetAffineLocally` `AlgebraicGeometry.targetAffineLocally_affineAnd_iff` `AlgebraicGeometry.IsAffineOpen.preimage` `AlgebraicGeometry.instIsAffineHomDescScheme` `CommRingCat.hasLimit` `small_subtype` `small_Pi` `CategoryTheory.Limits.colimit.ι_desc` `RingHom.RespectsIso.cancel_right_isIso` `CategoryTheory.Iso.isIso_hom` `CommRingCat.hom_comp` `LE.le.trans` `le_rfl` `AlgebraicGeometry.Scheme.Hom.app_eq_appLE` `CategoryTheory.eqToHom_op` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.prod.map_fst` `AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst_assoc` `AlgebraicGeometry.Scheme.Hom.appLE_map` `AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE` `AlgebraicGeometry.Scheme.Hom.appLE.congr_simp` `CategoryTheory.Limits.prod.map_snd` `AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd_assoc`

---

← Back to Index