English
In adhesive categories with van Kampen property, the pushout along a mono is van Kampen; this is part of a family of results in adhesive contexts.
Русский
В адгезивных категориях, обладающих свойством ван-Кемпен, расслоение через моно является ван-Кемпен; это часть ряда результатов в таких контекстах.
LaTeX
$$$[Adhesive C] \land [Mono f] \Rightarrow IsPushout(f,g,h,i).IsVanKampen$$
Lean4
theorem isVanKampen_inl {W E X Z : C} (c : BinaryCofan W E) [FinitaryExtensive C] [HasPullbacks C] (hc : IsColimit c)
(f : W ⟶ X) (h : X ⟶ Z) (i : c.pt ⟶ Z) (H : IsPushout f c.inl h i) : H.IsVanKampen :=
by
obtain ⟨hc₁⟩ := (is_coprod_iff_isPushout c hc H.1).mpr H
introv W' hf hg hh hi w
obtain ⟨hc₂⟩ :=
((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen c hc) (BinaryCofan.mk _ (pullback.fst _ _)) _ _ _
hg.w.symm pullback.condition.symm).mpr
⟨hg, IsPullback.of_hasPullback αY c.inr⟩
refine (is_coprod_iff_isPushout _ hc₂ w).symm.trans ?_
refine
((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen _ hc₁) (BinaryCofan.mk _ _) (pullback.snd _ _) _ _
?_ hh.w.symm).trans
?_
· dsimp; rw [← pullback.condition_assoc, Category.assoc, hi.w]
constructor
· rintro ⟨hc₃, hc₄⟩
refine ⟨hc₄, ?_⟩
let Y'' := pullback αZ i
let cmp : Y' ⟶ Y'' := pullback.lift i' αY hi.w
have e₁ : (g' ≫ cmp) ≫ pullback.snd _ _ = αW ≫ c.inl := by rw [Category.assoc, pullback.lift_snd, hg.w]
have e₂ : (pullback.fst _ _ ≫ cmp : pullback αY c.inr ⟶ _) ≫ pullback.snd _ _ = pullback.snd _ _ ≫ c.inr := by
rw [Category.assoc, pullback.lift_snd, pullback.condition]
obtain ⟨hc₄⟩ :=
((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen c hc) (BinaryCofan.mk _ _) αW _ _ e₁.symm
e₂.symm).mpr <|
by
constructor
· apply IsPullback.of_right _ e₁ (IsPullback.of_hasPullback _ _)
rw [Category.assoc, pullback.lift_fst, ← H.w, ← w.w]; exact hf.paste_horiz hc₄
· apply IsPullback.of_right _ e₂ (IsPullback.of_hasPullback _ _)
rw [Category.assoc, pullback.lift_fst]; exact hc₃
rw [← Category.id_comp αZ, ← show cmp ≫ pullback.snd _ _ = αY from pullback.lift_snd _ _ _]
apply IsPullback.paste_vert _ (IsPullback.of_hasPullback αZ i)
have : cmp = (hc₂.coconePointUniqueUpToIso hc₄).hom :=
by
apply BinaryCofan.IsColimit.hom_ext hc₂
exacts [(hc₂.comp_coconePointUniqueUpToIso_hom hc₄ ⟨WalkingPair.left⟩).symm,
(hc₂.comp_coconePointUniqueUpToIso_hom hc₄ ⟨WalkingPair.right⟩).symm]
rw [this]
exact IsPullback.of_vert_isIso ⟨by rw [← this, Category.comp_id, pullback.lift_fst]⟩
· rintro ⟨hc₃, hc₄⟩
exact ⟨(IsPullback.of_hasPullback αY c.inr).paste_horiz hc₄, hc₃⟩
