ColimitsOver

📁 Source: Mathlib/AlgebraicGeometry/ColimitsOver.lean

Statistics

Metric	Count
Definitions ColimitGluingData, cocone, functor, glued, gluedCocone, isColimit, isColimitGluedCocone, pullbackGluedIso, relativeGluingData, trans, transitionCocone, transitionMap	12
Theorems cocone_ι_transitionMap, cocone_ι_transitionMap_assoc, fst_gluedCocone_ι, fst_gluedCocone_ι_assoc, functor_map, functor_obj, gluedCocone_pt, isPullback, prop_trans, pullbackGluedIso_inv_fst, pullbackGluedIso_inv_fst_assoc, pullbackGluedIso_inv_snd, pullbackGluedIso_inv_snd_assoc, relativeGluingData_functor, relativeGluingData_natTrans_app, trans_app_left, transitionCocone_pt, transitionCocone_ι_app, transitionMap_comp, transitionMap_id, hasColimit_of_locallyDirected	21
Total	33

AlgebraicGeometry.Scheme.Cover

Definitions

Name	Category	Theorems
ColimitGluingData 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasColimit_of_locallyDirected 📖	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion trans CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.MorphismProperty.Over Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Over.pullback CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.Limits.HasColimit CategoryTheory.Functor.comp CategoryTheory.PreZeroHypercover.f Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.CategoryStruct.toQuiver	—	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop

AlgebraicGeometry.Scheme.Cover.ColimitGluingData

Definitions

