Documentation Verification Report

QuasiCompact

📁 Source: Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean

Statistics

Metric	Count
Definitions `QuasiCompactCover`, `ulift`, `uliftHom`, `quasiCompactCover`	4
Theorems `isCompactOpenCovered`, `exists_hom`, `exists_isAffineOpen_of_isCompact`, `homCover`, `inst`, `instBindScheme`, `instCoverOfIsIso`, `instPullback₁Scheme`, `instPullback₂Scheme`, `instSumScheme`, `instSumScheme_1`, `instUlift`, `isCompactOpenCovered_of_isAffineOpen`, `isCompactOpenCovered_of_isCompact`, `of_finite`, `of_hom`, `of_isOpenMap`, `singleton`, `isClosedUnderIsomorphisms_quasiCompactCover`, `quasiCompactCover_iff`, `quasiCompactCover_iff`	21
Total	25

AlgebraicGeometry

Definitions

Name	Category	Theorems
`QuasiCompactCover` 📖	CompData	16 math math: `QuasiCompactCover.of_finite`, `QuasiCompactCover.instCoverOfIsIso`, `Scheme.quasiCompactCover_shrink_iff`, `QuasiCompactCover.of_hom`, `QuasiCompactCover.of_isOpenMap`, `QuasiCompactCover.instUlift`, `QuasiCompactCover.inst`, `QuasiCompactCover.instPullback₁Scheme`, `Scheme.presieve₀_mem_qcPrecoverage_iff`, `Scheme.quasiCompactCover_iff`, `QuasiCompactCover.instSumScheme_1`, `QuasiCompactCover.singleton`, `QuasiCompactCover.homCover`, `quasiCompactCover_iff`, `QuasiCompactCover.instPullback₂Scheme`, `QuasiCompactCover.instSumScheme`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasiCompactCover_iff` 📖	mathematical	—	`QuasiCompactCover` `IsCompactOpenCovered` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `CategoryTheory.PreZeroHypercover.I₀` `Scheme` `Scheme.instCategory` `CategoryTheory.PreZeroHypercover.X` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `CategoryTheory.PreZeroHypercover.f` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `Scheme.Opens` `TopologicalSpace.Opens.instSetLike`	—	—

AlgebraicGeometry.IsAffineOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCompactOpenCovered` 📖	mathematical	—	`IsCompactOpenCovered` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.PreZeroHypercover.X` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `CategoryTheory.PreZeroHypercover.f` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `AlgebraicGeometry.Scheme.Opens` `TopologicalSpace.Opens.instSetLike`	—	`AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen`

AlgebraicGeometry.QuasiCompactCover

Definitions

Name	Category	Theorems
`ulift` 📖	CompOp	1 math math: `instUlift`
`uliftHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_hom` 📖	mathematical	—	`Finite` `AlgebraicGeometry.Scheme.AffineCover.I₀` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.Scheme.AffineCover.cover` `CategoryTheory.PreZeroHypercover.Hom.s₀` `CategoryTheory.PreZeroHypercover.Hom.h₀`	—	`exists_isAffineOpen_of_isCompact` `isCompact_univ` `AlgebraicGeometry.Scheme.Hom.comp_apply` `AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id_assoc` `CategoryTheory.MorphismProperty.RespectsLeft.precomp` `AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec` `AlgebraicGeometry.Scheme.Cover.map_prop` `instFiniteULift` `Finite.of_fintype` `Set.image_congr`
`exists_isAffineOpen_of_isCompact` 📖	mathematical	`IsCompact` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `AlgebraicGeometry.Scheme.Opens` `TopologicalSpace.Opens.instSetLike`	`AlgebraicGeometry.IsAffineOpen` `CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `Set.iUnion` `Set.image` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `CategoryTheory.PreZeroHypercover.f`	—	`IsCompactOpenCovered.exists_mem_of_isBasis` `AlgebraicGeometry.Scheme.isBasis_affineOpens` `AlgebraicGeometry.IsAffineOpen.isCompact` `isCompactOpenCovered_of_isCompact`
`homCover` 📖	mathematical	—	`AlgebraicGeometry.QuasiCompactCover` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.Scheme.Hom.cover`	—	`of_finite` `AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage` `Finite.of_fintype`
`inst` 📖	mathematical	—	`AlgebraicGeometry.QuasiCompactCover` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.IsOpenImmersion`	—	`of_isOpenMap` `AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage` `Topology.IsOpenEmbedding.isOpenMap` `AlgebraicGeometry.Scheme.Hom.isOpenEmbedding` `AlgebraicGeometry.Scheme.instIsOpenImmersionF`
`instBindScheme` 📖	mathematical	`AlgebraicGeometry.QuasiCompactCover` `CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	`CategoryTheory.PreZeroHypercover.bind`	—	`AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered` `isCompactOpenCovered_of_isCompact` `IsCompactOpenCovered.of_finite` `Finite.instSigma` `Set.image_congr` `Set.iUnion_sigma` `Set.iUnion_subtype` `Set.iUnion_congr_Prop` `Set.image_iUnion` `Set.image_image`
`instCoverOfIsIso` 📖	mathematical	—	`AlgebraicGeometry.QuasiCompactCover` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.Scheme.coverOfIsIso`	—	`of_isOpenMap` `AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage` `Homeomorph.isOpenMap`
`instPullback₁Scheme` 📖	mathematical	—	`AlgebraicGeometry.QuasiCompactCover` `CategoryTheory.PreZeroHypercover.pullback₁` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.PreZeroHypercover.f`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered` `AlgebraicGeometry.IsAffineOpen.isCompact_pullback_inf` `Set.image_congr` `instIsConcreteLE` `Set.iUnion_congr_Prop` `Set.preimage_iUnion` `Set.subset_iUnion_of_subset` `Set.subset_preimage_image` `subset_antisymm` `Set.instAntisymmSubset` `AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback` `IsCompactOpenCovered.of_isCompact_of_forall_exists_isCompactOpenCovered` `AlgebraicGeometry.IsAffineOpen.isCompact` `TopologicalSpace.Opens.isBasis_iff_nbhd` `AlgebraicGeometry.Scheme.isBasis_affineOpens` `TopologicalSpace.Opens.mem_top` `le_trans` `inf_le_right` `TopologicalSpace.Opens.is_open'` `inf_le_left`
`instPullback₂Scheme` 📖	mathematical	—	`AlgebraicGeometry.QuasiCompactCover` `CategoryTheory.PreZeroHypercover.pullback₂` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.PreZeroHypercover.f`	—	`of_hom` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `instPullback₁Scheme`
`instSumScheme` 📖	mathematical	—	`AlgebraicGeometry.QuasiCompactCover` `CategoryTheory.PreZeroHypercover.sum` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	—	`of_hom`
`instSumScheme_1` 📖	mathematical	—	`AlgebraicGeometry.QuasiCompactCover` `CategoryTheory.PreZeroHypercover.sum` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	—	`of_hom`
`instUlift` 📖	mathematical	—	`AlgebraicGeometry.QuasiCompactCover` `ulift`	—	`exists_isAffineOpen_of_isCompact` `AlgebraicGeometry.IsAffineOpen.isCompact` `IsCompactOpenCovered.of_finite` `Finite.of_fintype`
`isCompactOpenCovered_of_isAffineOpen` 📖	mathematical	—	`IsCompactOpenCovered` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.PreZeroHypercover.X` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `CategoryTheory.PreZeroHypercover.f` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `AlgebraicGeometry.Scheme.Opens` `TopologicalSpace.Opens.instSetLike`	—	—
`isCompactOpenCovered_of_isCompact` 📖	mathematical	`IsCompact` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `AlgebraicGeometry.Scheme.Opens` `TopologicalSpace.Opens.instSetLike`	`IsCompactOpenCovered` `CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.PreZeroHypercover.X` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `CategoryTheory.PreZeroHypercover.f`	—	`TopologicalSpace.Opens.IsBasis.exists_finite_of_isCompact` `AlgebraicGeometry.Scheme.isBasis_affineOpens` `IsCompactOpenCovered.of_biUnion_eq_of_finite` `Set.iUnion_congr_Prop` `Set.iUnion_exists` `Set.biUnion_and'` `Set.iUnion_iUnion_eq_right` `Set.Finite.image` `AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered`
`of_finite` 📖	mathematical	`AlgebraicGeometry.QuasiCompact` `CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `CategoryTheory.PreZeroHypercover.f`	`AlgebraicGeometry.QuasiCompactCover`	—	`IsCompactOpenCovered.of_finite_of_isSpectralMap` `AlgebraicGeometry.Scheme.Hom.isSpectralMap` `AlgebraicGeometry.Scheme.Cover.covers` `TopologicalSpace.Opens.is_open'` `AlgebraicGeometry.IsAffineOpen.isCompact`
`of_hom` 📖	mathematical	—	`AlgebraicGeometry.QuasiCompactCover`	—	`IsCompactOpenCovered.of_comp` `AlgebraicGeometry.instPrespectralSpaceCarrierCarrierCommRingCat` `AlgebraicGeometry.Scheme.Hom.continuous` `CategoryTheory.PreZeroHypercover.Hom.w₀` `TopologicalSpace.Opens.is_open'` `AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered`
`of_isOpenMap` 📖	mathematical	`IsOpenMap` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `CategoryTheory.PreZeroHypercover.f`	`AlgebraicGeometry.QuasiCompactCover`	—	`IsCompactOpenCovered.of_isOpenMap` `AlgebraicGeometry.instPrespectralSpaceCarrierCarrierCommRingCat` `AlgebraicGeometry.Scheme.Hom.continuous` `AlgebraicGeometry.Scheme.Cover.covers` `TopologicalSpace.Opens.is_open'` `AlgebraicGeometry.IsAffineOpen.isCompact`
`singleton` 📖	mathematical	—	`AlgebraicGeometry.QuasiCompactCover` `CategoryTheory.PreZeroHypercover.singleton` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	—	`homCover`

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
`quasiCompactCover` 📖	CompOp	3 math math: `isClosedUnderIsomorphisms_quasiCompactCover`, `quasiCompactCover_iff`, `qcCoverFamily_property`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosedUnderIsomorphisms_quasiCompactCover` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms` `CategoryTheory.PreZeroHypercover` `AlgebraicGeometry.Scheme` `instCategory` `CategoryTheory.PreZeroHypercover.instCategory` `quasiCompactCover`	—	`AlgebraicGeometry.QuasiCompactCover.of_hom`
`quasiCompactCover_iff` 📖	mathematical	—	`quasiCompactCover` `AlgebraicGeometry.QuasiCompactCover`	—	—

---

← Back to Index