Theorems · Theorem · category theory
SimplexCategory.eq_id_of_mono
∀ {x : SimplexCategory} (i : x ⟶ x) [CategoryTheory.Mono i], i = CategoryTheory.CategoryStruct.id x- Cited by
- 7 results in Mathlib
- Foundations
- Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Mono
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.CategoryStruct.idstatement · cited by 6,235
- SimplexCategorystatement and proof · cited by 2,204
- CategoryTheory.IsIsoproof · cited by 1,156
- CategoryTheory.Monostatement and proof · cited by 893
- SimplexCategory.eq_id_of_isIsoproof · cited by 4
- SimplexCategory.isIso_iff_of_monoproof · cited by 1
Cited by7
Results whose statement or proof uses this declaration.
- SimplexCategory.eq_δ_of_monoproof · cited by 4
- AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_compproof · cited by 1
- SSet.N.dim_lt_of_ltproof · cited by 1
- SSet.stdSimplex.nonDegenerate_top_dimproof · cited by 1
- AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInftyproof · cited by 1
- SSet.Subcomplex.Pairing.RankFunction.exists_or_of_range_m_Nproof · cited by 0
- SSet.S.mk_map_eq_iff_of_monoproof · cited by 0