Documentation Verification Report

Directed

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

Statistics

Metric	Count
Definitions `ofIsBasisOpensRange`, `trans`, `coconeOfLocallyDirected`, `functorOfLocallyDirected`, `functorOfLocallyDirectedHomBase`, `instCategoryI₀Pullback₁`, `intersectionOfLocallyDirected`, `locallyDirectedPullbackCover`, `trans`, `glueMorphismsOfLocallyDirected`, `glueMorphismsOverOfLocallyDirected`, `isColimitCoconeOfLocallyDirected`, `directedAffineCover`, `instLocallyDirectedIsOpenImmersionDirectedAffineCover`, `instPreorderI₀DirectedAffineCover`	15
Theorems `directed`, `ofIsBasisOpensRange_le_iff`, `ofIsBasisOpensRange_trans`, `property_trans`, `trans_comp`, `trans_id`, `w`, `coconeOfLocallyDirected_pt`, `coconeOfLocallyDirected_ι`, `exists_lift_trans_eq`, `exists_of_f_eq_f`, `exists_of_trans_eq_trans`, `functorOfLocallyDirectedHomBase_app`, `functorOfLocallyDirected_map`, `functorOfLocallyDirected_obj`, `instIsLocallyDirectedI₀CompFunctorOfLocallyDirectedForget`, `intersectionOfLocallyDirected_f`, `property_trans`, `trans_comp`, `trans_id`, `trans_map`, `instIsOpenImmersionMapI₀FunctorOfLocallyDirected`, `instIsOpenImmersionTrans`, `map_glueMorphismsOfLocallyDirected`, `map_glueMorphismsOfLocallyDirected_assoc`, `map_glueMorphismsOverOfLocallyDirected_left`, `map_glueMorphismsOverOfLocallyDirected_left_assoc`, `directedAffineCover_I₀`, `directedAffineCover_X`, `directedAffineCover_f`, `directedAffineCover_trans`	31
Total	46

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
`directedAffineCover` 📖	CompOp	4 math math: `directedAffineCover_f`, `directedAffineCover_I₀`, `directedAffineCover_X`, `directedAffineCover_trans`
`instLocallyDirectedIsOpenImmersionDirectedAffineCover` 📖	CompOp	1 math math: `directedAffineCover_trans`
`instPreorderI₀DirectedAffineCover` 📖	CompOp	1 math math: `directedAffineCover_trans`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`directedAffineCover_I₀` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `precoverage` `AlgebraicGeometry.IsOpenImmersion` `directedAffineCover` `Set.Elem` `Opens` `affineOpens`	—	—
`directedAffineCover_X` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `precoverage` `AlgebraicGeometry.IsOpenImmersion` `directedAffineCover` `Opens.toScheme` `Opens` `Set` `Set.instMembership` `affineOpens`	—	—
`directedAffineCover_f` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.f` `AlgebraicGeometry.Scheme` `instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `precoverage` `AlgebraicGeometry.IsOpenImmersion` `directedAffineCover` `Opens.ι` `Opens` `Set` `Set.instMembership` `affineOpens`	—	—
`directedAffineCover_trans` 📖	mathematical	`Set.Elem` `Opens` `affineOpens` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set` `Set.instMembership`	`Cover.trans` `AlgebraicGeometry.IsOpenImmersion` `directedAffineCover` `Preorder.smallCategory` `CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `precoverage` `instPreorderI₀DirectedAffineCover` `instLocallyDirectedIsOpenImmersionDirectedAffineCover` `CategoryTheory.homOfLE` `homOfLE`	—	—

AlgebraicGeometry.Scheme.Cover

Definitions

