Theorems · Theorem · category theory

CategoryTheory.Precoherent.pullback

∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.Precoherent C] {B₁ B₂ : C}
  (f : B₂ ⟶ B₁) (α : Type) [Finite α] (X₁ : α → C) (π₁ : (a : α) → X₁ a ⟶ B₁),
  CategoryTheory.EffectiveEpiFamily X₁ π₁ →
    ∃ β,
      ∃ (_ : Finite β),
        ∃ X₂ π₂,
          CategoryTheory.EffectiveEpiFamily X₂ π₂ ∧
            ∃ i ι,
              ∀ (b : β),
                CategoryTheory.CategoryStruct.comp (ι b) (π₁ (i b)) = CategoryTheory.CategoryStruct.comp (π₂ b) f

Given an effective epi family π₁ over B₁ and a morphism f : B₂ ⟶ B₁, there exists an effective epi family π₂ over B₂, such that π₂ factors through π₁.

Defined in

Mathlib.CategoryTheory.Sites.Coherent.Basic

Cited by

1 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.PrecoherentFinite