ι_functorMapSrc — Mathlib

English

A precise commuting identity relating Sigma-ι and functorMapSrc with respect to τ is established.

Русский

Устанавливается точное коммутативное тождество, связывающее Sigma-ι и functorMapSrc относительно τ.

LaTeX

$$$ \Sigma.\iota (FunctorObjIndex.mk i t b w) \;\circ\; functorMapSrc f τ = \Sigma.\iota (functorObjSrcFamily f πY) (FunctorObjIndex.mk i t' b' w') $$$

Lean4

@[reassoc]
theorem ι_functorMapSrc (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : t ≫ πX = f i ≫ b) (b' : B i ⟶ T)
    (hb' : b ≫ τ.right = b') (t' : A i ⟶ Y) (ht' : t ≫ τ.left = t') :
    Sigma.ι _ (FunctorObjIndex.mk i t b w) ≫ functorMapSrc f τ =
      Sigma.ι (functorObjSrcFamily f πY)
        (FunctorObjIndex.mk i t' b'
          (by
            have := τ.w
            dsimp at this
            rw [← hb', ← reassoc_of% w, ← ht', assoc, this])) :=
  by
  subst hb' ht'
  simp [functorMapSrc]

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