Name	Category	Theorems
`coconeOfLocallyDirected` 📖	CompOp	2 math math: `coconeOfLocallyDirected_ι`, `coconeOfLocallyDirected_pt`
`functorOfLocallyDirected` 📖	CompOp	12 math math: `functorOfLocallyDirected_obj`, `coconeOfLocallyDirected_ι`, `RelativeGluingData.ι_toBase`, `RelativeGluingData.ι_toBase_assoc`, `RelativeGluingData.equifibered`, `instIsLocallyDirectedI₀CompFunctorOfLocallyDirectedForget`, `functorOfLocallyDirected_map`, `coconeOfLocallyDirected_pt`, `AlgebraicGeometry.Scheme.OpenCover.instIsOpenImmersionMapI₀FunctorOfLocallyDirected`, `functorOfLocallyDirectedHomBase_app`, `ColimitGluingData.relativeGluingData_natTrans_app`, `RelativeGluingData.isPullback_natTrans_ι_toBase`
`functorOfLocallyDirectedHomBase` 📖	CompOp	2 math math: `coconeOfLocallyDirected_ι`, `functorOfLocallyDirectedHomBase_app`
`instCategoryI₀Pullback₁` 📖	CompOp	—
`intersectionOfLocallyDirected` 📖	CompOp	1 math math: `intersectionOfLocallyDirected_f`
`locallyDirectedPullbackCover` 📖	CompOp	—
`trans` 📖	CompOp	20 math math: `ColimitGluingData.cocone_ι_transitionMap`, `ColimitGluingData.transitionCocone_pt`, `ColimitGluingData.transitionMap_id`, `trans_id`, `exists_lift_trans_eq`, `exists_of_f_eq_f`, `LocallyDirected.ofIsBasisOpensRange_trans`, `ColimitGluingData.transitionCocone_ι_app`, `trans_map`, `functorOfLocallyDirected_map`, `property_trans`, `AlgebraicGeometry.Scheme.OpenCover.instIsOpenImmersionTrans`, `ColimitGluingData.cocone_ι_transitionMap_assoc`, `AlgebraicGeometry.Scheme.directedAffineCover_trans`, `ColimitGluingData.prop_trans`, `ColimitGluingData.trans_app_left`, `ColimitGluingData.transitionMap_comp`, `trans_comp`, `ColimitGluingData.functor_map`, `intersectionOfLocallyDirected_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coconeOfLocallyDirected_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `functorOfLocallyDirected` `coconeOfLocallyDirected`	—	—
`coconeOfLocallyDirected_ι` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.ι` `CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `functorOfLocallyDirected` `coconeOfLocallyDirected` `functorOfLocallyDirectedHomBase`	—	—
`exists_lift_trans_eq` 📖	mathematical	—	`DFunLike.coe` `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.Scheme.precoverage` `CategoryTheory.Limits.pullback` `CategoryTheory.PreZeroHypercover.f` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `TopCat.carrier` `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.Limits.pullback.lift` `trans`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `LocallyDirected.directed`
`exists_of_f_eq_f` 📖	mathematical	`DFunLike.coe` `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.Scheme.precoverage` `TopCat.carrier` `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`	`trans`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback` `exists_lift_trans_eq` `CategoryTheory.Limits.limit.lift_π`
`exists_of_trans_eq_trans` 📖	—	`DFunLike.coe` `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.Scheme.precoverage` `TopCat.carrier` `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'` `trans`	—	—	`trans_map` `AlgebraicGeometry.Scheme.Hom.comp_base` `CategoryTheory.ConcreteCategory.comp_apply` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback` `exists_lift_trans_eq` `CategoryTheory.Limits.limit.lift_π`
`functorOfLocallyDirectedHomBase_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `functorOfLocallyDirected` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `functorOfLocallyDirectedHomBase` `CategoryTheory.PreZeroHypercover.f`	—	—
`functorOfLocallyDirected_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `functorOfLocallyDirected` `trans`	—	—
`functorOfLocallyDirected_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `functorOfLocallyDirected` `CategoryTheory.PreZeroHypercover.X`	—	—
`instIsLocallyDirectedI₀CompFunctorOfLocallyDirectedForget` 📖	mathematical	—	`CategoryTheory.Functor.IsLocallyDirected` `CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `CategoryTheory.Functor.comp` `CategoryTheory.types` `functorOfLocallyDirected` `AlgebraicGeometry.Scheme.forget`	—	`trans_map` `AlgebraicGeometry.Scheme.Hom.comp_base` `CategoryTheory.ConcreteCategory.comp_apply` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback` `exists_lift_trans_eq` `CategoryTheory.Limits.limit.lift_π`
`intersectionOfLocallyDirected_f` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.f` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Limits.pullback` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `intersectionOfLocallyDirected` `CategoryTheory.Limits.pullback.lift` `CategoryTheory.PreZeroHypercover.I₀` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `trans`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback`
`property_trans` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `trans`	—	`LocallyDirected.property_trans`
`trans_comp` 📖	mathematical	—	`trans` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.PreZeroHypercover.X`	—	`LocallyDirected.trans_comp`
`trans_id` 📖	mathematical	—	`trans` `CategoryTheory.CategoryStruct.id` `CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.PreZeroHypercover.X`	—	`LocallyDirected.trans_id`
`trans_map` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `trans` `CategoryTheory.PreZeroHypercover.f`	—	`LocallyDirected.w`

