gluedLift_p1 — Mathlib

English

The second projection of the glued lift equals the second component of the pullback glue data.

Русский

Вторая проекция склейенного подъёма равна второй компоненте данных склейки обратного.

LaTeX

$$$ \\text{gluedLift}(\\mathcal{U},f,g,s) \\;\\gg\\; p_2 𝒰 f g = s.snd$$

Lean4

theorem gluedLift_p1 : gluedLift 𝒰 f g s ≫ p1 𝒰 f g = s.fst :=
  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 [p1, pullback.condition]

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