Theorems · Theorem · category theory

CategoryTheory.adhesive_of_preserves_and_reflects

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u''} [inst_1 : CategoryTheory.Category.{v'', u''} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Adhesive D]
  [H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [CategoryTheory.Mono f], CategoryTheory.Limits.HasPullback f g]
  [H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.Limits.HasPushout f g]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F]
  [CategoryTheory.Limits.ReflectsLimitsOfShape CategoryTheory.Limits.WalkingCospan F]
  [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan F]
  [CategoryTheory.Limits.ReflectsColimitsOfShape CategoryTheory.Limits.WalkingSpan F], CategoryTheory.Adhesive C

Defined in

Mathlib.CategoryTheory.Adhesive.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.AdhesiveCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.HasPushoutCategoryTheory.Limits.PreservesLimitsOfShapeCategoryTheory.Limits.ReflectsLimitsOfShapeCategoryTheory.Limits.PreservesColimitsOfShapeCategoryTheory.Limits.ReflectsColimitsOfShape