GlueData

📁 Source: Mathlib/CategoryTheory/GlueData.lean

Statistics

Metric	Count
Definitions GlueData, GlueData, GlueData, GlueData, GlueData, GlueData', J, U, V, f, f', t, t', t'', J, U, V, diagram, diagramIso, f, glued, gluedIso, mapGlueData, ofGlueData', sigmaOpens, t, t', vPullbackCone, vPullbackConeIsLimitOfMap, ι, π, GlueData	32
Theorems cocycle, cocycle_assoc, f_hasPullback, f_mono, t_fac, t_inv, t_inv_assoc, cocycle, cocycle_assoc, diagramIso_app_left, diagramIso_app_right, diagramIso_hom_app_left, diagramIso_hom_app_right, diagramIso_inv_app_left, diagramIso_inv_app_right, diagram_fst, diagram_left, diagram_right, diagram_snd, f_hasPullback, f_id, f_mono, glue_condition, glue_condition_apply, hasColimit_mapGlueData_diagram, hasColimit_multispan_comp, instHasPullbackMapF, mapGlueData_J, mapGlueData_U, mapGlueData_V, mapGlueData_f, mapGlueData_t, mapGlueData_t', t'_comp_eq_pullbackSymmetry, t'_comp_eq_pullbackSymmetry_assoc, t'_iij, t'_iji, t'_inv, t'_isIso, t'_jii, t_fac, t_fac_assoc, t_id, t_inv, t_inv_apply, t_inv_assoc, t_isIso, types_ι_jointly_surjective, types_π_surjective, ι_gluedIso_hom, ι_gluedIso_hom_assoc, ι_gluedIso_inv, ι_gluedIso_inv_assoc, ι_jointly_surjective, π_epi, instHasPullbackF', instIsIsoF', instMonoF'	58
Total	90

AlgebraicGeometry.LocallyRingedSpace

Definitions

Name	Category	Theorems
GlueData 📖	CompData	—

AlgebraicGeometry.PresheafedSpace

Definitions

Name	Category	Theorems
GlueData 📖	CompData	—

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
GlueData 📖	CompData	—

AlgebraicGeometry.SheafedSpace

Definitions

Name	Category	Theorems
GlueData 📖	CompData	—

CategoryTheory

Definitions

Name	Category	Theorems
GlueData 📖	CompData	—
GlueData' 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasPullbackF' 📖	mathematical	—	Limits.HasPullback GlueData'.J GlueData'.U GlueData'.V GlueData'.f'	—	Limits.hasPullback_of_left_iso instIsIsoEqToHom Limits.hasPullback_of_right_iso Category.id_comp GlueData'.f_hasPullback
instIsIsoF' 📖	mathematical	—	IsIso GlueData'.J GlueData'.U GlueData'.V GlueData'.f'	—	instIsIsoEqToHom
instMonoF' 📖	mathematical	—	Mono GlueData'.J GlueData'.U GlueData'.V GlueData'.f'	—	mono_of_strongMono strongMono_of_isIso instIsIsoEqToHom mono_comp GlueData'.f_mono

CategoryTheory.GlueData

Definitions

