MorphismProperty

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

Statistics

Metric	Count
Definitions AffineCover, I₀, J, X, cover, f, idx, map, obj, app, comp, id, idx, add, changeProp, copy, idx, mkOfCovers, pullbackCover, pullbackCover', pullbackHom, pushforwardIso, ulift, coverOfIsIso	24
Theorems cover_I₀, cover_X, cover_f, covers, map_prop, w, add_toPreZeroHypercover, comp_app, comp_idx_apply, copy_I₀, copy_X, copy_f, covers, exists_eq, iUnion_range, id_app, id_idx_apply, map_prop, mkOfCovers_I₀, mkOfCovers_X, mkOfCovers_f, nonempty_of_nonempty, pullbackHom_map, pullbackHom_map_assoc, pushforwardIso_I₀, pushforwardIso_X, pushforwardIso_f, ulift_I₀, ulift_X, ulift_f, exists_eq, coverOfIsIso_I₀, coverOfIsIso_X, coverOfIsIso_f, instJointlySurjectivePrecoverage, instSmallPrecoverage, presieve₀_mem_precoverage_iff	37
Total	61

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
AffineCover 📖	CompData	—
coverOfIsIso 📖	CompOp	5 math math: coverOfIsIso_I₀, AlgebraicGeometry.QuasiCompactCover.instCoverOfIsIso, coverOfIsIso_X, AlgebraicGeometry.instIsAffineXSchemeCoverOfIsIsoIsOpenImmersionId, coverOfIsIso_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coverOfIsIso_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage coverOfIsIso	—	—
coverOfIsIso_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage coverOfIsIso	—	—
coverOfIsIso_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage coverOfIsIso	—	—
instJointlySurjectivePrecoverage 📖	mathematical	—	JointlySurjective precoverage	—	CategoryTheory.Presieve.mem_comap_jointlySurjectivePrecoverage_iff jointlySurjectivePrecoverage.eq_1
instSmallPrecoverage 📖	mathematical	—	CategoryTheory.Precoverage.Small AlgebraicGeometry.Scheme instCategory precoverage	—	instJointlySurjectivePrecoverage CategoryTheory.Precoverage.ZeroHypercover.mem₀
presieve₀_mem_precoverage_iff 📖	mathematical	—	CategoryTheory.Presieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership CategoryTheory.Precoverage.coverings precoverage CategoryTheory.PreZeroHypercover.presieve₀ TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Set.range 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 Hom.toLRSHom' CategoryTheory.PreZeroHypercover.f	—	—

AlgebraicGeometry.Scheme.AffineCover

Definitions

Name	Category	Theorems
I₀ 📖	CompOp	5 math math: cover_I₀, AlgebraicGeometry.Scheme.affineOpenCover_I₀, AlgebraicGeometry.QuasiCompactCover.exists_hom, AlgebraicGeometry.Scheme.AffineOpenCover.openCover_I₀, AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_I₀
J 📖	CompOp	—
X 📖	CompOp	11 math math: map_prop, AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover_map_subschemeι, AlgebraicGeometry.Scheme.AffineOpenCover.instIsOpenImmersionF, AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_X_carrier, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map, covers, cover_X, AlgebraicGeometry.Scheme.IdealSheafData.subSchemeCover_map_inclusion_assoc, AlgebraicGeometry.Scheme.IdealSheafData.subSchemeCover_map_inclusion, AlgebraicGeometry.Scheme.affineOpenCover_X, AlgebraicGeometry.Scheme.AffineOpenCover.openCover_X
cover 📖	CompOp	4 math math: cover_I₀, AlgebraicGeometry.QuasiCompactCover.exists_hom, cover_f, cover_X
f 📖	CompOp	11 math math: AlgebraicGeometry.Scheme.AffineOpenCover.openCover_f, map_prop, AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover_map_subschemeι, AlgebraicGeometry.Scheme.AffineOpenCover.instIsOpenImmersionF, cover_f, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map, covers, AlgebraicGeometry.Scheme.IdealSheafData.subSchemeCover_map_inclusion_assoc, AlgebraicGeometry.Scheme.IdealSheafData.subSchemeCover_map_inclusion, AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_f, AlgebraicGeometry.Scheme.affineOpenCover_f
idx 📖	CompOp	3 math math: AlgebraicGeometry.Scheme.affineOpenCover_idx, covers, AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_idx
map 📖	CompOp	—
obj 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cover_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage cover I₀	—	—
cover_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage cover AlgebraicGeometry.Spec X	—	—
cover_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage cover f	—	—
covers 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set Set.instMembership Set.range AlgebraicGeometry.Spec X idx 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' f	—	—
map_prop 📖	mathematical	—	AlgebraicGeometry.Spec X f	—	—

AlgebraicGeometry.Scheme.Cover

Definitions

