WeightedGeometry.lean

1 import Mathlib.CategoryTheory.Preadditive.Basic
2 import Mathlib.Basic.ENNReal.Operations
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Optional directed geometry from an independently specified transport cost
8 
9 A cost is extra data. It must not be silently identified with a compatibility
10 residual: all zero transports are compatible in the additive setting.
11 -/
12 universe u v
13 namespace KomorebiSpace
14 open CategoryTheory CategoryTheory.Limits
15 open scoped ENNReal
16 noncomputable section
17 
18 structure TransportCost (C : Type u) [Category.{v} C] where
19   cost : {A B : C} → (A ⟶ B) → ℝ≥0∞
20   id_zero : ∀ A, cost (𝟙 A) = 0
21   comp_le : ∀ {A B D : C} (f : A ⟶ B) (g : B ⟶ D),
22     cost (f ≫ g) ≤ cost f + cost g
23 
24 namespace TransportCost
25 variable {C : Type u} [Category.{v} C]
26 
27 def distance (W : TransportCost C) (A B : C) : ℝ≥0∞ := ⨅ f : A ⟶ B, W.cost f
28 
29 theorem distance_le_cost (W : TransportCost C) {A B : C} (f : A ⟶ B) :
30     W.distance A B ≤ W.cost f := iInf_le _ f
31 
32 @[simp] theorem distance_self (W : TransportCost C) (A : C) : W.distance A A = 0 := by
33   apply le_antisymm _ bot_le
34   exact (W.distance_le_cost (𝟙 A)).trans_eq (W.id_zero A)
35 
36 theorem distance_triangle (W : TransportCost C) (A B D : C) :
37     W.distance A D ≤ W.distance A B + W.distance B D := by
38   apply ENNReal.le_iInf_add_iInf
39   intro f g
40   exact (W.distance_le_cost (f ≫ g)).trans (W.comp_le f g)
41 
42 theorem zero_cost_distance (W : TransportCost C) {A B : C}
43     (f : A ⟶ B) (hf : W.cost f = 0) : W.distance A B = 0 := by
44   exact le_antisymm ((W.distance_le_cost f).trans_eq hf) bot_le
45 
46 /-- Diagnostic: compatible zero arrows collapse this proposed geometry. -/
47 theorem collapse_of_zero_arrows [HasZeroMorphisms C] (W : TransportCost C)
48     (hzero : ∀ A B, W.cost (0 : A ⟶ B) = 0) (A B : C) :
49     W.distance A B = 0 := W.zero_cost_distance 0 (hzero A B)
50 
51 def symDistance (W : TransportCost C) (A B : C) : ℝ≥0∞ :=
52   max (W.distance A B) (W.distance B A)
53 
54 @[simp] theorem symDistance_self (W : TransportCost C) (A : C) :
55     W.symDistance A A = 0 := by simp [symDistance]
56 
57 theorem symDistance_comm (W : TransportCost C) (A B : C) :
58     W.symDistance A B = W.symDistance B A := max_comm _ _
59 
60 theorem symDistance_triangle (W : TransportCost C) (A B D : C) :
61     W.symDistance A D ≤ W.symDistance A B + W.symDistance B D := by
62   apply max_le
63   · exact (W.distance_triangle A B D).trans
64       (add_le_add (le_max_left _ _) (le_max_left _ _))
65   · calc
66       W.distance D A ≤ W.distance D B + W.distance B A := W.distance_triangle D B A
67       _ ≤ W.symDistance B D + W.symDistance A B :=
68         add_le_add (le_max_right _ _) (le_max_right _ _)
69       _ = W.symDistance A B + W.symDistance B D := add_comm _ _
70 
71 /-- Zero symmetric cost is an equivalence relation, not an isomorphism criterion. -/
72 def zeroDistanceSetoid (W : TransportCost C) : Setoid C where
73   r := fun A B => W.symDistance A B = 0
74   iseqv := ⟨W.symDistance_self,
75     fun h => by simpa only [W.symDistance_comm] using h,
76     fun {A B D} hAB hBD => by
77       apply le_antisymm _ bot_le
78       change W.symDistance A D ≤ (0 : ENNReal)
79       have ht := W.symDistance_triangle A B D
80       simpa only [hAB, hBD, zero_add] using ht⟩
81 
82 end TransportCost
83 end
84 end KomorebiSpace

Back to source controls