OAI/Algebra/Finitistic/Localization/FiniteSumTransport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.FiniteSumTransport.iso line 15
2. theorem OAI.LittleFinitistic.FiniteSumTransport.injection line 19
3. theorem OAI.LittleFinitistic.FiniteSumTransport.desc_square line 33

   Source documentation

   Coordinate isomorphisms commute with the supplied map from a finite sum.

   theorem desc_square {U : C} {V : D} (β : F.obj U ≅ G.obj V)
       (f : ∀ i, X i ⟶ U) (g : ∀ i, Y i ⟶ V)
       (h : ∀ i, (α i).hom ≫ G.map (g i) = F.map (f i) ≫ β.hom) :
       (iso F G X Y α).hom ≫ G.map (biproduct.desc g) =
         F.map (biproduct.desc f) ≫ β.hom := by
   …

   Mentions: OAI.LittleFinitistic.FiniteSumTransport.iso

4. theorem OAI.LittleFinitistic.FiniteSumTransport.projection line 47
5. theorem OAI.LittleFinitistic.FiniteSumTransport.matrix_square line 62

   Source documentation

   Entrywise coordinate squares identify the entire supplied finite matrix map.

   theorem matrix_square {J : Type} [Finite J] (X' : J → C) (Y' : J → D)
       (β : ∀ j, F.obj (X' j) ≅ G.obj (Y' j))
       (f : (⨁ X) ⟶ (⨁ X')) (g : (⨁ Y) ⟶ (⨁ Y'))
       (h : ∀ i j, (α i).hom ≫ G.map (biproduct.ι Y i ≫ g ≫ biproduct.π Y' j) =
         F.map (biproduct.ι X i ≫ f ≫ biproduct.π X' j) ≫ (β j).hom) :
       (iso F G X Y α).hom ≫ G.map g = F.map f ≫ (iso F G X' Y' β).hom := by
   …

   Mentions: OAI.LittleFinitistic.FiniteSumTransport.iso