Ind

📁 Source: Mathlib/CategoryTheory/MorphismProperty/Ind.lean

Statistics

Metric	Count
Definitions PreIndSpreads, ind	2
Theorems ind_of_preIndSpreads, ind_of_preIndSpreads, exists_isPushout, exists_hom_of_isFinitelyPresentable, exists_isPushout_of_isFiltered, ind_iff_exists, ind_iff_ind_underMk, ind_ind, ind_underObj_pushout, instContainsIdentitiesInd, instIsStableUnderCobaseChangeIndOfHasPushouts, instRespectsIsoInd, instRespectsLeftInd, le_ind, underObj_ind_eq_ind_underObj	15
Total	17

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
PreIndSpreads 📖	CompData	—
ind 📖	CompOp	11 math math: instRespectsIsoInd, ind_iff_ind_underMk, le_ind, instRespectsLeftInd, IsMultiplicative.ind_of_preIndSpreads, ind_ind, instIsStableUnderCobaseChangeIndOfHasPushouts, underObj_ind_eq_ind_underObj, ind_iff_exists, instContainsIdentitiesInd, IsStableUnderComposition.ind_of_preIndSpreads

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_hom_of_isFinitelyPresentable 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	—	CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit_under
exists_isPushout_of_isFiltered 📖	mathematical	CategoryTheory.Limits.Cocone.pt	CategoryTheory.IsPushout CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	PreIndSpreads.exists_isPushout
ind_iff_exists 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra isFinitelyPresentable	ind CategoryTheory.CategoryStruct.comp	—	ind_iff_ind_underMk CategoryTheory.ObjectProperty.ind_iff_exists CategoryTheory.Under.w CategoryTheory.Category.assoc CategoryTheory.Under.UnderMorphism.ext
ind_iff_ind_underMk 📖	mathematical	—	ind CategoryTheory.ObjectProperty.ind CategoryTheory.Under CategoryTheory.instCategoryUnder underObj	—	CategoryTheory.Category.comp_id CategoryTheory.Under.UnderMorphism.ext CategoryTheory.NatTrans.naturality CategoryTheory.IsFiltered.nonempty CategoryTheory.Category.id_comp CategoryTheory.Under.w CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.Limits.instPreservesFilteredColimitsOfSizeUnderForget
ind_ind 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra isFinitelyPresentable	ind	—	le_antisymm underObj_ind_eq_ind_underObj CategoryTheory.ObjectProperty.ind_ind CategoryTheory.Under.locallySmall le_ind
ind_underObj_pushout 📖	mathematical	CategoryTheory.ObjectProperty.ind CategoryTheory.Under CategoryTheory.instCategoryUnder underObj	CategoryTheory.Functor.obj CategoryTheory.Under.pushout CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Under.pushoutIsLeftAdjoint pushout_inr
instContainsIdentitiesInd 📖	mathematical	—	ContainsIdentities ind	—	le_ind id_mem
instIsStableUnderCobaseChangeIndOfHasPushouts 📖	mathematical	—	IsStableUnderCobaseChange ind	—	IsStableUnderCobaseChange.mk' instRespectsIsoInd IsStableUnderCobaseChange.respectsIso ind_iff_ind_underMk ind_underObj_pushout
instRespectsIsoInd 📖	mathematical	—	RespectsIso ind	—	instRespectsLeftInd Respects.toRespectsLeft CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
instRespectsLeftInd 📖	mathematical	—	RespectsLeft CategoryTheory.Category.toCategoryStruct ind	—	RespectsLeft.precomp CategoryTheory.Category.assoc
le_ind 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra ind	—	CategoryTheory.isFiltered_of_directed_le_nonempty OrderTop.instIsDirectedOrder CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.isConnected_of_nonempty_and_subsingleton
underObj_ind_eq_ind_underObj 📖	mathematical	—	underObj ind CategoryTheory.ObjectProperty.ind CategoryTheory.Under CategoryTheory.instCategoryUnder	—	—

CategoryTheory.MorphismProperty.IsMultiplicative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ind_of_preIndSpreads 📖	mathematical	CategoryTheory.IsFinitelyAccessibleCategory CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.isFinitelyPresentable	CategoryTheory.MorphismProperty.IsMultiplicative CategoryTheory.MorphismProperty.ind	—	CategoryTheory.MorphismProperty.IsStableUnderComposition.ind_of_preIndSpreads toIsStableUnderComposition CategoryTheory.MorphismProperty.instContainsIdentitiesInd toContainsIdentities

CategoryTheory.MorphismProperty.IsStableUnderComposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ind_of_preIndSpreads 📖	mathematical	CategoryTheory.IsFinitelyAccessibleCategory CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.isFinitelyPresentable	CategoryTheory.MorphismProperty.IsStableUnderComposition CategoryTheory.MorphismProperty.ind	—	CategoryTheory.MorphismProperty.ind_iff_exists CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit_under CategoryTheory.Category.assoc CategoryTheory.MorphismProperty.exists_isPushout_of_isFiltered CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Iso.isIso_inv CategoryTheory.Under.final_forget CategoryTheory.IsFiltered.toIsFilteredOrEmpty CategoryTheory.Limits.comp_preservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Under.pushoutIsLeftAdjoint CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.Limits.instPreservesFilteredColimitsOfSizeUnderForget CategoryTheory.IsFiltered.under CategoryTheory.NatTrans.naturality CategoryTheory.Category.id_comp CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.colimit.ι_desc_assoc CategoryTheory.IsPushout.inl_isoPushout_inv Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.pushout_inl

CategoryTheory.MorphismProperty.PreIndSpreads

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isPushout 📖	mathematical	CategoryTheory.Limits.Cocone.pt	CategoryTheory.IsPushout CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	—

---

← Back to Index