Documentation Verification Report

QuasiAffine

📁 Source: Mathlib/AlgebraicGeometry/QuasiAffine.lean

Statistics

Metric	Count
Definitions `IsQuasiAffine`, `openCoverBasicOpenTop`	2
Theorems `isBasis_basicOpen`, `of_forall_exists_mem_basicOpen`, `of_isAffineHom`, `of_isImmersion`, `toCompactSpace`, `toIsImmersion`, `instIsOpenImmersionToSpecΓOfIsQuasiAffine`, `instIsQuasiAffineOfIsAffine`, `instIsSeparatedOfIsQuasiAffine`, `isPullback_toSpecΓ_toSpecΓ`, `openCoverBasicOpenTop_f`, `preimage_opensRange_toSpecΓ`	12
Total	14

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
`IsQuasiAffine` 📖	CompData	5 math math: `IsQuasiAffine.of_isAffineHom`, `IsQuasiAffine.of_isImmersion`, `IsQuasiAffine.of_forall_exists_mem_basicOpen`, `exists_isQuasiAffine_of_isLimit`, `instIsQuasiAffineOfIsAffine`
`openCoverBasicOpenTop` 📖	CompOp	1 math math: `openCoverBasicOpenTop_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsOpenImmersionToSpecΓOfIsQuasiAffine` 📖	mathematical	—	`AlgebraicGeometry.IsOpenImmersion` `AlgebraicGeometry.Spec` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `Opens` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `toSpecΓ`	—	`ker_toSpecΓ` `IsQuasiAffine.toCompactSpace` `instIsIsoSubschemeιBotIdealSheafData` `Hom.toImage_imageι` `AlgebraicGeometry.IsOpenImmersion.comp` `AlgebraicGeometry.IsImmersion.instIsOpenImmersionToImageOfQuasiCompact` `IsQuasiAffine.toIsImmersion` `AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat` `AlgebraicGeometry.IsOpenImmersion.of_isIso`
`instIsQuasiAffineOfIsAffine` 📖	mathematical	—	`IsQuasiAffine`	—	`compactSpace_of_isAffine` `AlgebraicGeometry.IsImmersion.instOfIsClosedImmersion` `AlgebraicGeometry.IsClosedImmersion.instOfIsIsoScheme` `AlgebraicGeometry.IsAffine.affine`
`instIsSeparatedOfIsQuasiAffine` 📖	mathematical	—	`IsSeparated`	—	`AlgebraicGeometry.instHasTerminalScheme` `CategoryTheory.Limits.terminal.comp_from` `AlgebraicGeometry.IsSeparated.instCompScheme` `AlgebraicGeometry.IsSeparated.isSeparated_of_mono` `AlgebraicGeometry.IsPreimmersion.instMonoScheme` `AlgebraicGeometry.IsImmersion.toIsPreimmersion` `IsQuasiAffine.toIsImmersion` `IsSeparated.isSeparated_terminal_from` `instIsSeparatedOfIsAffine` `AlgebraicGeometry.isAffine_Spec`
`isPullback_toSpecΓ_toSpecΓ` 📖	mathematical	—	`CategoryTheory.IsPullback` `AlgebraicGeometry.Scheme` `instCategory` `AlgebraicGeometry.Spec` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `Opens` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `toSpecΓ` `AlgebraicGeometry.Spec.map` `Hom.appTop`	—	`AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace` `AlgebraicGeometry.instQuasiCompactOfIsAffineHom` `IsQuasiAffine.toCompactSpace` `IsQuasiAffine.of_isAffineHom` `le_top` `Eq.ge` `preimage_basicOpen_top` `AlgebraicGeometry.isLocalization_basicOpen_of_qcqs` `isCompact_univ` `isQuasiSeparated_univ` `instQuasiSeparatedSpaceCarrierCarrierCommRingCatOfIsSeparated` `instIsSeparatedOfIsQuasiAffine` `CommRingCat.isPushout_of_isLocalization` `basicOpen_le` `LE.le.trans` `Hom.map_appLE` `Hom.appLE.eq_1` `IsLocalization.Away.instMapRingHomPowersOfCoe` `isPullback_of_openCover` `Pullback.instHasPullback` `AlgebraicGeometry.IsAffineOpen.preimage` `CategoryTheory.IsPullback.of_iso` `CategoryTheory.IsPullback.map` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint` `CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint` `CategoryTheory.IsPushout.op` `instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Spec.map_comp` `CategoryTheory.Category.assoc` `Opens.toSpecΓ_SpecMap_presheaf_map_assoc` `Opens.toSpecΓ_naturality` `CategoryTheory.cancel_mono` `AlgebraicGeometry.IsOpenImmersion.mono` `Opens.instIsOpenImmersionι` `AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right` `AlgebraicGeometry.morphismRestrict_ι` `homOfLE_ι_assoc` `isoOfEq_hom_ι_assoc` `AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc` `CategoryTheory.Limits.pullback.condition` `CategoryTheory.Category.comp_id` `Opens.toSpecΓ_SpecMap_presheaf_map` `Opens.toSpecΓ_top` `AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc` `AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ` `CategoryTheory.Category.id_comp`
`openCoverBasicOpenTop_f` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.f` `AlgebraicGeometry.Scheme` `instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `precoverage` `AlgebraicGeometry.IsOpenImmersion` `openCoverBasicOpenTop` `Opens.ι` `basicOpen` `Top.top` `Opens` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `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` `AlgebraicGeometry.IsAffineOpen`	—	—
`preimage_opensRange_toSpecΓ` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opens` `AlgebraicGeometry.Spec` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `Hom.toLRSHom'` `AlgebraicGeometry.Spec.map` `Hom.appTop` `Hom.opensRange` `toSpecΓ` `instIsOpenImmersionToSpecΓOfIsQuasiAffine`	—	`instIsOpenImmersionToSpecΓOfIsQuasiAffine` `Hom.image_top_eq_opensRange` `AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback` `isPullback_toSpecΓ_toSpecΓ`

