Basic

📁 Source: Mathlib/CategoryTheory/Subfunctor/Basic.lean

Statistics

Metric	Count
Definitions Subfunctor, homOfLe, toFunctor, toPresheaf, ι, homOfLe, instCoeHeadObjToFunctor, obj, toFunctor, ι, Subpresheaf, instCompleteLatticeSubfunctor, instPartialOrderSubfunctor	13
Theorems bot_obj, eq_top_iff_isIso, homOfLe_ι, iInf_obj, iSup_min, iSup_obj, le_def, max_min, max_obj, min_obj, nat_trans_naturality, sInf_obj, sSup_obj, toPresheaf_map_coe, toPresheaf_obj, top_obj, bot_obj, eq_top_iff_isIso, ext, ext_iff, homOfLe_app_coe, homOfLe_ι, homOfLe_ι_assoc, iInf_obj, iSup_min, iSup_obj, instIsIsoFunctorTypeιTop, instMonoFunctorTypeHomOfLe, instMonoFunctorTypeι, instNonempty, le_def, map, max_min, max_obj, min_obj, nat_trans_naturality, sInf_obj, sSup_obj, toFunctor_map_coe, toFunctor_obj, top_obj, ι_app	42
Total	55

CategoryTheory

Definitions

Name	Category	Theorems
Subfunctor 📖	CompData	69 math math: Subfunctor.Subpresheaf.equalizer_le, Subfunctor.Subpresheaf.max_obj, Subfunctor.instNonempty, Subfunctor.range_le_equalizer_iff, Subfunctor.range_toRange, Subfunctor.Subpresheaf.preimage_eq_top_iff, Subfunctor.Subpresheaf.iSup_obj, Subfunctor.Subpresheaf.min_obj, Subfunctor.max_obj, Subfunctor.max_min, Subfunctor.Subpresheaf.image_le_iff, Subfunctor.isGeneratedBy_iff, Subfunctor.Subpresheaf.isGeneratedBy_iff, Subfunctor.IsGeneratedBy.ofSection_le, Subfunctor.image_le_iff, Subfunctor.sSup_obj, Subfunctor.equivalenceMonoOver_inverse_map, Subfunctor.range_eq_top, Subfunctor.equivalenceMonoOver_functor_map, Subfunctor.Subpresheaf.image_top, Subfunctor.le_sheafify, Subfunctor.Subpresheaf.bot_obj, Subfunctor.equivalenceMonoOver_inverse_obj, Subfunctor.eq_top_iff_isIso, Subfunctor.Subpresheaf.le_def, Subfunctor.iSup_min, Subfunctor.equalizer_le, Presheaf.isLocallySurjective_iff_range_sheafify_eq_top, Subfunctor.equivalenceMonoOver_functor_obj, Subfunctor.min_obj, Subfunctor.orderIsoSubobject_apply, Presheaf.isLocallySurjective_iff_range_sheafify_eq_top', Subfunctor.Subpresheaf.epi_iff_range_eq_top, Subfunctor.IsGeneratedBy.iSup_eq, Subfunctor.le_def, Subfunctor.Subpresheaf.iInf_obj, Subfunctor.Subpresheaf.top_obj, Subfunctor.Subpresheaf.range_le_equalizer_iff, Subfunctor.sInf_obj, Subfunctor.Subpresheaf.range_id, Subfunctor.instIsIsoFunctorTypeιTop, Subfunctor.bot_obj, Subfunctor.Subpresheaf.iSup_min, Subfunctor.image_top, Subfunctor.equivalenceMonoOver_unitIso, Subfunctor.Subpresheaf.sInf_obj, Subfunctor.orderIsoSubobject_symm_apply, Subfunctor.image_iSup, Subfunctor.ofSection_le_iff, Subfunctor.Subpresheaf.sSup_obj, Subfunctor.iInf_obj, Subfunctor.Subpresheaf.ofSection_le_iff, Subfunctor.top_obj, Subpresheaf.le_sheafify, Subfunctor.Subpresheaf.range_comp_le, Subfunctor.iSup_obj, Subfunctor.Subpresheaf.image_iSup, Subfunctor.Subpresheaf.max_min, presheafIsGeneratedBy_of_isFinite, Subfunctor.preimage_eq_top_iff, Subfunctor.Subpresheaf.eq_top_iff_isIso, Subfunctor.Subpresheaf.IsGeneratedBy.ofSection_le, Subfunctor.epi_iff_range_eq_top, Subfunctor.Subpresheaf.IsGeneratedBy.iSup_eq, Subfunctor.Subpresheaf.range_eq_top, Subfunctor.range_id, Subfunctor.range_comp_le, Subfunctor.equivalenceMonoOver_counitIso, Subfunctor.Subpresheaf.range_toRange
Subpresheaf 📖	CompOp	—
instCompleteLatticeSubfunctor 📖	CompOp	95 math math: SSet.Subcomplex.preimage_eq_top_iff, SSet.horn₃₁.desc.multicofork_π_two, SSet.iSup_subcomplexOfSimplex_prod_eq_top, Subfunctor.Subpresheaf.max_obj, SSet.finite_iSup_iff, SSet.Subcomplex.range_eq_top, Subfunctor.range_toRange, SSet.horn₃₂.desc.multicofork_π_one, SSet.Subcomplex.topIso_inv_app_coe, Subfunctor.Subpresheaf.preimage_eq_top_iff, Subfunctor.Subpresheaf.iSup_obj, SSet.iSup_skeleton, Subfunctor.Subpresheaf.min_obj, SSet.Subcomplex.preimage_min, SSet.Subcomplex.eq_top_iff_of_hasDimensionLT, Subfunctor.max_obj, SSet.Subcomplex.topIso_inv_ι, SSet.horn₃₁.desc.multicofork_pt, Subfunctor.max_min, SSet.hasDimensionLT_subcomplex_top_iff, SSet.Subcomplex.instSubsingletonHomToSSetBot, Subfunctor.isGeneratedBy_iff, Subfunctor.Subpresheaf.isGeneratedBy_iff, Subfunctor.sSup_obj, SSet.Subcomplex.eq_top_iff_contains_nonDegenerate, SSet.Subcomplex.preimage_range, Subfunctor.range_eq_top, Subfunctor.Subpresheaf.image_top, SSet.horn₃₁.desc.multicofork_π_two_assoc, SSet.horn₃₁.desc.multicofork_π_zero_assoc, SSet.instHasDimensionLTToSSetBotSubcomplex, Subfunctor.Subpresheaf.bot_obj, Subfunctor.eq_top_iff_isIso, Subfunctor.iSup_min, SSet.skeleton_succ, SSet.Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top, Presheaf.isLocallySurjective_iff_range_sheafify_eq_top, Subfunctor.min_obj, Presheaf.isLocallySurjective_iff_range_sheafify_eq_top', Subfunctor.Subpresheaf.epi_iff_range_eq_top, SSet.Subcomplex.image_top, Subfunctor.IsGeneratedBy.iSup_eq, Subfunctor.Subpresheaf.iInf_obj, Subfunctor.Subpresheaf.top_obj, Subfunctor.sInf_obj, Subfunctor.Subpresheaf.range_id, Subfunctor.instIsIsoFunctorTypeιTop, Subfunctor.bot_obj, SSet.Subcomplex.topIso_inv_ι_assoc, SSet.horn_eq_iSup, SSet.range_eq_iSup_sigma_ι, SSet.Subcomplex.BicartSq.isPushout, SSet.horn₃₂.desc.multicofork_π_zero_assoc, Subfunctor.Subpresheaf.iSup_min, Subfunctor.image_top, SSet.hasDimensionLT_iSup_iff, SSet.iSup_skeletonOfMono, SSet.iSup_range_eq_top_of_isColimit, SSet.horn₃₁.desc.multicofork_π_three_assoc, SSet.horn₃₁.desc.multicofork_π_zero, SSet.finite_subcomplex_top_iff, SSet.Subcomplex.preimage_max, Subfunctor.Subpresheaf.sInf_obj, SSet.horn₃₂.desc.multicofork_π_three, Subfunctor.image_iSup, Subfunctor.Subpresheaf.sSup_obj, Subfunctor.iInf_obj, SSet.boundary_eq_iSup, Subfunctor.top_obj, SSet.stdSimplex.face_inter_face, SSet.horn₃₂.desc.multicofork_pt, Subfunctor.iSup_obj, SSet.Subcomplex.range_eq_top_iff, SSet.Subcomplex.preimage_iSup, SSet.N.iSup_subcomplex_eq_top, Subfunctor.Subpresheaf.image_iSup, SSet.Subcomplex.topIso_hom, Subfunctor.Subpresheaf.max_min, presheafIsGeneratedBy_of_isFinite, SSet.horn₃₂.desc.multicofork_π_zero, SSet.horn₃₂.desc.multicofork_π_three_assoc, SSet.horn₃₂.desc.multicofork_π_one_assoc, Subfunctor.preimage_eq_top_iff, Subfunctor.Subpresheaf.eq_top_iff_isIso, SSet.horn₃₁.desc.multicofork_π_three, Subfunctor.epi_iff_range_eq_top, Subfunctor.Subpresheaf.IsGeneratedBy.iSup_eq, Subfunctor.Subpresheaf.range_eq_top, SSet.Subcomplex.image_iSup, Subfunctor.range_id, Subfunctor.Subpresheaf.range_toRange, SSet.range_eq_iSup_of_isColimit, SSet.Subcomplex.preimage_iInf, SSet.skeletonOfMono_succ, SSet.skeleton_zero
instPartialOrderSubfunctor 📖	CompOp	56 math math: SSet.RelativeMorphism.image_le, SSet.Subcomplex.preimage_eq_top_iff, Subfunctor.Subpresheaf.equalizer_le, SSet.ofSimplex_le_skeleton, SSet.Subcomplex.toSSetFunctor_map, Subfunctor.range_le_equalizer_iff, Subfunctor.Subpresheaf.preimage_eq_top_iff, SSet.iSup_skeleton, SSet.skeleton_le_skeletonOfMono, Subfunctor.Subpresheaf.image_le_iff, SSet.Subcomplex.toSSetFunctor_obj, Subfunctor.IsGeneratedBy.ofSection_le, Subfunctor.image_le_iff, Subfunctor.equivalenceMonoOver_inverse_map, SSet.Subcomplex.image_le_iff, Subfunctor.equivalenceMonoOver_functor_map, SSet.Subcomplex.image_monotone, SSet.skeleton_obj_eq_top, SSet.RelativeMorphism.le_preimage, Subfunctor.le_sheafify, Subfunctor.equivalenceMonoOver_inverse_obj, SSet.mem_skeleton_obj_iff_of_nonDegenerate, Subfunctor.Subpresheaf.le_def, Subfunctor.equalizer_le, SSet.skeleton_succ, Subfunctor.equivalenceMonoOver_functor_obj, Subfunctor.orderIsoSubobject_apply, SSet.orderEmbeddingN_apply, Subfunctor.le_def, SSet.face_le_horn, SSet.Subcomplex.image_preimage_le, Subfunctor.Subpresheaf.range_le_equalizer_iff, SSet.Subcomplex.ofSimplex_le_iff, SSet.Subcomplex.le_iff_of_hasDimensionLT, SSet.skeletonOfMono_zero, SSet.Subcomplex.le_iff_contains_nonDegenerate, SSet.mem_skeleton, SSet.iSup_skeletonOfMono, SSet.skeletonOfMono_obj_eq_top, Subfunctor.equivalenceMonoOver_unitIso, SSet.Subcomplex.image_le_range, SSet.mem_skeletonOfMono_obj_iff_of_nonDegenerate, Subfunctor.orderIsoSubobject_symm_apply, SSet.N.le_iff, Subfunctor.ofSection_le_iff, Subfunctor.Subpresheaf.ofSection_le_iff, Subpresheaf.le_sheafify, Subfunctor.Subpresheaf.range_comp_le, SSet.stdSimplex.face_le_face_iff, Subfunctor.preimage_eq_top_iff, Subfunctor.Subpresheaf.IsGeneratedBy.ofSection_le, Subfunctor.range_comp_le, Subfunctor.equivalenceMonoOver_counitIso, SSet.S.le_def, SSet.skeletonOfMono_succ, SSet.skeleton_zero

