ExactProducts.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.RectificationTotal.exact_prod line 10
Source documentation
Exact pairs remain exact under the concrete binary product of maps.
```
theorem exact_prod (h : Function.Exact f g) (h' : Function.Exact f' g') :
    Function.Exact (Prod.map f f') (Prod.map g g') := by
…
```

theorem OAI.LittleFinitistic.RectificationTotal.shortExact_prod line 23

Source documentation

Short exactness is also preserved by the concrete binary product.

theorem shortExact_prod (h : Function.Exact f g) (h' : Function.Exact f' g')
    (hf : Function.Injective f) (hf' : Function.Injective f')
    (hg : Function.Surjective g) (hg' : Function.Surjective g') :
    Function.Injective (Prod.map f f') ∧
      Function.Exact (Prod.map f f') (Prod.map g g') ∧
      Function.Surjective (Prod.map g g') := by
…

theorem OAI.LittleFinitistic.RectificationTotal.exact_transport line 45
theorem OAI.LittleFinitistic.RectificationTotal.shortExact_transport line 56