tensorHom_left_snd — Mathlib

English

Similarly, (f ⊗ g).left composed with fst equals fst composed with f.left; and with snd yields snd relations for Over.

Русский

Аналогично, (f ⊗ g).left ∘ fst = fst ∘ f.left; и для snd выполняются подобные соотношения.

LaTeX

$$$ (f \\otimes g).left \\circ \\mathrm{fst}(f_S, f_U) = \\mathrm{fst}(R.hom, T.hom) \\circ f.left $$$

Lean4

@[reassoc (attr := simp)]
theorem tensorHom_left_snd {S U : C} {R T : Over X} (fS : S ⟶ X) (fU : U ⟶ X) (f : R ⟶ mk fS) (g : T ⟶ mk fU) :
    (f ⊗ₘ g).left ≫ pullback.snd fS fU = pullback.snd R.hom T.hom ≫ g.left :=
  limit.lift_π _ _

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