CategoryTheory.Subfunctor

Definitions

Name	Category	Theorems
homOfLe 📖	CompOp	10 math math: homOfLe_app_coe, equivalenceMonoOver_functor_map, homOfLe_ι_assoc, homOfLe_ι, Subpresheaf.homOfLe_ι, instMonoFunctorTypeHomOfLe, equivalenceMonoOver_unitIso, to_sheafifyLift, CategoryTheory.Subpresheaf.to_sheafifyLift, equivalenceMonoOver_counitIso
instCoeHeadObjToFunctor 📖	CompOp	—
obj 📖	CompOp	102 math math: SSet.Subcomplex.mem_ofSimplex_obj_iff, Subpresheaf.toPresheaf_obj, Subpresheaf.max_obj, toFunctor_obj, SSet.Subcomplex.image_obj, SSet.Subcomplex.topIso_inv_app_coe, SSet.Subcomplex.toRange_app_val, SSet.Subcomplex.lift_app_coe, Subpresheaf.iSup_obj, SSet.Subcomplex.degenerate_eq_top_iff, homOfLe_app_coe, Subpresheaf.min_obj, SSet.Subcomplex.eq_top_iff_of_hasDimensionLT, max_obj, nat_trans_naturality, SSet.PtSimplex.RelStruct.δ_castSucc_map, sSup_obj, SSet.Subcomplex.eq_top_iff_contains_nonDegenerate, SSet.PtSimplex.RelStruct.δ_castSucc_map_assoc, SSet.PtSimplex.MulStruct.δ_succ_succ_map_assoc, ofSection_obj, SSet.RelativeMorphism.ofSimplex₀_map, SSet.Subcomplex.toImage_app_coe, SSet.PtSimplex.MulStruct.δ_succ_succ_map, Subpresheaf.mem_ofSection_obj, SSet.horn_obj, SSet.skeleton_obj_eq_top, SSet.Subcomplex.yonedaEquiv_coe, SSet.stdSimplex.face_obj, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map, Subpresheaf.mem_equalizer_iff, SSet.Subcomplex.mem_nonDegenerate_iff, Subpresheaf.bot_obj, SSet.mem_skeleton_obj_iff_of_nonDegenerate, Subpresheaf.IsGeneratedBy.mem, SSet.stdSimplex.mem_face_iff, preimage_obj, Subpresheaf.le_def, SSet.horn.edge_coe, SSet.Subcomplex.mem_degenerate_iff, min_obj, SSet.Subcomplex.prod_obj, map, SSet.Subcomplex.preimage_obj, le_def, Subpresheaf.iInf_obj, Subpresheaf.top_obj, isSheaf_iff, sInf_obj, mem_equalizer_iff, SSet.Subcomplex.ofSimplex_le_iff, SSet.Subcomplex.le_iff_of_hasDimensionLT, bot_obj, SSet.horn.edge₃_coe_down, SSet.Subcomplex.fromPreimage_app_coe, SSet.Subcomplex.homOfLE_app_val, SSet.stdSimplex.obj₀Equiv_symm_mem_face_iff, range_obj, toFunctor_map_coe, Subpresheaf.nat_trans_naturality, SSet.Subcomplex.le_iff_contains_nonDegenerate, SSet.horn_obj_zero, SSet.mem_skeleton, SSet.horn.spineId_vertex_coe, toRange_app_val, SSet.horn.spineId_arrow_coe, SSet.skeletonOfMono_obj_eq_top, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc, mem_ofSection_obj, SSet.Subcomplex.mem_ofSimplex_obj, Subpresheaf.sInf_obj, SSet.mem_skeletonOfMono_obj_iff_of_nonDegenerate, SSet.Subcomplex.PairingCore.notMem₁, image_obj, Subpresheaf.toRange_app_val, toRangeSheafify_app_coe, ofSection_le_iff, Subpresheaf.sSup_obj, iInf_obj, ι_app, CategoryTheory.Subpresheaf.isSheaf_iff, Subpresheaf.ofSection_le_iff, top_obj, CategoryTheory.FunctorToTypes.mem_fromOverSubfunctor_iff, IsGeneratedBy.mem, SSet.horn.primitiveEdge_coe_down, iSup_obj, Subpresheaf.toPresheaf_map_coe, SSet.PtSimplex.RelStruct.δ_succ_map, SSet.Subcomplex.PairingCore.notMem₂, ext_iff, equalizer_obj, sieveOfSection_apply, SSet.RelativeMorphism.map_coe, SSet.Subcomplex.N.notMem, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map_assoc, SSet.horn.const_val_apply, SSet.horn.primitiveTriangle_coe, lift_app_coe, SSet.skeletonOfMono_succ, SSet.PtSimplex.RelStruct.δ_succ_map_assoc, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map
toFunctor 📖	CompOp	76 math math: isSeparated, Subpresheaf.toPresheaf_obj, Subpresheaf.equalizer.fork_ι, Subpresheaf.equalizer.condition, toFunctor_obj, range_le_equalizer_iff, range_toRange, homOfLe_app_coe, nat_trans_naturality, range_ι, CategoryTheory.Subpresheaf.isSeparated, equalizer.ι_ι_assoc, equivalenceMonoOver_functor_map, homOfLe_ι_assoc, homOfLe_ι, SSet.Subcomplex.yonedaEquiv_coe, Subpresheaf.mem_equalizer_iff, lift_ι, eq_top_iff_isIso, Subpresheaf.toRange_ι, equivalenceMonoOver_functor_obj, orderIsoSubobject_apply, instEpiFunctorTypeToRange, Subpresheaf.range_ι, Subpresheaf.range_le_equalizer_iff, isSheaf_iff, mem_equalizer_iff, lift_ι_assoc, toRange_ι_assoc, Subpresheaf.homOfLe_ι, instIsIsoFunctorTypeιTop, instIsIsoFunctorTypeToRangeOfMono, sheafify_isSheaf, toFunctor_map_coe, equalizer.condition, Subpresheaf.nat_trans_naturality, fromPreimage_ι, instMonoFunctorTypeHomOfLe, toRange_app_val, equivalenceMonoOver_unitIso, CategoryTheory.Subpresheaf.sheafify_isSheaf, CategoryTheory.Presheaf.instIsLocallySurjectiveHomToRangeSheafify, instMonoFunctorTypeι_1, equalizer.fork_pt, range_subobjectMk_ι, Subpresheaf.fromPreimage_ι, Subpresheaf.toRange_app_val, toRangeSheafify_app_coe, fromPreimage_ι_assoc, ι_app, CategoryTheory.Subpresheaf.isSheaf_iff, Subpresheaf.family_of_elements_compatible, CategoryTheory.Subpresheaf.eq_sheafify_iff, Subpresheaf.subobjectMk_range_arrow, Subpresheaf.toPresheaf_map_coe, Subpresheaf.equalizer.ι_ι, to_sheafifyLift, Subpresheaf.range_subobjectMk_ι, CategoryTheory.FunctorToTypes.monoFactorisation_I, instMonoFunctorTypeι, CategoryTheory.Presheaf.instIsLocallyInjectiveHomιOpposite, equalizer.condition_assoc, family_of_elements_compatible, equalizer_obj, Subpresheaf.eq_top_iff_isIso, equalizer.ι_ι, equalizer.fork_ι, CategoryTheory.Subpresheaf.to_sheafifyLift, eq_sheafify_iff, lift_app_coe, equivalenceMonoOver_counitIso, Subpresheaf.range_toRange, subobjectMk_range_arrow, Subpresheaf.lift_ι, toRange_ι, CategoryTheory.Sheaf.image_val
ι 📖	CompOp	41 math math: range_le_equalizer_iff, equalizer.lift_ι', SSet.Subcomplex.topIso_inv_ι, CategoryTheory.Sheaf.imageι_val, range_ι, equalizer.ι_ι_assoc, equalizer.lift_ι'_assoc, equivalenceMonoOver_functor_map, homOfLe_ι_assoc, homOfLe_ι, lift_ι, eq_top_iff_isIso, Subpresheaf.toRange_ι, equivalenceMonoOver_functor_obj, orderIsoSubobject_apply, Subpresheaf.range_ι, Subpresheaf.range_le_equalizer_iff, lift_ι_assoc, toRange_ι_assoc, Subpresheaf.homOfLe_ι, instIsIsoFunctorTypeιTop, SSet.Subcomplex.topIso_inv_ι_assoc, fromPreimage_ι, equivalenceMonoOver_unitIso, range_subobjectMk_ι, Subpresheaf.fromPreimage_ι, fromPreimage_ι_assoc, ι_app, Subpresheaf.subobjectMk_range_arrow, Subpresheaf.equalizer.ι_ι, Subpresheaf.range_subobjectMk_ι, CategoryTheory.FunctorToTypes.monoFactorisation_m, instMonoFunctorTypeι, CategoryTheory.Presheaf.instIsLocallyInjectiveHomιOpposite, Subpresheaf.eq_top_iff_isIso, equalizer.ι_ι, equivalenceMonoOver_counitIso, Subpresheaf.equalizer.lift_ι', subobjectMk_range_arrow, Subpresheaf.lift_ι, toRange_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_obj 📖	mathematical	—	obj Bot.bot CategoryTheory.Subfunctor OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Set CategoryTheory.Functor.obj CategoryTheory.types BooleanAlgebra.toBot Set.instBooleanAlgebra	—	—
eq_top_iff_isIso 📖	mathematical	—	Top.top CategoryTheory.Subfunctor OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category toFunctor ι	—	instIsIsoFunctorTypeιTop ext Set.ext CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.IsIso.inv_hom_id_apply
ext 📖	—	obj	—	—	—
ext_iff 📖	mathematical	—	obj	—	ext
homOfLe_app_coe 📖	mathematical	CategoryTheory.Subfunctor Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor	CategoryTheory.Functor.obj CategoryTheory.types Set Set.instMembership obj CategoryTheory.NatTrans.app toFunctor homOfLe	—	—
homOfLe_ι 📖	mathematical	CategoryTheory.Subfunctor Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category toFunctor homOfLe ι	—	CategoryTheory.NatTrans.ext' CategoryTheory.types_ext
homOfLe_ι_assoc 📖	mathematical	CategoryTheory.Subfunctor Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category toFunctor homOfLe ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homOfLe_ι
iInf_obj 📖	mathematical	—	obj iInf CategoryTheory.Subfunctor CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Set.iInter CategoryTheory.Functor.obj CategoryTheory.types	—	Set.sInter_image Set.iInter_congr_Prop Set.iInter_exists Set.iInter_iInter_eq'
iSup_min 📖	mathematical	—	CategoryTheory.Subfunctor SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup	—	ext Set.ext iSup_obj
iSup_obj 📖	mathematical	—	obj iSup CategoryTheory.Subfunctor CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup CategoryTheory.instCompleteLatticeSubfunctor Set.iUnion CategoryTheory.Functor.obj CategoryTheory.types	—	Set.sUnion_image Set.iUnion_congr_Prop Set.iUnion_exists Set.iUnion_iUnion_eq'
instIsIsoFunctorTypeιTop 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category toFunctor Top.top CategoryTheory.Subfunctor OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder ι	—	CategoryTheory.NatIso.isIso_of_isIso_app CategoryTheory.isIso_iff_bijective Subtype.coe_injective
instMonoFunctorTypeHomOfLe 📖	mathematical	CategoryTheory.Subfunctor Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor	CategoryTheory.Mono CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category toFunctor homOfLe	—	CategoryTheory.NatTrans.ext CategoryTheory.congr_app
instMonoFunctorTypeι 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category toFunctor ι	—	CategoryTheory.NatTrans.ext CategoryTheory.congr_app
instNonempty 📖	mathematical	—	CategoryTheory.Subfunctor	—	bot_nonempty
le_def 📖	mathematical	—	CategoryTheory.Subfunctor Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Set CategoryTheory.Functor.obj CategoryTheory.types Set.instLE obj	—	—
map 📖	mathematical	—	Set CategoryTheory.Functor.obj CategoryTheory.types Set.instHasSubset obj Set.preimage CategoryTheory.Functor.map	—	—
max_min 📖	mathematical	—	CategoryTheory.Subfunctor SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor SemilatticeSup.toMax Lattice.toSemilatticeSup	—	ext Set.ext
max_obj 📖	mathematical	—	obj CategoryTheory.Subfunctor SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor Set CategoryTheory.Functor.obj CategoryTheory.types Set.instUnion	—	—
min_obj 📖	mathematical	—	obj CategoryTheory.Subfunctor SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor Set CategoryTheory.Functor.obj CategoryTheory.types Set.instInter	—	—
nat_trans_naturality 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types Set Set.instMembership obj CategoryTheory.NatTrans.app toFunctor CategoryTheory.Functor.map	—	CategoryTheory.FunctorToTypes.naturality
sInf_obj 📖	mathematical	—	obj InfSet.sInf CategoryTheory.Subfunctor CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Set CategoryTheory.Functor.obj CategoryTheory.types Set.instInfSet Set.image	—	—
sSup_obj 📖	mathematical	—	obj SupSet.sSup CategoryTheory.Subfunctor CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup CategoryTheory.instCompleteLatticeSubfunctor Set CategoryTheory.Functor.obj CategoryTheory.types Set.instSupSet Set.image	—	—
toFunctor_map_coe 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types Set Set.instMembership obj CategoryTheory.Functor.map toFunctor	—	—
toFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types toFunctor Set.Elem obj	—	—
top_obj 📖	mathematical	—	obj Top.top CategoryTheory.Subfunctor OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set CategoryTheory.Functor.obj CategoryTheory.types BooleanAlgebra.toTop Set.instBooleanAlgebra	—	—
ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.types toFunctor ι CategoryTheory.Functor.obj Set Set.instMembership obj	—	—

