English
If F : C → D preserves and reflects certain limits/colimits and D is adhesive, then C inherits adhesivity.
Русский
Если F : C → D сохраняет и отражает определённые пределы/коспины, а D адгезивна, то C наследует адгезивность.
LaTeX
$$$\text{Adhesive}(C)$$$
Lean4
theorem adhesive_of_preserves_and_reflects (F : C ⥤ D) [Adhesive D]
[H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g]
[H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g] [PreservesLimitsOfShape WalkingCospan F]
[ReflectsLimitsOfShape WalkingCospan F] [PreservesColimitsOfShape WalkingSpan F]
[ReflectsColimitsOfShape WalkingSpan F] : Adhesive C :=
by
apply Adhesive.mk (hasPullback_of_mono_left := H₁) (hasPushout_of_mono_left := H₂)
intro W X Y Z f g h i hf H
rw [IsPushout.isVanKampen_iff]
refine IsVanKampenColimit.of_mapCocone F ?_
refine (IsVanKampenColimit.precompose_isIso_iff (diagramIsoSpan _).inv).mp ?_
refine IsVanKampenColimit.of_iso ?_ (PushoutCocone.isoMk _).symm
refine (IsPushout.isVanKampen_iff (H.map F)).mp ?_
apply Adhesive.van_kampen
