English
Given a Mayer-Vietoris square S and a weak sheafification, the resulting square after applying Yoneda and free constructions is a pushout in AddCommGrp-sheaves.
Русский
Для квадрата Майера–Виетоpиса S и слабой шейфификации получившийся квадрат после применения Яноиды и свободных конструкторов является пуш-аутом в категориях аддитивных коммутативных групп-својств.
LaTeX
$$$ (S.map\ (\mathrm{yoneda} \circ \mathrm{whiskeringRight}(\_ , \_ , \_).obj\ \mathrm{free} \circ \mathrm{presheafToSheaf}\ J\ _)).\mathrm{IsPushout} $$$
Lean4
/-- Constructor for Mayer-Vietoris squares taking as an input
a pullback square `sq` such that `sq.f₂₄` and `sq.f₃₄` are two monomorphisms
which form a covering of `S.X₄`. -/
@[simps! toSquare]
noncomputable def mk_of_isPullback (sq : Square C) [Mono sq.f₂₄] [Mono sq.f₃₄] (h₁ : sq.IsPullback)
(h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄) : J.MayerVietorisSquare :=
have : Mono sq.f₁₃ := h₁.mono_f₁₃
mk' sq
(fun F ↦ by
apply Square.IsPullback.mk
refine
PullbackCone.IsLimit.mk _
(fun s ↦
F.2.amalgamateOfArrows _ h₂ (fun j ↦ WalkingPair.casesOn j s.fst s.snd)
(fun W ↦ by
rintro (_ | _) (_ | _) a b fac
· obtain rfl : a = b := by simpa only [← cancel_mono sq.f₂₄] using fac
rfl
· obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' h₁.isLimit _ _ fac
simpa using s.condition =≫ F.val.map φ.op
· obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' h₁.isLimit _ _ fac.symm
simpa using s.condition.symm =≫ F.val.map φ.op
· obtain rfl : a = b := by simpa only [← cancel_mono sq.f₃₄] using fac
rfl))
(fun _ ↦ ?_) (fun _ ↦ ?_) (fun s m hm₁ hm₂ ↦ ?_)
· exact F.2.amalgamateOfArrows_map _ _ _ _ WalkingPair.left
· exact F.2.amalgamateOfArrows_map _ _ _ _ WalkingPair.right
· apply F.2.hom_ext_ofArrows _ h₂
rintro (_ | _)
· rw [F.2.amalgamateOfArrows_map _ _ _ _ WalkingPair.left]
exact hm₁
· rw [F.2.amalgamateOfArrows_map _ _ _ _ WalkingPair.right]
exact hm₂)
