gluedLift_p2 — Mathlib

English

In the pullback setup, the fst-to-V morphism composed with fst yields the snd projection; illustrates how fst interacts with V and the pullback.

Русский

В конфигурации обратного диаграммы композиция fst-to-V с fst даёт проекцию snd; иллюстрирует взаимодействие fst с V и обратным.

LaTeX

$$$ pullbackFstιToV 𝒰 f g i j \\;\\gg\\; \\mathrm{fst} \\_ \\_ = \\mathrm{snd} \\_ \\_$$

Lean4

theorem gluedLift_p2 : gluedLift 𝒰 f g s ≫ p2 𝒰 f g = s.snd :=
  by
  rw [← cancel_epi (Cover.fromGlued <| 𝒰.pullback₁ s.fst)]
  apply Multicoequalizer.hom_ext
  intro b
  simp_rw [Cover.fromGlued, Multicoequalizer.π_desc_assoc, gluedLift, ← Category.assoc]
  simp_rw [(Cover.ι_glueMorphisms <| 𝒰.pullback₁ s.fst)]
  simp [p2]

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