Theorems · Inductive type · category theory
CategoryTheory.JointlyFaithful
{C : Type u_1} →
[inst : CategoryTheory.Category.{u_4, u_1} C] →
{I : Type u_2} →
{D : I → Type u_3} →
[inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] →
((i : I) → CategoryTheory.Functor C (D i)) → PropA family of functors is jointly faithful if whenever two morphisms f : X ⟶ Y
and g : X ⟶ Y become equal after applying all functors F i, then f = g.
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
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.Functorstatement · cited by 16,252
Cited by9
Results whose statement or proof uses this declaration.
- CategoryTheory.JointlyFaithful.map_injectivestatement and proof · cited by 2
- CategoryTheory.JointlyFaithful.of_jointly_reflects_isIso_of_monostatement · cited by 2
- CategoryTheory.JointlyReflectIsomorphisms.jointlyFaithfulstatement · cited by 1
- CategoryTheory.JointlyFaithful.jointlyReflectEpimorphismsstatement and proof · cited by 1
- CategoryTheory.JointlyFaithful.jointlyReflectMonomorphismsstatement and proof · cited by 1
- CategoryTheory.JointlyFaithful.jointlyReflectsIsomorphismsstatement and proof · cited by 1
- CategoryTheory.JointlyFaithful.casesOnstatement and proof · cited by 0
- CategoryTheory.JointlyFaithful.recOnstatement and proof · cited by 0
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyFaithfulstatement · cited by 0