Theorems · Theorem · category theory

CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation.of_mono

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (f : P ⟶ Q) [CategoryTheory.Mono f] {x : CategoryTheory.Presieve.FamilyOfElements P R}
  {t : P.obj (Opposite.op X)},
  (x.map f).IsAmalgamation ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X))) t) → x.IsAmalgamation t

Defined in

Mathlib.CategoryTheory.Sites.IsSheafFor

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Mono