Name	Category	Theorems
J 📖	CompOp	105 math math: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc, TopCat.GlueData.preimage_image_eq_image, TopCat.GlueData.π_surjective, TopCat.GlueData.open_image_open, TopCat.GlueData.ι_fromOpenSubsetsGlue, types_π_surjective, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersion, AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersion, TopCat.GlueData.isOpen_iff, TopCat.GlueData.ι_fromOpenSubsetsGlue_apply, t'_iij, AlgebraicGeometry.SheafedSpace.GlueData.f_open, t_inv, TopCat.GlueData.rel_equiv, AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base, AlgebraicGeometry.Scheme.GlueData.glue_condition, AlgebraicGeometry.Scheme.GlueData.f_open, f_id, t'_iji, AlgebraicGeometry.Scheme.GlueData.instPreservesColimitTopCatWalkingMultispanProdJMultispanDiagramForgetToTop, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, glue_condition_apply, AlgebraicGeometry.Scheme.Pullback.gluing_J, AlgebraicGeometry.Scheme.GlueData.instPreservesColimitWalkingMultispanProdJMultispanDiagramForget, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι_assoc, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionιLocallyRingedSpaceToLocallyRingedSpaceGlueData, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, TopCat.GlueData.f_open, AlgebraicGeometry.Scheme.Cover.gluedCover_J, t_fac, t_inv_apply, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', TopCat.GlueData.range_fromOpenSubsetsGlue, AlgebraicGeometry.Scheme.GlueData.ι_eq_iff, t'_comp_eq_pullbackSymmetry_assoc, diagram_left, glue_condition, diagram_snd, TopCat.GlueData.fromOpenSubsetsGlue_isOpenEmbedding, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, t_fac_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.ι_isOpenEmbedding, AlgebraicGeometry.PresheafedSpace.GlueData.f_open, AlgebraicGeometry.PresheafedSpace.GlueData.componentwise_diagram_π_isIso, AlgebraicGeometry.SheafedSpace.GlueData.ι_isoPresheafedSpace_inv, TopCat.GlueData.fromOpenSubsetsGlue_injective, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, t'_inv, AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₂, t_inv_assoc, t'_jii, TopCat.GlueData.ι_isOpenEmbedding, cocycle_assoc, TopCat.GlueData.ofOpenSubsets_toGlueData_J, π_epi, AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.Scheme.Pullback.gluing_ι, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, TopCat.GlueData.preimage_range, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, TopCat.GlueData.ι_mono, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv_assoc, diagram_fst, t_isIso, AlgebraicGeometry.SheafedSpace.GlueData.ιIsOpenImmersion, f_mono, t_id, TopCat.GlueData.image_inter, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι, TopCat.GlueData.fromOpenSubsetsGlue_isOpenMap, AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv, AlgebraicGeometry.PresheafedSpace.GlueData.ι_jointly_surjective, AlgebraicGeometry.Scheme.GlueData.glue_condition_assoc, TopCat.GlueData.ι_jointly_surjective, hasColimit_multispan_comp, AlgebraicGeometry.Scheme.GlueData.oneHypercover_I₀, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_J, AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π, AlgebraicGeometry.Scheme.GlueData.openCover_I₀, TopCat.GlueData.ι_eq_iff_rel, cocycle, AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π, t'_isIso, diagram_right, AlgebraicGeometry.LocallyRingedSpace.GlueData.f_open, types_ι_jointly_surjective, AlgebraicGeometry.Scheme.GlueData.oneHypercover_Y, t'_comp_eq_pullbackSymmetry, TopCat.GlueData.ι_injective, AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', f_hasPullback, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionFLocallyRingedSpaceToLocallyRingedSpaceGlueData, TopCat.GlueData.preimage_image_eq_image', AlgebraicGeometry.LocallyRingedSpace.GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace, AlgebraicGeometry.SheafedSpace.GlueData.ι_jointly_surjective, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst
U 📖	CompOp	89 math math: TopCat.GlueData.preimage_image_eq_image, TopCat.GlueData.π_surjective, TopCat.GlueData.open_image_open, TopCat.GlueData.ι_fromOpenSubsetsGlue, types_π_surjective, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersion, AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersion, TopCat.GlueData.ofOpenSubsets_toGlueData_U, TopCat.GlueData.isOpen_iff, AlgebraicGeometry.Scheme.Cover.gluedCover_U, TopCat.GlueData.ι_fromOpenSubsetsGlue_apply, t'_iij, AlgebraicGeometry.SheafedSpace.GlueData.f_open, TopCat.GlueData.rel_equiv, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base, AlgebraicGeometry.Scheme.Cover.ι_fromGlued_assoc, AlgebraicGeometry.Scheme.GlueData.glue_condition, AlgebraicGeometry.Scheme.GlueData.f_open, f_id, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst_assoc, AlgebraicGeometry.Scheme.GlueData.isOpen_iff, t'_iji, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, glue_condition_apply, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst, AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionιLocallyRingedSpaceToLocallyRingedSpaceGlueData, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, TopCat.GlueData.f_open, t_fac, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', AlgebraicGeometry.Scheme.GlueData.ι_eq_iff, t'_comp_eq_pullbackSymmetry_assoc, glue_condition, AlgebraicGeometry.Scheme.GlueData.openCover_X, diagram_snd, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective, AlgebraicGeometry.Scheme.Pullback.gluing_U, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, t_fac_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.ι_isOpenEmbedding, AlgebraicGeometry.PresheafedSpace.GlueData.f_open, AlgebraicGeometry.SheafedSpace.GlueData.ι_isoPresheafedSpace_inv, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, t'_inv, AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₂, t'_jii, TopCat.GlueData.ι_isOpenEmbedding, cocycle_assoc, π_epi, AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, TopCat.GlueData.preimage_range, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, TopCat.GlueData.ι_mono, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv_assoc, AlgebraicGeometry.SheafedSpace.GlueData.ιIsOpenImmersion, f_mono, TopCat.GlueData.image_inter, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, AlgebraicGeometry.Scheme.GlueData.oneHypercover_X, AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv, AlgebraicGeometry.PresheafedSpace.GlueData.ι_jointly_surjective, AlgebraicGeometry.Scheme.GlueData.glue_condition_assoc, TopCat.GlueData.ι_jointly_surjective, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd, AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π, TopCat.GlueData.ι_eq_iff_rel, cocycle, AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π, t'_isIso, diagram_right, AlgebraicGeometry.LocallyRingedSpace.GlueData.f_open, AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_U, t'_comp_eq_pullbackSymmetry, TopCat.GlueData.ι_injective, AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', f_hasPullback, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionFLocallyRingedSpaceToLocallyRingedSpaceGlueData, TopCat.GlueData.preimage_image_eq_image', AlgebraicGeometry.LocallyRingedSpace.GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace, AlgebraicGeometry.SheafedSpace.GlueData.ι_jointly_surjective, AlgebraicGeometry.Scheme.Cover.ι_fromGlued
V 📖	CompOp	58 math math: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc, TopCat.GlueData.preimage_image_eq_image, t'_iij, AlgebraicGeometry.SheafedSpace.GlueData.f_open, t_inv, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base, AlgebraicGeometry.Scheme.Cover.gluedCover_V, AlgebraicGeometry.Scheme.GlueData.glue_condition, AlgebraicGeometry.Scheme.GlueData.f_open, f_id, t'_iji, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, glue_condition_apply, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, TopCat.GlueData.f_open, t_fac, t_inv_apply, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', t'_comp_eq_pullbackSymmetry_assoc, diagram_left, glue_condition, diagram_snd, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, t_fac_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.f_open, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, t'_inv, AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₂, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_V, t_inv_assoc, t'_jii, cocycle_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, TopCat.GlueData.preimage_range, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, t_isIso, TopCat.GlueData.ofOpenSubsets_toGlueData_V, f_mono, t_id, TopCat.GlueData.image_inter, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, AlgebraicGeometry.Scheme.GlueData.glue_condition_assoc, cocycle, t'_isIso, AlgebraicGeometry.LocallyRingedSpace.GlueData.f_open, AlgebraicGeometry.Scheme.GlueData.oneHypercover_Y, t'_comp_eq_pullbackSymmetry, AlgebraicGeometry.Scheme.Pullback.gluing_V, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', f_hasPullback, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionFLocallyRingedSpaceToLocallyRingedSpaceGlueData, TopCat.GlueData.preimage_image_eq_image', AlgebraicGeometry.LocallyRingedSpace.GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst
diagram 📖	CompOp	56 math math: diagramIso_app_right, TopCat.GlueData.preimage_image_eq_image, TopCat.GlueData.π_surjective, TopCat.GlueData.open_image_open, TopCat.GlueData.ι_fromOpenSubsetsGlue, types_π_surjective, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersion, AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersion, TopCat.GlueData.isOpen_iff, TopCat.GlueData.ι_fromOpenSubsetsGlue_apply, AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram, AlgebraicGeometry.Scheme.GlueData.instPreservesColimitTopCatWalkingMultispanProdJMultispanDiagramForgetToTop, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, diagramIso_app_left, AlgebraicGeometry.Scheme.GlueData.instPreservesColimitWalkingMultispanProdJMultispanDiagramForget, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι_assoc, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionιLocallyRingedSpaceToLocallyRingedSpaceGlueData, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, diagramIso_inv_app_left, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', TopCat.GlueData.range_fromOpenSubsetsGlue, diagramIso_inv_app_right, diagram_left, diagram_snd, TopCat.GlueData.fromOpenSubsetsGlue_isOpenEmbedding, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective, AlgebraicGeometry.PresheafedSpace.GlueData.ι_isOpenEmbedding, AlgebraicGeometry.SheafedSpace.GlueData.ι_isoPresheafedSpace_inv, TopCat.GlueData.fromOpenSubsetsGlue_injective, TopCat.GlueData.ι_isOpenEmbedding, AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.Scheme.Pullback.gluing_ι, TopCat.GlueData.preimage_range, TopCat.GlueData.ι_mono, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv_assoc, diagram_fst, AlgebraicGeometry.SheafedSpace.GlueData.ιIsOpenImmersion, TopCat.GlueData.image_inter, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι, TopCat.GlueData.fromOpenSubsetsGlue_isOpenMap, AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv, AlgebraicGeometry.PresheafedSpace.GlueData.ι_jointly_surjective, TopCat.GlueData.ι_jointly_surjective, hasColimit_multispan_comp, AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π, TopCat.GlueData.ι_eq_iff_rel, diagram_right, types_ι_jointly_surjective, hasColimit_mapGlueData_diagram, TopCat.GlueData.ι_injective, diagramIso_hom_app_right, TopCat.GlueData.preimage_image_eq_image', AlgebraicGeometry.SheafedSpace.GlueData.ι_jointly_surjective, diagramIso_hom_app_left
diagramIso 📖	CompOp	6 math math: diagramIso_app_right, diagramIso_app_left, diagramIso_inv_app_left, diagramIso_inv_app_right, diagramIso_hom_app_right, diagramIso_hom_app_left
f 📖	CompOp	49 math math: TopCat.GlueData.preimage_image_eq_image, t'_iij, AlgebraicGeometry.SheafedSpace.GlueData.f_open, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base, AlgebraicGeometry.Scheme.GlueData.glue_condition, AlgebraicGeometry.Scheme.GlueData.f_open, f_id, t'_iji, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, glue_condition_apply, AlgebraicGeometry.Scheme.Pullback.gluing_f, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, TopCat.GlueData.f_open, t_fac, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', t'_comp_eq_pullbackSymmetry_assoc, glue_condition, diagram_snd, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, t_fac_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.f_open, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, t'_inv, AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₂, t'_jii, cocycle_assoc, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_f, AlgebraicGeometry.Scheme.Cover.gluedCover_f, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, TopCat.GlueData.preimage_range, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, diagram_fst, f_mono, TopCat.GlueData.image_inter, TopCat.GlueData.ofOpenSubsets_toGlueData_f, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, AlgebraicGeometry.Scheme.GlueData.glue_condition_assoc, cocycle, t'_isIso, AlgebraicGeometry.LocallyRingedSpace.GlueData.f_open, AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₁, t'_comp_eq_pullbackSymmetry, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', f_hasPullback, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionFLocallyRingedSpaceToLocallyRingedSpaceGlueData, TopCat.GlueData.preimage_image_eq_image', AlgebraicGeometry.LocallyRingedSpace.GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace
glued 📖	CompOp	47 math math: TopCat.GlueData.preimage_image_eq_image, TopCat.GlueData.π_surjective, TopCat.GlueData.open_image_open, TopCat.GlueData.ι_fromOpenSubsetsGlue, types_π_surjective, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersion, AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersion, ι_gluedIso_inv, TopCat.GlueData.isOpen_iff, TopCat.GlueData.ι_fromOpenSubsetsGlue_apply, ι_gluedIso_inv_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, glue_condition_apply, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv, AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionιLocallyRingedSpaceToLocallyRingedSpaceGlueData, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', TopCat.GlueData.range_fromOpenSubsetsGlue, AlgebraicGeometry.Scheme.GlueData.ι_eq_iff, glue_condition, TopCat.GlueData.fromOpenSubsetsGlue_isOpenEmbedding, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective, AlgebraicGeometry.PresheafedSpace.GlueData.ι_isOpenEmbedding, AlgebraicGeometry.SheafedSpace.GlueData.ι_isoPresheafedSpace_inv, TopCat.GlueData.fromOpenSubsetsGlue_injective, TopCat.GlueData.ι_isOpenEmbedding, π_epi, AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, TopCat.GlueData.preimage_range, TopCat.GlueData.ι_mono, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv_assoc, AlgebraicGeometry.SheafedSpace.GlueData.ιIsOpenImmersion, TopCat.GlueData.image_inter, TopCat.GlueData.fromOpenSubsetsGlue_isOpenMap, AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv, ι_gluedIso_hom, AlgebraicGeometry.PresheafedSpace.GlueData.ι_jointly_surjective, TopCat.GlueData.ι_jointly_surjective, AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π, TopCat.GlueData.ι_eq_iff_rel, TopCat.GlueData.ι_injective, ι_gluedIso_hom_assoc, ι_jointly_surjective, TopCat.GlueData.preimage_image_eq_image', AlgebraicGeometry.SheafedSpace.GlueData.ι_jointly_surjective
gluedIso 📖	CompOp	4 math math: ι_gluedIso_inv, ι_gluedIso_inv_assoc, ι_gluedIso_hom, ι_gluedIso_hom_assoc
mapGlueData 📖	CompOp	18 math math: diagramIso_app_right, ι_gluedIso_inv, ι_gluedIso_inv_assoc, diagramIso_app_left, mapGlueData_J, mapGlueData_U, diagramIso_inv_app_left, diagramIso_inv_app_right, mapGlueData_t, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv_assoc, mapGlueData_f, ι_gluedIso_hom, hasColimit_mapGlueData_diagram, ι_gluedIso_hom_assoc, mapGlueData_t', diagramIso_hom_app_right, diagramIso_hom_app_left, mapGlueData_V
ofGlueData' 📖	CompOp	—
sigmaOpens 📖	CompOp	3 math math: TopCat.GlueData.π_surjective, types_π_surjective, π_epi
t 📖	CompOp	29 math math: TopCat.GlueData.preimage_image_eq_image, AlgebraicGeometry.Scheme.Cover.gluedCover_t, TopCat.GlueData.ofOpenSubsets_toGlueData_t, t_inv, AlgebraicGeometry.Scheme.Pullback.gluing_t, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, AlgebraicGeometry.Scheme.GlueData.glue_condition, t'_iji, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, glue_condition_apply, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, t_fac, t_inv_apply, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', glue_condition, diagram_snd, t_fac_assoc, mapGlueData_t, AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₂, t_inv_assoc, t'_jii, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, t_isIso, t_id, AlgebraicGeometry.Scheme.GlueData.glue_condition_assoc, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', TopCat.GlueData.preimage_image_eq_image'
t' 📖	CompOp	18 math math: t'_iij, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, t'_iji, t_fac, t'_comp_eq_pullbackSymmetry_assoc, t_fac_assoc, t'_inv, t'_jii, cocycle_assoc, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t', AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, cocycle, t'_isIso, AlgebraicGeometry.Scheme.Pullback.gluing_t', t'_comp_eq_pullbackSymmetry, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', mapGlueData_t', AlgebraicGeometry.Scheme.Cover.gluedCover_t'
vPullbackCone 📖	CompOp	—
vPullbackConeIsLimitOfMap 📖	CompOp	—
ι 📖	CompOp	41 math math: TopCat.GlueData.preimage_image_eq_image, TopCat.GlueData.open_image_open, TopCat.GlueData.ι_fromOpenSubsetsGlue, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersion, AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersion, ι_gluedIso_inv, TopCat.GlueData.isOpen_iff, TopCat.GlueData.ι_fromOpenSubsetsGlue_apply, ι_gluedIso_inv_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, glue_condition_apply, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv, AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionιLocallyRingedSpaceToLocallyRingedSpaceGlueData, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', AlgebraicGeometry.Scheme.GlueData.ι_eq_iff, glue_condition, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective, AlgebraicGeometry.PresheafedSpace.GlueData.ι_isOpenEmbedding, AlgebraicGeometry.SheafedSpace.GlueData.ι_isoPresheafedSpace_inv, TopCat.GlueData.ι_isOpenEmbedding, AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, TopCat.GlueData.preimage_range, TopCat.GlueData.ι_mono, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv_assoc, AlgebraicGeometry.SheafedSpace.GlueData.ιIsOpenImmersion, TopCat.GlueData.image_inter, AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv, ι_gluedIso_hom, AlgebraicGeometry.PresheafedSpace.GlueData.ι_jointly_surjective, TopCat.GlueData.ι_jointly_surjective, AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π, TopCat.GlueData.ι_eq_iff_rel, types_ι_jointly_surjective, TopCat.GlueData.ι_injective, ι_gluedIso_hom_assoc, ι_jointly_surjective, TopCat.GlueData.preimage_image_eq_image', AlgebraicGeometry.SheafedSpace.GlueData.ι_jointly_surjective
π 📖	CompOp	3 math math: TopCat.GlueData.π_surjective, types_π_surjective, π_epi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cocycle 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback V J U f f_hasPullback t' CategoryTheory.CategoryStruct.id	—	—
cocycle_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback V J U f f_hasPullback t'	—	f_hasPullback CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' cocycle
diagramIso_app_left 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	CategoryTheory.Iso.app CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Functor.comp CategoryTheory.Limits.MultispanIndex.multispan diagram mapGlueData diagramIso CategoryTheory.Limits.WalkingMultispan.left CategoryTheory.Iso.refl CategoryTheory.Functor.obj	—	—
diagramIso_app_right 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	CategoryTheory.Iso.app CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Functor.comp CategoryTheory.Limits.MultispanIndex.multispan diagram mapGlueData diagramIso CategoryTheory.Limits.WalkingMultispan.right CategoryTheory.Iso.refl CategoryTheory.Functor.obj	—	—
diagramIso_hom_app_left 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Functor.comp CategoryTheory.Limits.MultispanIndex.multispan diagram mapGlueData CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category diagramIso CategoryTheory.Limits.WalkingMultispan.left CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
diagramIso_hom_app_right 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Functor.comp CategoryTheory.Limits.MultispanIndex.multispan diagram mapGlueData CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category diagramIso CategoryTheory.Limits.WalkingMultispan.right CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
diagramIso_inv_app_left 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan mapGlueData diagram CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category diagramIso CategoryTheory.Limits.WalkingMultispan.left CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
diagramIso_inv_app_right 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan mapGlueData diagram CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category diagramIso CategoryTheory.Limits.WalkingMultispan.right CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
diagram_fst 📖	mathematical	—	CategoryTheory.Limits.MultispanIndex.fst CategoryTheory.Limits.MultispanShape.prod J diagram f	—	—
diagram_left 📖	mathematical	—	CategoryTheory.Limits.MultispanIndex.left CategoryTheory.Limits.MultispanShape.prod J diagram V	—	—
diagram_right 📖	mathematical	—	CategoryTheory.Limits.MultispanIndex.right CategoryTheory.Limits.MultispanShape.prod J diagram U	—	—
diagram_snd 📖	mathematical	—	CategoryTheory.Limits.MultispanIndex.snd CategoryTheory.Limits.MultispanShape.prod J diagram CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct V U t f	—	—
f_hasPullback 📖	mathematical	—	CategoryTheory.Limits.HasPullback V J U f	—	—
f_id 📖	mathematical	—	CategoryTheory.IsIso V J U f	—	—
f_mono 📖	mathematical	—	CategoryTheory.Mono V J U f	—	—
glue_condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct V J glued t U f ι	—	CategoryTheory.Category.assoc CategoryTheory.Limits.Multicoequalizer.condition
glue_condition_apply 📖	mathematical	—	DFunLike.coe U glued CategoryTheory.ConcreteCategory.hom ι V J f t	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise glue_condition
hasColimit_mapGlueData_diagram 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	CategoryTheory.Limits.HasMulticoequalizer CategoryTheory.Limits.MultispanShape.prod mapGlueData diagram	—	CategoryTheory.Limits.hasColimit_of_iso hasColimit_multispan_comp
hasColimit_multispan_comp 📖	mathematical	—	CategoryTheory.Limits.HasColimit CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod J CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Functor.comp CategoryTheory.Limits.MultispanIndex.multispan diagram	—	—
instHasPullbackMapF 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	CategoryTheory.Limits.HasPullback CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	f_hasPullback
mapGlueData_J 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	mapGlueData	—	—
mapGlueData_U 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	mapGlueData CategoryTheory.Functor.obj	—	—
mapGlueData_V 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	mapGlueData CategoryTheory.Functor.obj	—	—
mapGlueData_f 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	mapGlueData CategoryTheory.Functor.map	—	—
mapGlueData_t 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	t mapGlueData CategoryTheory.Functor.map	—	—
mapGlueData_t' 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	t' mapGlueData CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Functor.map f_hasPullback CategoryTheory.Iso.inv instHasPullbackMapF CategoryTheory.Limits.PreservesPullback.iso CategoryTheory.Iso.hom	—	—
t'_comp_eq_pullbackSymmetry 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback V J U f f_hasPullback t' CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Iso.hom CategoryTheory.Limits.pullbackSymmetry	—	f_hasPullback t'_isIso CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.IsIso.eq_inv_of_hom_inv_id cocycle CategoryTheory.cancel_mono CategoryTheory.Limits.pullback.fst_of_mono f_mono CategoryTheory.Category.assoc CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst t_fac CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc t_fac_assoc t_inv CategoryTheory.Category.comp_id
t'_comp_eq_pullbackSymmetry_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback V J U f f_hasPullback t' CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Iso.hom CategoryTheory.Limits.pullbackSymmetry	—	f_hasPullback CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' t'_comp_eq_pullbackSymmetry
t'_iij 📖	mathematical	—	t' CategoryTheory.Iso.hom CategoryTheory.Limits.pullback V J U f f_hasPullback CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Limits.pullbackSymmetry	—	f_hasPullback t_fac f_id CategoryTheory.IsIso.eq_comp_inv CategoryTheory.Limits.pullback.condition CategoryTheory.Category.comp_id t_id CategoryTheory.Mono.right_cancellation CategoryTheory.Limits.pullback.fst_of_mono f_mono CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Category.assoc CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst
t'_iji 📖	mathematical	—	t' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback V J U f f_hasPullback CategoryTheory.Limits.pullback.fst t CategoryTheory.inv CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.isIso_snd_of_mono f_mono	—	f_hasPullback CategoryTheory.Limits.isIso_snd_of_mono f_mono CategoryTheory.Category.assoc t_fac CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id
t'_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback V J U f f_hasPullback CategoryTheory.Limits.hasPullback_symmetry t' CategoryTheory.Iso.hom CategoryTheory.Limits.pullbackSymmetry CategoryTheory.CategoryStruct.id	—	f_hasPullback CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.cancel_mono CategoryTheory.Limits.pullback.fst_of_mono f_mono CategoryTheory.Category.assoc CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst t_fac CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc t_fac_assoc t_inv CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
t'_isIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.pullback V J U f f_hasPullback t'	—	f_hasPullback cocycle CategoryTheory.Category.assoc
t'_jii 📖	mathematical	—	t' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback V J U f f_hasPullback CategoryTheory.Limits.pullback.fst t CategoryTheory.inv CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback_snd_iso_of_left_iso f_id	—	f_hasPullback CategoryTheory.Limits.pullback_snd_iso_of_left_iso f_id CategoryTheory.Category.assoc t_fac CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id
t_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback V J U f f_hasPullback t' CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst t	—	—
t_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback V J U f f_hasPullback t' CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst t	—	f_hasPullback CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' t_fac
t_id 📖	mathematical	—	t CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct V J	—	—
t_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct V J t CategoryTheory.CategoryStruct.id	—	f_hasPullback CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Limits.pullback_fst_iso_of_right_iso f_id CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst cocycle CategoryTheory.Category.comp_id CategoryTheory.IsIso.inv_hom_id CategoryTheory.IsIso.comp_inv_eq CategoryTheory.Category.assoc CategoryTheory.IsIso.eq_inv_comp CategoryTheory.Limits.isIso_snd_of_mono f_mono CategoryTheory.Limits.has_kernel_pair_of_mono CategoryTheory.Limits.pullback_snd_iso_of_left_iso CategoryTheory.IsIso.inv_hom_id_assoc CategoryTheory.Limits.fst_eq_snd_of_mono_eq t'_iji t'_jii t'_iij
t_inv_apply 📖	mathematical	—	DFunLike.coe V J CategoryTheory.ConcreteCategory.hom t	—	CategoryTheory.comp_apply CategoryTheory.id_apply Mathlib.Tactic.Elementwise.hom_elementwise t_inv
t_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct V J t	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' t_inv
t_isIso 📖	mathematical	—	CategoryTheory.IsIso V J t	—	t_inv
types_ι_jointly_surjective 📖	mathematical	—	ι CategoryTheory.types CategoryTheory.Limits.Types.hasColimit CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod J CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan diagram	—	CategoryTheory.Limits.Types.hasColimit CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.instSmallDiscrete CategoryTheory.Limits.Multicoequalizer.ι_sigmaπ CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.Types.hasColimitsOfSize types_π_surjective CategoryTheory.ConcreteCategory.congr_hom CategoryTheory.Iso.hom_inv_id
types_π_surjective 📖	mathematical	—	sigmaOpens CategoryTheory.types CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete J CategoryTheory.discreteCategory CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CategoryTheory.Discrete.functor U glued CategoryTheory.Limits.Types.hasColimit CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan diagram π	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CategoryTheory.Limits.Types.hasColimit CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small CategoryTheory.epi_iff_surjective π_epi
ι_gluedIso_hom 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj glued mapGlueData hasColimit_mapGlueData_diagram CategoryTheory.Functor.map ι CategoryTheory.Iso.hom gluedIso	—	hasColimit_mapGlueData_diagram CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.ι_preservesColimitIso_hom_assoc CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom CategoryTheory.Category.id_comp
ι_gluedIso_hom_assoc 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj glued CategoryTheory.Functor.map ι mapGlueData hasColimit_mapGlueData_diagram CategoryTheory.Iso.hom gluedIso	—	hasColimit_mapGlueData_diagram CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_gluedIso_hom
ι_gluedIso_inv 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapGlueData glued hasColimit_mapGlueData_diagram CategoryTheory.Functor.obj ι CategoryTheory.Iso.inv gluedIso CategoryTheory.Functor.map	—	hasColimit_mapGlueData_diagram CategoryTheory.Iso.comp_inv_eq ι_gluedIso_hom
ι_gluedIso_inv_assoc 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapGlueData glued hasColimit_mapGlueData_diagram ι CategoryTheory.Functor.obj CategoryTheory.Iso.inv gluedIso CategoryTheory.Functor.map	—	hasColimit_mapGlueData_diagram CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_gluedIso_inv
ι_jointly_surjective 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.types CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan V J U f	CategoryTheory.Functor.map glued ι	—	hasColimit_mapGlueData_diagram CategoryTheory.Limits.Types.hasColimit CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self types_ι_jointly_surjective ι_gluedIso_inv CategoryTheory.Iso.hom_inv_id
π_epi 📖	mathematical	—	CategoryTheory.Epi sigmaOpens CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete J CategoryTheory.discreteCategory CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Discrete.functor U glued π	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.Multicoequalizer.instEpiSigmaπ

