Squares.lean

1 import Mathlib.CategoryTheory.Preadditive.Basic
2 import Mathlib.Tactic.Abel
3 
4 set_option autoImplicit false
5 
6 /-! Typed compatibility defects in a preadditive category. -/
7 universe u v
8 namespace KomorebiSpace
9 open CategoryTheory
10 namespace Squares
11 variable {C : Type u} [Category.{v} C] [Preadditive C]
12 
13 def defect {A B A' B' : C} (f : A ⟶ B) (f' : A' ⟶ B')
14     (u : A ⟶ A') (v : B ⟶ B') : A ⟶ B' := f ≫ v - u ≫ f'
15 
16 theorem zero_iff {A B A' B' : C} (f : A ⟶ B) (f' : A' ⟶ B')
17     (u : A ⟶ A') (v : B ⟶ B') :
18     defect f f' u v = 0 ↔ f ≫ v = u ≫ f' := sub_eq_zero
19 
20 /-- Horizontal pasting, with all defects transported into a common Hom group. -/
21 theorem horizontal {A B D A' B' D' : C}
22     (f : A ⟶ B) (g : B ⟶ D) (f' : A' ⟶ B') (g' : B' ⟶ D')
23     (u : A ⟶ A') (v : B ⟶ B') (w : D ⟶ D') :
24     defect (f ≫ g) (f' ≫ g') u w =
25       f ≫ defect g g' v w + defect f f' u v ≫ g' := by
26   simp only [defect, Preadditive.comp_sub, Preadditive.sub_comp, Category.assoc]
27   abel
28 
29 /-- Vertical pasting. -/
30 theorem vertical {A B A' B' A'' B'' : C}
31     (f : A ⟶ B) (f' : A' ⟶ B') (f'' : A'' ⟶ B'')
32     (u : A ⟶ A') (v : B ⟶ B') (u' : A' ⟶ A'') (v' : B' ⟶ B'') :
33     defect f f'' (u ≫ u') (v ≫ v') =
34       defect f f' u v ≫ v' + u ≫ defect f' f'' u' v' := by
35   simp only [defect, Preadditive.comp_sub, Preadditive.sub_comp, Category.assoc]
36   abel
37 
38 theorem horizontal_flat {A B D A' B' D' : C}
39     (f : A ⟶ B) (g : B ⟶ D) (f' : A' ⟶ B') (g' : B' ⟶ D')
40     (u : A ⟶ A') (v : B ⟶ B') (w : D ⟶ D')
41     (hf : defect f f' u v = 0) (hg : defect g g' v w = 0) :
42     defect (f ≫ g) (f' ≫ g') u w = 0 := by
43   rw [horizontal, hf, hg]; simp
44 
45 theorem vertical_flat {A B A' B' A'' B'' : C}
46     (f : A ⟶ B) (f' : A' ⟶ B') (f'' : A'' ⟶ B'')
47     (u : A ⟶ A') (v : B ⟶ B') (u' : A' ⟶ A'') (v' : B' ⟶ B'')
48     (h₁ : defect f f' u v = 0) (h₂ : defect f' f'' u' v' = 0) :
49     defect f f'' (u ≫ u') (v ≫ v') = 0 := by
50   rw [vertical, h₁, h₂]; simp
51 end Squares
52 end KomorebiSpace

Back to source controls