Theorems · Inductive type · category theory
CategoryTheory.MorphismProperty.multiplicativeClosure
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty CGiven a morphism property W, the multiplicativeClosure W is the smallest
multiplicative property greater than or equal to W.
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- CategoryTheory.MorphismPropertystatement · cited by 2,179
Cited by24
Results whose statement or proof uses this declaration.
- CategoryTheory.MorphismProperty.le_multiplicativeClosurestatement · cited by 6
- SimplexCategoryGenRel.P_σproof · cited by 5
- SimplexCategoryGenRel.P_δproof · cited by 5
- CategoryTheory.MorphismProperty.multiplicativeClosure_le_iffstatement and proof · cited by 4
- SimplexCategoryGenRel.multiplicativeClosure_isGenerator_eq_topstatement and proof · cited by 2
- CategoryTheory.Cat.FreeRefl.multiplicativeClosure_morphismPropertyHomMkstatement and proof · cited by 2
- SimplexCategoryGenRel.hom_inductionproof · cited by 1
- CategoryTheory.MorphismProperty.strictMap_multiplicativeClosure_lestatement and proof · cited by 1
- SSet.Truncated.HomotopyCategory.multiplicativeClosure_morphismPropertyHomMkstatement and proof · cited by 1
- CategoryTheory.MorphismProperty.multiplicativeClosure.belowstatement · cited by 1
- CategoryTheory.MorphismProperty.multiplicativeClosure.casesOnstatement and proof · cited by 1
- CategoryTheory.MorphismProperty.multiplicativeClosure_eq_multiplicativeClosure'statement and proof · cited by 1