CategoryTheory.Subfunctor.Subpresheaf

Definitions

Name	Category	Theorems
homOfLe 📖	CompOp	—
toFunctor 📖	CompOp	—
toPresheaf 📖	CompOp	—
ι 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_obj 📖	mathematical	—	CategoryTheory.Subfunctor.obj Bot.bot CategoryTheory.Subfunctor OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Set CategoryTheory.Functor.obj CategoryTheory.types BooleanAlgebra.toBot Set.instBooleanAlgebra	—	CategoryTheory.Subfunctor.bot_obj
eq_top_iff_isIso 📖	mathematical	—	Top.top CategoryTheory.Subfunctor OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor CategoryTheory.Subfunctor.ι	—	CategoryTheory.Subfunctor.eq_top_iff_isIso
homOfLe_ι 📖	mathematical	CategoryTheory.Subfunctor Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor CategoryTheory.Subfunctor.homOfLe CategoryTheory.Subfunctor.ι	—	CategoryTheory.Subfunctor.homOfLe_ι
iInf_obj 📖	mathematical	—	CategoryTheory.Subfunctor.obj iInf CategoryTheory.Subfunctor CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Set.iInter CategoryTheory.Functor.obj CategoryTheory.types	—	CategoryTheory.Subfunctor.iInf_obj
iSup_min 📖	mathematical	—	CategoryTheory.Subfunctor SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup	—	CategoryTheory.Subfunctor.iSup_min
iSup_obj 📖	mathematical	—	CategoryTheory.Subfunctor.obj iSup CategoryTheory.Subfunctor CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup CategoryTheory.instCompleteLatticeSubfunctor Set.iUnion CategoryTheory.Functor.obj CategoryTheory.types	—	CategoryTheory.Subfunctor.iSup_obj
le_def 📖	mathematical	—	CategoryTheory.Subfunctor Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Set CategoryTheory.Functor.obj CategoryTheory.types Set.instLE CategoryTheory.Subfunctor.obj	—	CategoryTheory.Subfunctor.le_def
max_min 📖	mathematical	—	CategoryTheory.Subfunctor SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor SemilatticeSup.toMax Lattice.toSemilatticeSup	—	CategoryTheory.Subfunctor.max_min
max_obj 📖	mathematical	—	CategoryTheory.Subfunctor.obj CategoryTheory.Subfunctor SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor Set CategoryTheory.Functor.obj CategoryTheory.types Set.instUnion	—	CategoryTheory.Subfunctor.max_obj
min_obj 📖	mathematical	—	CategoryTheory.Subfunctor.obj CategoryTheory.Subfunctor SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor Set CategoryTheory.Functor.obj CategoryTheory.types Set.instInter	—	CategoryTheory.Subfunctor.min_obj
nat_trans_naturality 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types Set Set.instMembership CategoryTheory.Subfunctor.obj CategoryTheory.NatTrans.app CategoryTheory.Subfunctor.toFunctor CategoryTheory.Functor.map	—	CategoryTheory.Subfunctor.nat_trans_naturality
sInf_obj 📖	mathematical	—	CategoryTheory.Subfunctor.obj InfSet.sInf CategoryTheory.Subfunctor CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Set CategoryTheory.Functor.obj CategoryTheory.types Set.instInfSet Set.image	—	CategoryTheory.Subfunctor.sInf_obj
sSup_obj 📖	mathematical	—	CategoryTheory.Subfunctor.obj SupSet.sSup CategoryTheory.Subfunctor CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup CategoryTheory.instCompleteLatticeSubfunctor Set CategoryTheory.Functor.obj CategoryTheory.types Set.instSupSet Set.image	—	CategoryTheory.Subfunctor.sSup_obj
toPresheaf_map_coe 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types Set Set.instMembership CategoryTheory.Subfunctor.obj CategoryTheory.Functor.map CategoryTheory.Subfunctor.toFunctor	—	CategoryTheory.Subfunctor.toFunctor_map_coe
toPresheaf_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Subfunctor.toFunctor Set.Elem CategoryTheory.Subfunctor.obj	—	CategoryTheory.Subfunctor.toFunctor_obj
top_obj 📖	mathematical	—	CategoryTheory.Subfunctor.obj Top.top CategoryTheory.Subfunctor OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set CategoryTheory.Functor.obj CategoryTheory.types BooleanAlgebra.toTop Set.instBooleanAlgebra	—	CategoryTheory.Subfunctor.top_obj

---

← Back to Index