AlgebraicGeometry.Scheme.IsQuasiAffine

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBasis_basicOpen` 📖	mathematical	—	`TopologicalSpace.Opens.IsBasis` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `setOf` `TopologicalSpace.Opens` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `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` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `AlgebraicGeometry.IsAffineOpen` `AlgebraicGeometry.Scheme.basicOpen`	—	`TopologicalSpace.Opens.isBasis_iff_nbhd` `TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open` `PrimeSpectrum.isBasis_basic_opens` `Set.mem_image_of_mem` `TopologicalSpace.Opens.is_open'` `AlgebraicGeometry.Scheme.instIsOpenImmersionToSpecΓOfIsQuasiAffine` `AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion` `SetLike.coe_injective` `Set.image_preimage_eq_of_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.image_subset_range` `AlgebraicGeometry.IsAffineOpen.Spec_basicOpen` `LE.le.trans_eq` `Set.preimage_mono` `Set.preimage_image_eq` `Topology.IsEmbedding.injective` `AlgebraicGeometry.Scheme.Hom.isEmbedding` `AlgebraicGeometry.IsImmersion.toIsPreimmersion` `toIsImmersion`
`of_forall_exists_mem_basicOpen` 📖	mathematical	`AlgebraicGeometry.IsAffineOpen` `AlgebraicGeometry.Scheme.basicOpen` `Top.top` `AlgebraicGeometry.Scheme.Opens` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`AlgebraicGeometry.Scheme.IsQuasiAffine`	—	`QuasiSeparatedSpace.of_isOpenCover` `eq_top_iff` `TopologicalSpace.Opens.mem_iSup` `AlgebraicGeometry.isRetrocompact_basicOpen` `AlgebraicGeometry.IsAffineOpen.isQuasiSeparated` `AlgebraicGeometry.IsZariskiLocalAtTarget.of_forall_source_exists_preimage` `AlgebraicGeometry.isOpenImmersion_isZariskiLocalAtTarget` `CategoryTheory.MorphismProperty.Respects.toRespectsRight` `CategoryTheory.MorphismProperty.instRespectsOfIsStableUnderComposition` `AlgebraicGeometry.isOpenImmersion_isStableUnderComposition` `AlgebraicGeometry.IsOpenImmersion.instHasOfPostcompPropertyScheme` `Eq.ge` `AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen` `le_top` `AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top` `AlgebraicGeometry.isLocalization_basicOpen_of_qcqs` `isCompact_univ` `isQuasiSeparated_univ` `CategoryTheory.MorphismProperty.comp_mem` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Iso.isIso_hom` `AlgebraicGeometry.IsOpenImmersion.of_isLocalization` `AlgebraicGeometry.IsImmersion.instOfIsOpenImmersion`
`of_isAffineHom` 📖	mathematical	—	`AlgebraicGeometry.Scheme.IsQuasiAffine`	—	`AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace` `AlgebraicGeometry.instQuasiCompactOfIsAffineHom` `toCompactSpace` `of_forall_exists_mem_basicOpen` `TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open` `isBasis_basicOpen` `Set.mem_univ` `isOpen_univ` `AlgebraicGeometry.Scheme.preimage_basicOpen_top` `AlgebraicGeometry.IsAffineOpen.preimage`
`of_isImmersion` 📖	mathematical	—	`AlgebraicGeometry.Scheme.IsQuasiAffine`	—	`AlgebraicGeometry.Scheme.toSpecΓ_naturality` `AlgebraicGeometry.IsImmersion.comp` `toIsImmersion` `AlgebraicGeometry.IsImmersion.of_comp`
`toCompactSpace` 📖	mathematical	—	`CompactSpace` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	—
`toIsImmersion` 📖	mathematical	—	`AlgebraicGeometry.IsImmersion` `AlgebraicGeometry.Spec` `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` `AlgebraicGeometry.Scheme.toSpecΓ`	—	—

---

← Back to Index