OAI/Algebra/Finitistic/Rectification/BiprodEvaluationSquare.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.BiprodEvaluationSquare.square line 14

   Source documentation

   Transport both diagonal actions through additive evaluation and given summand isomorphisms.

   theorem square {A B : C} {A' B' : D} (f : A ⟶ A) (g : B ⟶ B)
       (i : F.obj A ≅ A') (j : F.obj B ≅ B') (f' : A' ⟶ A') (g' : B' ⟶ B')
       (hf : F.map f ≫ i.hom = i.hom ≫ f') (hg : F.map g ≫ j.hom = j.hom ≫ g') :
       F.map (biprod.map f g) ≫ (F.mapBiprod A B ≪≫ biprod.mapIso i j).hom =
         (F.mapBiprod A B ≪≫ biprod.mapIso i j).hom ≫ biprod.map f' g' := by
   …

2. theorem OAI.LittleFinitistic.BiprodEvaluationSquare.action_formula line 37