associativityFunctorEquivNaturalityFunctorIso

English

The equivalence Sum.functorEquiv sends associativity of sums to associativity of products.

Русский

Эквивалентность Sum.functorEquiv переносит ассоциативность сумм к ассоциативности произведений.

LaTeX

$$associativityFunctorEquivNaturalityFunctorIso A A' T B$$

Lean4

/-- The equivalence `Sum.functorEquiv` sends associativity of sums to associativity of products -/
@[simps! hom_app_fst hom_app_snd_fst hom_app_snd_snd inv_app_fst inv_app_snd_fst inv_app_snd_snd]
def associativityFunctorEquivNaturalityFunctorIso :
    ((sum.associativity A A' T).congrLeft.trans <|
          (Sum.functorEquiv A (A' ⊕ T) B).trans <| Equivalence.refl.prod <| Sum.functorEquiv _ _ B).functor ≅
      (Sum.functorEquiv (A ⊕ A') T B).trans ((Sum.functorEquiv A A' B).prod Equivalence.refl) |>.trans
          (prod.associativity _ _ _) |>.functor :=
  NatIso.ofComponents
    (fun E ↦
      Iso.prod
        ((Functor.associator _ _ _).symm ≪≫
          isoWhiskerRight (sum.inlCompInverseAssociator A A' T) E ≪≫ Functor.associator _ _ _)
        (Iso.prod
          (isoWhiskerLeft _ (Functor.associator _ _ E).symm ≪≫
            (Functor.associator _ _ E).symm ≪≫
              isoWhiskerRight (sum.inlCompInrCompInverseAssociator A A' T) E ≪≫ Functor.associator _ _ E)
          (isoWhiskerLeft _ (Functor.associator _ _ E).symm ≪≫
            (Functor.associator _ _ E).symm ≪≫ isoWhiskerRight (sum.inrCompInrCompInverseAssociator A A' T) E)))
    (by
      intros
      ext
      all_goals
        dsimp
        simp only [Category.comp_id, Category.id_comp, NatTrans.naturality])

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