Theorems · Theorem · category theory

CategoryTheory.Localization.Preadditive.add.congr_simp

∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1)
  [inst_3 : L.IsLocalization W] [inst_4 : W.HasLeftCalculusOfFractions] {X Y : C} {X' Y' : D} (eX eX_1 : L.obj X ≅ X'),
  eX = eX_1 →
    ∀ (eY eY_1 : L.obj Y ≅ Y'),
      eY = eY_1 →
        ∀ (f₁ f₁_1 : X' ⟶ Y'),
          f₁ = f₁_1 →
            ∀ (f₂ f₂_1 : X' ⟶ Y'),
              f₂ = f₂_1 →
                CategoryTheory.Localization.Preadditive.add W eX eY f₁ f₂ =
                  CategoryTheory.Localization.Preadditive.add W_1 eX_1 eY_1 f₁_1 f₂_1

Defined in

Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Cited by

1 results in Mathlib

Foundations

Depth 40 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.Functor.IsLocalizationCategoryTheory.MorphismProperty.HasLeftCalculusOfFractions