CategoryTheory.GlueData'

Definitions

Name	Category	Theorems
J 📖	CompOp	8 math math: CategoryTheory.instMonoF', cocycle_assoc, cocycle, CategoryTheory.instHasPullbackF', t_inv, t_inv_assoc, t_fac, CategoryTheory.instIsIsoF'
U 📖	CompOp	8 math math: CategoryTheory.instMonoF', cocycle_assoc, cocycle, CategoryTheory.instHasPullbackF', f_mono, t_fac, f_hasPullback, CategoryTheory.instIsIsoF'
V 📖	CompOp	10 math math: CategoryTheory.instMonoF', cocycle_assoc, cocycle, CategoryTheory.instHasPullbackF', t_inv, t_inv_assoc, f_mono, t_fac, f_hasPullback, CategoryTheory.instIsIsoF'
f 📖	CompOp	5 math math: cocycle_assoc, cocycle, f_mono, t_fac, f_hasPullback
f' 📖	CompOp	3 math math: CategoryTheory.instMonoF', CategoryTheory.instHasPullbackF', CategoryTheory.instIsIsoF'
t 📖	CompOp	3 math math: t_inv, t_inv_assoc, t_fac
t' 📖	CompOp	3 math math: cocycle_assoc, cocycle, t_fac
t'' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cocycle 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback V U f f_hasPullback J t' CategoryTheory.CategoryStruct.id	—	—
cocycle_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback V U f f_hasPullback J t'	—	f_hasPullback CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' cocycle
f_hasPullback 📖	mathematical	—	CategoryTheory.Limits.HasPullback V U f	—	—
f_mono 📖	mathematical	—	CategoryTheory.Mono V U f	—	—
t_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback V U f f_hasPullback J t' CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst t	—	—
t_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct V J t CategoryTheory.CategoryStruct.id	—	—
t_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct V J t	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' t_inv

TopCat

Definitions

Name	Category	Theorems
GlueData 📖	CompData	—

---

← Back to Index