Gluing

📁 Source: Mathlib/Topology/Gluing.lean

Statistics

Metric	Count
Definitions MkCore, J, U, V, t, t', fromOpenSubsetsGlue, mk', ofOpenSubsets, openCoverGlueHomeo, toGlueData	11
Theorems V_id, cocycle, t_id, t_inter, t_inv, eqvGen_of_π_eq, f_open, fromOpenSubsetsGlue_injective, fromOpenSubsetsGlue_isOpenEmbedding, fromOpenSubsetsGlue_isOpenMap, image_inter, instIsIsoT, isOpen_iff, ofOpenSubsets_toGlueData_J, ofOpenSubsets_toGlueData_U, ofOpenSubsets_toGlueData_V, ofOpenSubsets_toGlueData_f, ofOpenSubsets_toGlueData_t, open_image_open, preimage_image_eq_image, preimage_image_eq_image', preimage_range, range_fromOpenSubsetsGlue, rel_equiv, ι_eq_iff_rel, ι_fromOpenSubsetsGlue, ι_fromOpenSubsetsGlue_apply, ι_injective, ι_isOpenEmbedding, ι_jointly_surjective, ι_mono, π_surjective	32
Total	43

TopCat.GlueData

Definitions

Name	Category	Theorems
MkCore 📖	CompData	—
fromOpenSubsetsGlue 📖	CompOp	6 math math: ι_fromOpenSubsetsGlue, ι_fromOpenSubsetsGlue_apply, range_fromOpenSubsetsGlue, fromOpenSubsetsGlue_isOpenEmbedding, fromOpenSubsetsGlue_injective, fromOpenSubsetsGlue_isOpenMap
mk' 📖	CompOp	—
ofOpenSubsets 📖	CompOp	11 math math: ι_fromOpenSubsetsGlue, ofOpenSubsets_toGlueData_U, ι_fromOpenSubsetsGlue_apply, ofOpenSubsets_toGlueData_t, range_fromOpenSubsetsGlue, fromOpenSubsetsGlue_isOpenEmbedding, fromOpenSubsetsGlue_injective, ofOpenSubsets_toGlueData_J, ofOpenSubsets_toGlueData_V, ofOpenSubsets_toGlueData_f, fromOpenSubsetsGlue_isOpenMap
openCoverGlueHomeo 📖	CompOp	—
toGlueData 📖	CompOp	27 math math: eqvGen_of_π_eq, preimage_image_eq_image, π_surjective, open_image_open, ι_fromOpenSubsetsGlue, ofOpenSubsets_toGlueData_U, isOpen_iff, ι_fromOpenSubsetsGlue_apply, ofOpenSubsets_toGlueData_t, rel_equiv, f_open, range_fromOpenSubsetsGlue, fromOpenSubsetsGlue_isOpenEmbedding, fromOpenSubsetsGlue_injective, ι_isOpenEmbedding, ofOpenSubsets_toGlueData_J, AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv, preimage_range, ι_mono, ofOpenSubsets_toGlueData_V, image_inter, ofOpenSubsets_toGlueData_f, fromOpenSubsetsGlue_isOpenMap, ι_jointly_surjective, ι_eq_iff_rel, ι_injective, preimage_image_eq_image'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqvGen_of_π_eq 📖	mathematical	DFunLike.coe CategoryTheory.GlueData.sigmaOpens TopCat TopCat.instCategory toGlueData CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.GlueData.J CategoryTheory.discreteCategory CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize TopCat.topCat_hasColimits CategoryTheory.Discrete.functor CategoryTheory.GlueData.U CategoryTheory.GlueData.glued CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopCat.carrier CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.GlueData.π	Relation.EqvGen TopCat.carrier CategoryTheory.Limits.sigmaObj CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J TopCat TopCat.instCategory toGlueData CategoryTheory.Limits.MultispanIndex.right CategoryTheory.GlueData.diagram CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self CategoryTheory.Discrete.functor Function.Coequalizer.Rel CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanIndex.left DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.Limits.MultispanIndex.fstSigmaMap CategoryTheory.Limits.MultispanIndex.sndSigmaMap	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize TopCat.topCat_hasColimits CategoryTheory.Limits.Multicoequalizer.instHasCoequalizerFstSigmaMapSndSigmaMap TopCat.mono_iff_injective CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Limits.Types.hasColimit univLE_of_max CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint TopCat.instIsLeftAdjointForgetContinuousMapCarrier CategoryTheory.ι_preservesColimitIso_hom CategoryTheory.ConcreteCategory.forget_map_eq_coe CategoryTheory.types_comp_apply CategoryTheory.Limits.Types.hasColimitsOfShape Quot.eq CategoryTheory.Limits.colimit.ι_map_assoc CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom CategoryTheory.Category.id_comp
f_open 📖	mathematical	—	Topology.IsOpenEmbedding TopCat.carrier CategoryTheory.GlueData.V TopCat TopCat.instCategory toGlueData CategoryTheory.GlueData.J CategoryTheory.GlueData.U TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.GlueData.f	—	—
fromOpenSubsetsGlue_injective 📖	mathematical	—	TopCat.carrier CategoryTheory.GlueData.glued TopCat TopCat.instCategory toGlueData ofOpenSubsets CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopCat.of DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier fromOpenSubsetsGlue	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self ι_jointly_surjective ι_eq_iff_rel ι_fromOpenSubsetsGlue_apply
fromOpenSubsetsGlue_isOpenEmbedding 📖	mathematical	—	Topology.IsOpenEmbedding TopCat.carrier CategoryTheory.GlueData.glued TopCat TopCat.instCategory toGlueData ofOpenSubsets CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopCat.of TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier fromOpenSubsetsGlue	—	Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self ContinuousMap.continuous_toFun fromOpenSubsetsGlue_injective fromOpenSubsetsGlue_isOpenMap
fromOpenSubsetsGlue_isOpenMap 📖	mathematical	—	IsOpenMap TopCat.carrier CategoryTheory.GlueData.glued TopCat TopCat.instCategory toGlueData ofOpenSubsets CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopCat.of TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier fromOpenSubsetsGlue	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self isOpen_iff_forall_mem_open ι_jointly_surjective Set.inter_subset_left Set.image_preimage_eq_inter_range Topology.IsOpenEmbedding.isOpenMap TopologicalSpace.Opens.isOpenEmbedding ι_fromOpenSubsetsGlue TopCat.coe_comp Set.preimage_comp Set.preimage_image_eq fromOpenSubsetsGlue_injective isOpen_iff Set.mem_image_of_mem ι_fromOpenSubsetsGlue_apply Set.mem_range_self
image_inter 📖	mathematical	—	Set TopCat.carrier CategoryTheory.GlueData.glued TopCat TopCat.instCategory toGlueData CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram Set.instInter Set.range CategoryTheory.GlueData.U DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.GlueData.ι CategoryTheory.GlueData.V CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GlueData.f	—	Set.ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self ι_eq_iff_rel CategoryTheory.GlueData.glue_condition_apply
instIsIsoT 📖	mathematical	—	CategoryTheory.IsIso TopCat TopCat.instCategory CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier MkCore.U TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.toTopCat MkCore.V MkCore.t	—	TopCat.ext MkCore.t_inv
isOpen_iff 📖	mathematical	—	IsOpen TopCat.carrier CategoryTheory.GlueData.glued TopCat TopCat.instCategory toGlueData CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopCat.str CategoryTheory.GlueData.U Set.preimage DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.GlueData.ι	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.instSmallDiscrete CategoryTheory.Limits.Multicoequalizer.ι_sigmaπ CategoryTheory.Limits.Multicoequalizer.instHasCoequalizerFstSigmaMapSndSigmaMap Homeomorph.isOpen_preimage univLE_of_max TopCat.coequalizer_isOpen_iff TopCat.colimit_isOpen_iff
ofOpenSubsets_toGlueData_J 📖	mathematical	—	CategoryTheory.GlueData.J TopCat TopCat.instCategory toGlueData ofOpenSubsets	—	—
ofOpenSubsets_toGlueData_U 📖	mathematical	—	CategoryTheory.GlueData.U TopCat TopCat.instCategory toGlueData ofOpenSubsets CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.str TopCat.of Preorder.smallCategory TopCat.carrier PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.toTopCat	—	—
ofOpenSubsets_toGlueData_V 📖	mathematical	—	CategoryTheory.GlueData.V TopCat TopCat.instCategory toGlueData ofOpenSubsets CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier TopCat.str TopCat.of Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.toTopCat MkCore.U TopologicalSpace.Opens.map TopologicalSpace.Opens.inclusion' TopCat.ofHom SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype MkCore.J	—	—
ofOpenSubsets_toGlueData_f 📖	mathematical	—	CategoryTheory.GlueData.f TopCat TopCat.instCategory toGlueData ofOpenSubsets TopologicalSpace.Opens.inclusion' CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.str TopCat.of Preorder.smallCategory TopCat.carrier PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.toTopCat TopologicalSpace.Opens.map	—	—
ofOpenSubsets_toGlueData_t 📖	mathematical	—	CategoryTheory.GlueData.t TopCat TopCat.instCategory toGlueData ofOpenSubsets TopCat.ofHom TopCat.carrier CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.str TopCat.of Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.toTopCat SetLike.instMembership TopologicalSpace.Opens.instSetLike TopologicalSpace.Opens.map TopologicalSpace.Opens.inclusion' instTopologicalSpaceSubtype	—	—
open_image_open 📖	mathematical	—	IsOpen TopCat.carrier CategoryTheory.GlueData.glued TopCat TopCat.instCategory toGlueData CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopCat.str Set.image CategoryTheory.GlueData.U DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.GlueData.ι SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self isOpen_iff preimage_image_eq_image Topology.IsOpenEmbedding.isOpenMap f_open Continuous.isOpen_preimage ContinuousMap.continuous_toFun TopologicalSpace.Opens.isOpen
preimage_image_eq_image 📖	mathematical	—	Set.preimage TopCat.carrier CategoryTheory.GlueData.U TopCat TopCat.instCategory toGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.GlueData.ι Set.image CategoryTheory.GlueData.V CategoryTheory.GlueData.f CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GlueData.t	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self Set.ext Set.preimage_image_eq ι_injective Set.image_congr CategoryTheory.GlueData.glue_condition_apply Set.image_preimage_eq_inter_range Set.inter_eq_self_of_subset_left preimage_range Set.preimage_mono Set.image_subset_range
preimage_image_eq_image' 📖	mathematical	—	Set.preimage TopCat.carrier CategoryTheory.GlueData.U TopCat TopCat.instCategory toGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.GlueData.ι Set.image CategoryTheory.GlueData.V CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GlueData.t CategoryTheory.GlueData.f	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self TopCat.coe_comp Set.image_comp Set.eq_preimage_iff_image_eq CategoryTheory.isIso_iff_bijective CategoryTheory.Functor.map_isIso CategoryTheory.GlueData.t_isIso Set.preimage_preimage CategoryTheory.GlueData.t_inv_assoc preimage_image_eq_image
preimage_range 📖	mathematical	—	Set.preimage TopCat.carrier CategoryTheory.GlueData.U TopCat TopCat.instCategory toGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.GlueData.ι Set.range CategoryTheory.GlueData.V CategoryTheory.GlueData.f	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self Set.preimage_image_eq ι_injective Set.image_univ Set.image_comp TopCat.coe_comp image_inter Set.preimage_range_inter
range_fromOpenSubsetsGlue 📖	mathematical	—	Set.range TopCat.carrier TopCat.of CategoryTheory.GlueData.glued TopCat TopCat.instCategory toGlueData ofOpenSubsets CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier fromOpenSubsetsGlue Set.iUnion SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	—	Set.ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self ι_jointly_surjective ι_fromOpenSubsetsGlue_apply Set.subset_iUnion
rel_equiv 📖	mathematical	—	CategoryTheory.GlueData.J TopCat TopCat.instCategory toGlueData TopCat.carrier CategoryTheory.GlueData.U Rel	—	CategoryTheory.GlueData.f_id CategoryTheory.IsIso.inv_hom_id_apply CategoryTheory.GlueData.t_id CategoryTheory.GlueData.t_inv_apply CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits TopCat.topCat_hasLimits TopCat.pullbackIsoProdSubtype_inv_fst_apply TopCat.pullbackIsoProdSubtype_inv_snd_apply CategoryTheory.GlueData.f_hasPullback CategoryTheory.GlueData.t_fac_assoc CategoryTheory.Limits.pullback.condition CategoryTheory.Epi.left_cancellation CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.GlueData.t'_isIso CategoryTheory.GlueData.cocycle_assoc CategoryTheory.GlueData.t_inv_assoc CategoryTheory.congr_fun
ι_eq_iff_rel 📖	mathematical	—	DFunLike.coe CategoryTheory.GlueData.U TopCat TopCat.instCategory toGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopCat.carrier CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.GlueData.ι Rel	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.instSmallDiscrete univLE_of_max CategoryTheory.ConcreteCategory.congr_hom CategoryTheory.Iso.inv_hom_id Equivalence.eqvGen_iff InvImage.equivalence rel_equiv Relation.EqvGen.mono CategoryTheory.ConcreteCategory.bijective_of_isIso CategoryTheory.Iso.isIso_inv TopCat.sigmaIsoSigma_inv_apply CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.Limits.colimit.ι_desc_assoc TopCat.sigmaIsoSigma_hom_ι_apply eqvGen_of_π_eq CategoryTheory.GlueData.glue_condition_apply
ι_fromOpenSubsetsGlue 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.GlueData.U toGlueData ofOpenSubsets CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopCat.of CategoryTheory.GlueData.ι fromOpenSubsetsGlue TopologicalSpace.Opens.inclusion'	—	CategoryTheory.Limits.Multicoequalizer.π_desc CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self
ι_fromOpenSubsetsGlue_apply 📖	mathematical	—	DFunLike.coe ContinuousMap TopCat.carrier CategoryTheory.GlueData.glued TopCat TopCat.instCategory toGlueData ofOpenSubsets CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopCat.str TopCat.of ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat.instConcreteCategoryContinuousMapCarrier fromOpenSubsetsGlue CategoryTheory.GlueData.U CategoryTheory.GlueData.ι TopologicalSpace.Opens.inclusion'	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise ι_fromOpenSubsetsGlue
ι_injective 📖	mathematical	—	TopCat.carrier CategoryTheory.GlueData.U TopCat TopCat.instCategory toGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.GlueData.ι	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self ι_eq_iff_rel CategoryTheory.GlueData.t_id
ι_isOpenEmbedding 📖	mathematical	—	Topology.IsOpenEmbedding TopCat.carrier CategoryTheory.GlueData.U TopCat TopCat.instCategory toGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.GlueData.ι	—	Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self ContinuousMap.continuous_toFun ι_injective open_image_open
ι_jointly_surjective 📖	mathematical	—	CategoryTheory.GlueData.J TopCat TopCat.instCategory toGlueData TopCat.carrier CategoryTheory.GlueData.U DFunLike.coe CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.GlueData.ι	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.GlueData.ι_jointly_surjective CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint TopCat.instIsLeftAdjointForgetContinuousMapCarrier CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint TopCat.instIsRightAdjointForgetContinuousMapCarrier
ι_mono 📖	mathematical	—	CategoryTheory.Mono TopCat TopCat.instCategory CategoryTheory.GlueData.U toGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram CategoryTheory.GlueData.ι	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self TopCat.mono_iff_injective ι_injective
π_surjective 📖	mathematical	—	TopCat.carrier CategoryTheory.GlueData.sigmaOpens TopCat TopCat.instCategory toGlueData CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.GlueData.J CategoryTheory.discreteCategory CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize TopCat.topCat_hasColimits CategoryTheory.Discrete.functor CategoryTheory.GlueData.U CategoryTheory.GlueData.glued CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.GlueData.π	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize TopCat.topCat_hasColimits TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self TopCat.epi_iff_surjective CategoryTheory.GlueData.π_epi

TopCat.GlueData.MkCore

Definitions

Name	Category	Theorems
J 📖	CompOp	1 math math: TopCat.GlueData.ofOpenSubsets_toGlueData_V
U 📖	CompOp	7 math math: V_id, TopCat.GlueData.instIsIsoT, t_inv, t_id, TopCat.GlueData.ofOpenSubsets_toGlueData_V, t_inter, cocycle
V 📖	CompOp	6 math math: V_id, TopCat.GlueData.instIsIsoT, t_inv, t_id, t_inter, cocycle
t 📖	CompOp	5 math math: TopCat.GlueData.instIsIsoT, t_inv, t_id, t_inter, cocycle
t' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
V_id 📖	mathematical	—	V Top.top TopologicalSpace.Opens TopCat.carrier U TopCat.str OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
cocycle 📖	mathematical	TopCat.carrier U TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike V	TopCat.carrier U TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike V DFunLike.coe CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier t t_inter	—	—
t_id 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier U TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat V CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier t	—	—
t_inter 📖	mathematical	TopCat.carrier U TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike V	TopCat.carrier U TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike V DFunLike.coe CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier t	—	—
t_inv 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier U TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat V CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier t	—	t_inter V_id cocycle t_id

---

← Back to Index