AlgebraicGeometry.Scheme.Cover.LocallyDirected

Definitions

Name	Category	Theorems
`ofIsBasisOpensRange` 📖	CompOp	1 math math: `ofIsBasisOpensRange_trans`
`trans` 📖	CompOp	5 math math: `directed`, `trans_comp`, `trans_id`, `property_trans`, `w`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`directed` 📖	mathematical	—	`DFunLike.coe` `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.Scheme.precoverage` `CategoryTheory.Limits.pullback` `CategoryTheory.PreZeroHypercover.f` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `TopCat.carrier` `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.Limits.pullback.lift` `trans` `w`	—	—
`ofIsBasisOpensRange_le_iff` 📖	—	`CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.IsOpenImmersion` `Preorder.toLE` `AlgebraicGeometry.Scheme.Opens` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `AlgebraicGeometry.Scheme.Hom.opensRange` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.PreZeroHypercover.f` `AlgebraicGeometry.Scheme.instIsOpenImmersionF`	—	—	`AlgebraicGeometry.Scheme.instIsOpenImmersionF`
`ofIsBasisOpensRange_trans` 📖	mathematical	`CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.IsOpenImmersion` `Preorder.toLE` `AlgebraicGeometry.Scheme.Opens` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `AlgebraicGeometry.Scheme.Hom.opensRange` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.PreZeroHypercover.f` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `TopologicalSpace.Opens.IsBasis` `Set.range` `TopologicalSpace.Opens`	`AlgebraicGeometry.Scheme.Cover.trans` `Preorder.smallCategory` `ofIsBasisOpensRange` `CategoryTheory.homOfLE` `AlgebraicGeometry.IsOpenImmersion.lift`	—	`AlgebraicGeometry.Scheme.instIsOpenImmersionF`
`property_trans` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `trans`	—	—
`trans_comp` 📖	mathematical	—	`trans` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.PreZeroHypercover.X`	—	—
`trans_id` 📖	mathematical	—	`trans` `CategoryTheory.CategoryStruct.id` `CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.PreZeroHypercover.X`	—	—
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `trans` `CategoryTheory.PreZeroHypercover.f`	—	—

AlgebraicGeometry.Scheme.OpenCover

Definitions

Name	Category	Theorems
`glueMorphismsOfLocallyDirected` 📖	CompOp	2 math math: `map_glueMorphismsOfLocallyDirected_assoc`, `map_glueMorphismsOfLocallyDirected`
`glueMorphismsOverOfLocallyDirected` 📖	CompOp	2 math math: `map_glueMorphismsOverOfLocallyDirected_left_assoc`, `map_glueMorphismsOverOfLocallyDirected_left`
`isColimitCoconeOfLocallyDirected` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsOpenImmersionMapI₀FunctorOfLocallyDirected` 📖	mathematical	—	`AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected` `CategoryTheory.Functor.map`	—	`AlgebraicGeometry.Scheme.Cover.property_trans`
`instIsOpenImmersionTrans` 📖	mathematical	—	`AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.Scheme.Cover.trans`	—	`AlgebraicGeometry.Scheme.Cover.property_trans`
`map_glueMorphismsOfLocallyDirected` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.IsOpenImmersion` `AlgebraicGeometry.Scheme.Cover.trans`	`CategoryTheory.PreZeroHypercover.f` `glueMorphismsOfLocallyDirected`	—	`AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms`
`map_glueMorphismsOfLocallyDirected_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.IsOpenImmersion` `AlgebraicGeometry.Scheme.Cover.trans`	`CategoryTheory.PreZeroHypercover.f` `glueMorphismsOfLocallyDirected`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_glueMorphismsOfLocallyDirected`
`map_glueMorphismsOverOfLocallyDirected_left` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.IsOpenImmersion` `AlgebraicGeometry.Scheme.Cover.trans` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom` `CategoryTheory.PreZeroHypercover.f`	`CategoryTheory.CommaMorphism.left` `glueMorphismsOverOfLocallyDirected`	—	`map_glueMorphismsOfLocallyDirected`
`map_glueMorphismsOverOfLocallyDirected_left_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.IsOpenImmersion` `AlgebraicGeometry.Scheme.Cover.trans` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom` `CategoryTheory.PreZeroHypercover.f`	`CategoryTheory.CommaMorphism.left` `glueMorphismsOverOfLocallyDirected`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_glueMorphismsOverOfLocallyDirected_left`

---

← Back to Index