Theorems · Theorem · category theory

CategoryTheory.EffectiveEquivalenceRelation.mk.inj

∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {R A : C} {p₁ p₂ : R ⟶ A}
  {toEquivalenceRelation : CategoryTheory.EquivalenceRelation p₁ p₂} {B : C} {π : A ⟶ B}
  {isKernelPair : CategoryTheory.IsKernelPair π p₁ p₂} {isPushout : CategoryTheory.IsPushout p₁ p₂ π π}
  {toEquivalenceRelation_1 : CategoryTheory.EquivalenceRelation p₁ p₂} {B_1 : C} {π_1 : A ⟶ B_1}
  {isKernelPair_1 : CategoryTheory.IsKernelPair π_1 p₁ p₂} {isPushout_1 : CategoryTheory.IsPushout p₁ p₂ π_1 π_1},
  { toEquivalenceRelation := toEquivalenceRelation, B := B, π := π, isKernelPair := isKernelPair,
        isPushout := isPushout } =
      { toEquivalenceRelation := toEquivalenceRelation_1, B := B_1, π := π_1, isKernelPair := isKernelPair_1,
        isPushout := isPushout_1 } →
    toEquivalenceRelation = toEquivalenceRelation_1 ∧ B = B_1 ∧ π ≍ π_1

Defined in

Mathlib.CategoryTheory.EquivalenceRelation

Cited by

1 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms