sigmaIsoSigma_hom_ι — Mathlib

English

For a family α, the i-th injection followed by the forward projection of the sigma-sigma isomorphism equals the canonical injection into the sigma object.

Русский

Для семейства α i-я инъекция затем образующая карта изоморфизма σ-σ равна канонической инъекции в объект сигма.

LaTeX

$$$\\Sigma\\_\\iota α i \\;\\circ\\; (\\sigma\\mathrm{iso}\\sigma α).hom = \\sigma\\iota α i$$$

Lean4

@[reassoc (attr := simp)]
theorem sigmaIsoSigma_hom_ι {ι : Type v} (α : ι → TopCat.{max v u}) (i : ι) :
    Sigma.ι α i ≫ (sigmaIsoSigma α).hom = sigmaι α i := by simp [sigmaIsoSigma]

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