adhesive_of_preserves_and_reflects_isomorphism

English

If F preserves and reflects isomorphisms and certain limits/colimits are preserved, then C is adhesive when D is adhesive.

Русский

Если F сохраняет и отражает изоморфизмы и заданные пределы/коспины сохраняются, то C адгезивна, если D адгезивна.

LaTeX

$$$\text{Adhesive}(C)$$$

Lean4

theorem adhesive_of_preserves_and_reflects_isomorphism (F : C ⥤ D) [Adhesive D] [HasPullbacks C] [HasPushouts C]
    [PreservesLimitsOfShape WalkingCospan F] [PreservesColimitsOfShape WalkingSpan F] [F.ReflectsIsomorphisms] :
    Adhesive C :=
  by
  haveI : ReflectsLimitsOfShape WalkingCospan F := reflectsLimitsOfShape_of_reflectsIsomorphisms
  haveI : ReflectsColimitsOfShape WalkingSpan F := reflectsColimitsOfShape_of_reflectsIsomorphisms
  exact adhesive_of_preserves_and_reflects F

Похожие утверждения