Documentation Verification Report

LocalClosure

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

Statistics

Metric	Count
Definitions `sourceLocalClosure`, `cover`	2
Theorems `iff_forall_exists`, `instContainsIdentitiesScheme`, `instIsMultiplicativeSchemeOfIsStableUnderBaseChange`, `instIsStableUnderBaseChangeScheme`, `instIsStableUnderCompositionSchemeOfIsStableUnderBaseChange`, `instIsZariskiLocalAtSourceIsOpenImmersionOfRespectsIsoOfRespectsLeftScheme`, `instRespectsIsoScheme`, `instRespectsLeftSchemeOfIsStableUnderBaseChange`, `instRespectsRightScheme`, `le`, `property_coverMap_comp`	11
Total	13

AlgebraicGeometry

Definitions

Name	Category	Theorems
`sourceLocalClosure` 📖	CompOp	11 math math: `sourceLocalClosure.instIsMultiplicativeSchemeOfIsStableUnderBaseChange`, `sourceLocalClosure.iff_forall_exists`, `sourceLocalClosure.instIsZariskiLocalAtSourceIsOpenImmersionOfRespectsIsoOfRespectsLeftScheme`, `sourceLocalClosure.instRespectsIsoScheme`, `sourceLocalClosure.instIsStableUnderCompositionSchemeOfIsStableUnderBaseChange`, `sourceLocalClosure.instContainsIdentitiesScheme`, `sourceLocalClosure.instRespectsLeftSchemeOfIsStableUnderBaseChange`, `sourceLocalClosure.instIsStableUnderBaseChangeScheme`, `IsLocalIso.eq_sourceLocalClosure_isOpenImmersion`, `sourceLocalClosure.instRespectsRightScheme`, `sourceLocalClosure.le`

AlgebraicGeometry.sourceLocalClosure

Definitions

Name	Category	Theorems
`cover` 📖	CompOp	1 math math: `property_coverMap_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_forall_exists` 📖	mathematical	—	`AlgebraicGeometry.sourceLocalClosure` `AlgebraicGeometry.IsOpenImmersion` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Scheme.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `AlgebraicGeometry.Scheme.Opens.toScheme` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Opens.ι`	—	`AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `AlgebraicGeometry.Scheme.Cover.covers` `AlgebraicGeometry.Scheme.Hom.isoOpensRange_inv_comp` `CategoryTheory.Category.assoc` `CategoryTheory.MorphismProperty.cancel_left_of_respectsIso` `CategoryTheory.Iso.isIso_inv` `AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι`
`instContainsIdentitiesScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.ContainsIdentities` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.sourceLocalClosure`	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange.respectsIso` `CategoryTheory.IsIso.id` `CategoryTheory.MorphismProperty.id_mem`
`instIsMultiplicativeSchemeOfIsStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.sourceLocalClosure`	—	`instContainsIdentitiesScheme` `CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities` `instIsStableUnderCompositionSchemeOfIsStableUnderBaseChange` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition`
`instIsStableUnderBaseChangeScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.sourceLocalClosure`	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk'` `instRespectsIsoScheme` `CategoryTheory.MorphismProperty.instRespectsOfRespectsLeftOfRespectsRight` `CategoryTheory.MorphismProperty.Respects.toRespectsLeft` `CategoryTheory.MorphismProperty.IsStableUnderBaseChange.respectsIso` `CategoryTheory.MorphismProperty.Respects.toRespectsRight` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.hasPullbackVertPaste` `CategoryTheory.MorphismProperty.cancel_left_of_respectsIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.MorphismProperty.pullback_fst` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange`
`instIsStableUnderCompositionSchemeOfIsStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.sourceLocalClosure`	—	`AlgebraicGeometry.Scheme.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.hasPullbackHorizPaste` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.pullback.condition_assoc` `CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd_assoc` `CategoryTheory.MorphismProperty.comp_mem` `CategoryTheory.MorphismProperty.pullback_snd` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange`
`instIsZariskiLocalAtSourceIsOpenImmersionOfRespectsIsoOfRespectsLeftScheme` 📖	mathematical	—	`AlgebraicGeometry.IsZariskiLocalAtSource` `AlgebraicGeometry.sourceLocalClosure` `AlgebraicGeometry.IsOpenImmersion`	—	`CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_iff` `instRespectsIsoScheme` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.condition_assoc` `CategoryTheory.MorphismProperty.RespectsLeft.precomp` `AlgebraicGeometry.IsOpenImmersion.instSndScheme` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `AlgebraicGeometry.Scheme.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition` `AlgebraicGeometry.isOpenImmersion_isStableUnderComposition`
`instRespectsIsoScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.sourceLocalClosure`	—	`instRespectsLeftSchemeOfIsStableUnderBaseChange` `CategoryTheory.MorphismProperty.Respects.toRespectsLeft` `CategoryTheory.MorphismProperty.IsStableUnderBaseChange.isomorphisms` `instRespectsRightScheme` `CategoryTheory.MorphismProperty.Respects.toRespectsRight`
`instRespectsLeftSchemeOfIsStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsLeft` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.sourceLocalClosure`	—	`AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.condition_assoc` `CategoryTheory.MorphismProperty.RespectsLeft.precomp` `CategoryTheory.MorphismProperty.pullback_snd` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange`
`instRespectsRightScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsRight` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.sourceLocalClosure`	—	`CategoryTheory.Category.assoc` `CategoryTheory.MorphismProperty.RespectsRight.postcomp`
`le` 📖	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.sourceLocalClosure`	—	`CategoryTheory.IsIso.id` `CategoryTheory.Category.id_comp`
`property_coverMap_comp` 📖	mathematical	`AlgebraicGeometry.sourceLocalClosure`	`CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `cover` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.PreZeroHypercover.f`	—	—

---

← Back to Index