Theorems · Theorem · category theory

CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.exists_d_comp_eq_d

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] {G : C},
  CategoryTheory.IsSeparator G →
    ∀ {A : C} (B : C) [CategoryTheory.Injective B] {M : ModuleCat (CategoryTheory.End G)ᵐᵒᵖ}
      (g : M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ A)),
      CategoryTheory.Mono g →
        ∀ (f : M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ B)),
          ∃ l,
            CategoryTheory.CategoryStruct.comp (CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d g) l =
              CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d f

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.IsGrothendieckAbelianCategoryTheory.Injective