Name	Category	Theorems
cocone 📖	CompOp	16 math math: pullbackGluedIso_inv_snd_assoc, isPullback, cocone_ι_transitionMap, pullbackGluedIso_inv_fst_assoc, transitionCocone_pt, transitionMap_id, fst_gluedCocone_ι, transitionCocone_ι_app, fst_gluedCocone_ι_assoc, cocone_ι_transitionMap_assoc, transitionMap_comp, functor_map, pullbackGluedIso_inv_snd, pullbackGluedIso_inv_fst, functor_obj, relativeGluingData_natTrans_app
functor 📖	CompOp	4 math math: relativeGluingData_functor, functor_map, functor_obj, relativeGluingData_natTrans_app
glued 📖	CompOp	5 math math: pullbackGluedIso_inv_snd_assoc, pullbackGluedIso_inv_fst_assoc, gluedCocone_pt, pullbackGluedIso_inv_snd, pullbackGluedIso_inv_fst
gluedCocone 📖	CompOp	3 math math: fst_gluedCocone_ι, fst_gluedCocone_ι_assoc, gluedCocone_pt
isColimit 📖	CompOp	—
isColimitGluedCocone 📖	CompOp	—
pullbackGluedIso 📖	CompOp	4 math math: pullbackGluedIso_inv_snd_assoc, pullbackGluedIso_inv_fst_assoc, pullbackGluedIso_inv_snd, pullbackGluedIso_inv_fst
relativeGluingData 📖	CompOp	6 math math: pullbackGluedIso_inv_fst_assoc, fst_gluedCocone_ι, fst_gluedCocone_ι_assoc, relativeGluingData_functor, pullbackGluedIso_inv_fst, relativeGluingData_natTrans_app
trans 📖	CompOp	4 math math: cocone_ι_transitionMap, transitionCocone_ι_app, cocone_ι_transitionMap_assoc, trans_app_left
transitionCocone 📖	CompOp	2 math math: transitionCocone_pt, transitionCocone_ι_app
transitionMap 📖	CompOp	6 math math: isPullback, cocone_ι_transitionMap, transitionMap_id, cocone_ι_transitionMap_assoc, transitionMap_comp, functor_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cocone_ι_transitionMap 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.MorphismProperty.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over.map CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition AlgebraicGeometry.Scheme.Cover.trans prop_trans CategoryTheory.Functor.comp CategoryTheory.MorphismProperty.Over.pullback CategoryTheory.PreZeroHypercover.f CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt cocone CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι transitionMap trans	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition prop_trans CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.Limits.IsColimit.fac
cocone_ι_transitionMap_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.MorphismProperty.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over.map CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition AlgebraicGeometry.Scheme.Cover.trans prop_trans CategoryTheory.MorphismProperty.Over.pullback CategoryTheory.PreZeroHypercover.f CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp cocone CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι transitionMap trans	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition prop_trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cocone_ι_transitionMap
fst_gluedCocone_ι 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.MorphismProperty.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Over.pullback AlgebraicGeometry.Scheme.Cover.trans CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt gluedCocone CategoryTheory.Limits.pullback.fst CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Functor.comp cocone CategoryTheory.Limits.colimit AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor relativeGluingData AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin CategoryTheory.Limits.colimit.ι	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion
fst_gluedCocone_ι_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.MorphismProperty.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Over.pullback AlgebraicGeometry.Scheme.Cover.trans CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback CategoryTheory.Comma.left CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.fst CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt gluedCocone CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Functor.comp cocone CategoryTheory.Limits.colimit.ι AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor relativeGluingData AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fst_gluedCocone_ι
functor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion functor CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.PreZeroHypercover.X CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Over.map CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition AlgebraicGeometry.Scheme.Cover.trans prop_trans CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp CategoryTheory.MorphismProperty.Over.pullback CategoryTheory.PreZeroHypercover.f CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop cocone CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism transitionMap	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition prop_trans CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop
functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion functor CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.PreZeroHypercover.X CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Limits.Cocone.pt CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.comp CategoryTheory.MorphismProperty.Over.pullback CategoryTheory.PreZeroHypercover.f CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop cocone	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
gluedCocone_pt 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.MorphismProperty.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Over.pullback AlgebraicGeometry.Scheme.Cover.trans CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.Limits.Cocone.pt gluedCocone glued	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop
isPullback 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.MorphismProperty.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Over.pullback AlgebraicGeometry.Scheme.Cover.trans CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop	CategoryTheory.IsPullback CategoryTheory.Comma.left CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over.map CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition prop_trans CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp CategoryTheory.PreZeroHypercover.f cocone CategoryTheory.Comma.right CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism transitionMap CategoryTheory.Comma.hom	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.MorphismProperty.instRespectsIsoTop AlgebraicGeometry.Scheme.Cover.trans_map CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition prop_trans CategoryTheory.MorphismProperty.instHasOfPostcompPropertyTop CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.MorphismProperty.instIsLeftAdjointOverTopMapOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong CategoryTheory.Limits.IsColimit.ι_map CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Adjunction.counit_naturality cocone_ι_transitionMap CategoryTheory.MorphismProperty.Over.Hom.ext CategoryTheory.Limits.pullback.hom_ext CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.MorphismProperty.Over.mapPullbackAdj_counit_app CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst_snd CategoryTheory.Limits.limit.lift_π_assoc AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.IsPullback.of_iso CategoryTheory.IsPullback.of_hasPullback CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.MorphismProperty.Over.w
prop_trans 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Scheme.Cover.trans	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
pullbackGluedIso_inv_fst 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.MorphismProperty.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Over.pullback AlgebraicGeometry.Scheme.Cover.trans CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.left CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp CategoryTheory.PreZeroHypercover.f cocone CategoryTheory.Functor.obj glued CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.Iso.inv pullbackGluedIso CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.Limits.colimit.ι AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor relativeGluingData AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin CategoryTheory.IsPullback.isoPullback_hom_fst
pullbackGluedIso_inv_fst_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.MorphismProperty.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Over.pullback AlgebraicGeometry.Scheme.Cover.trans CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.left CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp CategoryTheory.PreZeroHypercover.f cocone CategoryTheory.Functor.obj glued CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.Iso.inv pullbackGluedIso CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.Limits.colimit.ι AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor relativeGluingData AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackGluedIso_inv_fst
pullbackGluedIso_inv_snd 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.MorphismProperty.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Over.pullback AlgebraicGeometry.Scheme.Cover.trans CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.left CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp CategoryTheory.PreZeroHypercover.f cocone CategoryTheory.Functor.obj glued CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.Iso.inv pullbackGluedIso CategoryTheory.Limits.pullback.snd CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.IsPullback.isoPullback_hom_snd
pullbackGluedIso_inv_snd_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.MorphismProperty.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Over.pullback AlgebraicGeometry.Scheme.Cover.trans CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.left CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp CategoryTheory.PreZeroHypercover.f cocone CategoryTheory.Functor.obj glued CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.Iso.inv pullbackGluedIso CategoryTheory.Limits.pullback.snd CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackGluedIso_inv_snd
relativeGluingData_functor 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.MorphismProperty.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Over.pullback AlgebraicGeometry.Scheme.Cover.trans CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop	AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor relativeGluingData functor	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop
relativeGluingData_natTrans_app 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.MorphismProperty.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Over.pullback AlgebraicGeometry.Scheme.Cover.trans CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop	CategoryTheory.NatTrans.app CategoryTheory.PreZeroHypercover.I₀ functor AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected AlgebraicGeometry.Scheme.Cover.RelativeGluingData.natTrans relativeGluingData CategoryTheory.Comma.hom CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp CategoryTheory.PreZeroHypercover.f cocone	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop
trans_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.comp CategoryTheory.MorphismProperty.Over.pullback CategoryTheory.PreZeroHypercover.f CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.MorphismProperty.Over.map CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition AlgebraicGeometry.Scheme.Cover.trans prop_trans CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange trans CategoryTheory.Limits.pullback.map CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition prop_trans CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange
transitionCocone_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.MorphismProperty.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.comp CategoryTheory.MorphismProperty.Over.pullback CategoryTheory.PreZeroHypercover.f CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.MorphismProperty.Over.map CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition AlgebraicGeometry.Scheme.Cover.trans prop_trans transitionCocone cocone	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition prop_trans
transitionCocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MorphismProperty.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.comp CategoryTheory.MorphismProperty.Over.pullback CategoryTheory.PreZeroHypercover.f CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.MorphismProperty.Over.map CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition AlgebraicGeometry.Scheme.Cover.trans prop_trans CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt cocone CategoryTheory.Limits.Cocone.ι CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange transitionCocone CategoryTheory.CategoryStruct.comp trans	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition prop_trans CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange
transitionMap_comp 📖	mathematical	—	transitionMap CategoryTheory.CategoryStruct.comp CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.Over Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.PreZeroHypercover.X CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over.map CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition AlgebraicGeometry.Scheme.Cover.trans prop_trans CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp CategoryTheory.MorphismProperty.Over.pullback CategoryTheory.PreZeroHypercover.f CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop cocone CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MorphismProperty.Over.mapComp CategoryTheory.MorphismProperty.instRespectsIsoTop CategoryTheory.Functor.map	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition prop_trans CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.MorphismProperty.instIsLeftAdjointOverTopMapOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong CategoryTheory.MorphismProperty.instRespectsIsoTop CategoryTheory.MorphismProperty.Over.Hom.ext CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong AlgebraicGeometry.Scheme.Cover.trans_comp CategoryTheory.Category.comp_id cocone_ι_transitionMap CategoryTheory.Limits.pullback.map.congr_simp CategoryTheory.NatTrans.naturality_assoc CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.map_comp_assoc CategoryTheory.Category.id_comp
transitionMap_id 📖	mathematical	—	transitionMap CategoryTheory.CategoryStruct.id CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.MorphismProperty.Over Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.PreZeroHypercover.X CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Over.map CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition AlgebraicGeometry.Scheme.Cover.trans CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MorphismProperty.Over.mapId CategoryTheory.MorphismProperty.instRespectsIsoTop CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp CategoryTheory.MorphismProperty.Over.pullback CategoryTheory.PreZeroHypercover.f CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop cocone	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition prop_trans CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.MorphismProperty.instIsLeftAdjointOverTopMapOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong CategoryTheory.MorphismProperty.instRespectsIsoTop CategoryTheory.MorphismProperty.Over.Hom.ext CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong cocone_ι_transitionMap AlgebraicGeometry.Scheme.Cover.trans_id CategoryTheory.Limits.pullback.map.congr_simp CategoryTheory.Limits.pullback.map_id CategoryTheory.Category.id_comp CategoryTheory.NatTrans.naturality

---

← Back to Index