Name	Category	Theorems
add 📖	CompOp	1 math math: add_toPreZeroHypercover
changeProp 📖	CompOp	—
copy 📖	CompOp	3 math math: copy_f, copy_X, copy_I₀
idx 📖	CompOp	5 math math: AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f, ulift_X, covers, ulift_f, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X
mkOfCovers 📖	CompOp	3 math math: mkOfCovers_I₀, mkOfCovers_X, mkOfCovers_f
pullbackCover 📖	CompOp	—
pullbackCover' 📖	CompOp	—
pullbackHom 📖	CompOp	10 math math: AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom, AlgebraicGeometry.HasAffineProperty.iff_of_openCover, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc, AlgebraicGeometry.IsLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map_assoc, pullbackHom_map_assoc, pullbackHom_map, AlgebraicGeometry.Scheme.Pullback.diagonalCover_map
pushforwardIso 📖	CompOp	3 math math: pushforwardIso_f, pushforwardIso_I₀, pushforwardIso_X
ulift 📖	CompOp	3 math math: ulift_X, ulift_f, ulift_I₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_toPreZeroHypercover 📖	mathematical	—	CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.precoverage add CategoryTheory.PreZeroHypercover.add	—	—
comp_app 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.h₀ CategoryTheory.CategoryStruct.comp CategoryTheory.PreZeroHypercover CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.Hom.s₀	—	CategoryTheory.PreZeroHypercover.comp_h₀
comp_idx_apply 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.CategoryStruct.comp CategoryTheory.PreZeroHypercover CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.instCategory	—	CategoryTheory.PreZeroHypercover.comp_s₀
copy_I₀ 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage DFunLike.coe Equiv CategoryTheory.PreZeroHypercover.I₀ EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Iso.hom CategoryTheory.PreZeroHypercover.f	copy	—	—
copy_X 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage DFunLike.coe Equiv CategoryTheory.PreZeroHypercover.I₀ EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Iso.hom CategoryTheory.PreZeroHypercover.f	copy	—	—
copy_f 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage DFunLike.coe Equiv CategoryTheory.PreZeroHypercover.I₀ EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Iso.hom CategoryTheory.PreZeroHypercover.f	copy	—	—
covers 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set Set.instMembership Set.range CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover idx 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	—	exists_eq
exists_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 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	—	AlgebraicGeometry.Scheme.JointlySurjective.exists_eq CategoryTheory.Precoverage.ZeroHypercover.mem₀
iUnion_range 📖	mathematical	—	Set.iUnion 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.Precoverage.ZeroHypercover.toPreZeroHypercover Set.range 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 Set.univ	—	Set.eq_univ_iff_forall Set.mem_iUnion exists_eq
id_app 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.h₀ CategoryTheory.CategoryStruct.id CategoryTheory.PreZeroHypercover CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.instCategory CategoryTheory.PreZeroHypercover.X	—	CategoryTheory.PreZeroHypercover.id_h₀
id_idx_apply 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.CategoryStruct.id CategoryTheory.PreZeroHypercover CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.instCategory	—	CategoryTheory.PreZeroHypercover.id_s₀
map_prop 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.Precoverage.ZeroHypercover.mem₀
mkOfCovers_I₀ 📖	mathematical	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace 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.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage mkOfCovers	—	—
mkOfCovers_X 📖	mathematical	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace 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.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage mkOfCovers	—	—
mkOfCovers_f 📖	mathematical	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace 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 AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage mkOfCovers	—	—
nonempty_of_nonempty 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover	—	exists_eq
pullbackHom_map 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage CategoryTheory.PreZeroHypercover.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Precoverage.ZeroHypercover.pullback₁ AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange pullbackHom	—	CategoryTheory.Limits.pullback.condition
pullbackHom_map_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage CategoryTheory.PreZeroHypercover.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Precoverage.ZeroHypercover.pullback₁ AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange pullbackHom	—	AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackHom_map
pushforwardIso_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage pushforwardIso	—	—
pushforwardIso_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage pushforwardIso	—	—
pushforwardIso_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage pushforwardIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X	—	AlgebraicGeometry.Scheme.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition
ulift_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage ulift TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace	—	—
ulift_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage ulift idx AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage	—	—
ulift_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage ulift idx AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage	—	AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage

AlgebraicGeometry.Scheme.Cover.Hom

Definitions

Name	Category	Theorems
app 📖	CompOp	—
comp 📖	CompOp	—
id 📖	CompOp	—
idx 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
w 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreZeroHypercover.Hom.h₀ CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.PreZeroHypercover.Hom.w₀

AlgebraicGeometry.Scheme.JointlySurjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_eq 📖	mathematical	CategoryTheory.Presieve AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Set Set.instMembership CategoryTheory.Precoverage.coverings	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.range 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'	—	—

---

← Back to Index