English
If a functor adjunction and related conditions hold, adhesive structure transfers along reflective adjunctions.
Русский
Если выполняются условия связки-функторов и сопутствующие условия, адгезивность переносится через отражающие отношения.
LaTeX
$$$\text{Adhesive}(D)$$$
Lean4
theorem adhesive_of_reflective [HasPullbacks D] [Adhesive C] [HasPullbacks C] [HasPushouts C]
[H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g] {Gl : C ⥤ D} {Gr : D ⥤ C} (adj : Gl ⊣ Gr)
[Gr.Full] [Gr.Faithful] [PreservesLimitsOfShape WalkingCospan Gl] : Adhesive D :=
by
have := adj.leftAdjoint_preservesColimits
have := adj.rightAdjoint_preservesLimits
apply Adhesive.mk (hasPushout_of_mono_left := H₂)
intro W X Y Z f g h i _ H
have := Adhesive.van_kampen (IsPushout.of_hasPushout (Gr.map f) (Gr.map g))
rw [IsPushout.isVanKampen_iff] at this ⊢
refine
(IsVanKampenColimit.precompose_isIso_iff
(Functor.isoWhiskerLeft _ (asIso adj.counit) ≪≫ Functor.rightUnitor _).hom).mp
?_
refine ((this.precompose_isIso (spanCompIso _ _ _).hom).map_reflective adj).of_iso (IsColimit.uniqueUpToIso ?_ ?_)
· exact isColimitOfPreserves Gl ((IsColimit.precomposeHomEquiv _ _).symm <| pushoutIsPushout _ _)
· exact (IsColimit.precomposeHomEquiv _ _).symm H.isColimit
