OAI/Algebra/Finitistic/Localization/SplitComponentExact.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ExternalTensor.Section4.SourceFiltration.component_shortExact line 13

   Source documentation

   A specified degreewise splitting proves exactness for its original maps.

   theorem component_shortExact (i : X ⟶ Y) (q : Y ⟶ Z)
       (r : Y ⟶ X) (s : Z ⟶ Y)
       (hi : i ≫ r = 𝟙 _) (hq : s ≫ q = 𝟙 _)
       (hz : i ≫ q = 0) (hs : r ≫ i + q ≫ s = 𝟙 _) (n : ℤ) :
       Function.Injective (i.f n) ∧ Function.Exact (i.f n) (q.f n) ∧
         Function.Surjective (q.f n) := by
   …

   Mentions: OAI.ExternalTensor.Section4.q, OAI.ExternalTensor.Section4.SourceFiltration.Z

2. theorem OAI.ExternalTensor.Section4.SourceFiltration.inr_fst_shortExact line 40
3. theorem OAI.ExternalTensor.Section4.SourceFiltration.zero_id_shortExact line 48