preimage_map_fst_pullbackDiagonal

English

For any f:X→Y, g:Z→Y, the preimage of pullbackDiagonal f under map_fst equals pullbackDiagonal of (f ∘ g).

Русский

Преобразование предварительного образа диагонали через map_fst даёт диагональ в композиции f∘g.

LaTeX

$$$(\\mathrm{map\\_fst}\ f\ g)^{-1}(\\mathrm{pullbackDiagonal}\ f) = \\mathrm{pullbackDiagonal}(f \\circ g)$$$

Lean4

theorem preimage_map_fst_pullbackDiagonal {f : X → Y} {g : Z → Y} :
    @map_fst X Y Z f g ⁻¹' pullbackDiagonal f = pullbackDiagonal (@snd X Y Z f g) :=
  by
  ext ⟨⟨p₁, p₂⟩, he⟩
  simp_rw [pullbackDiagonal, mem_setOf, Subtype.ext_iff, Prod.ext_iff]
  exact (and_iff_left he).symm

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