/-- **Lawvere's monoidal category `([0, ∞], ≥, +, 0)`.** Its objects are the extendednon-negative reals; we use the order dual of `ℝ≥0∞`, so that (by Mathlib's category structure ona preorder) there is exactly one arrow `a ⟶ b` when `a ≥ b` as distances, and none otherwise. -/abbrev Dist : Type := ℝ≥0∞ᵒᵈ
/-- The monoidal structure on `Dist`: `a ⊗ b = a + b`, unit `0`. Addition is monotone, so itacts on arrows, and the associator and unitors are the equalities `(a + b) + c = a + (b + c)`,`0 + a = a`, `a + 0 = a`. In a category with at most one arrow between two objects every diagramcommutes, so the pentagon and triangle axioms hold automatically. -/instance distMonoidal : MonoidalCategory Dist where tensorObj a b := a + b whiskerLeft a _ _ f := homOfLE (add_le_add_right (leOfHom f) a) whiskerRight f b := homOfLE (add_le_add_left (leOfHom f) b) tensorUnit := 0 associator a b c := eqToIso (add_assoc a b c) leftUnitor a := eqToIso (zero_add a) rightUnitor a := eqToIso (add_zero a) id_tensorHom_id _ _ := Subsingleton.elim _ _ tensorHom_comp_tensorHom _ _ _ _ := Subsingleton.elim _ _ whiskerLeft_id _ _ := Subsingleton.elim _ _ id_whiskerRight _ _ := Subsingleton.elim _ _ associator_naturality _ _ _ := Subsingleton.elim _ _ leftUnitor_naturality _ := Subsingleton.elim _ _ rightUnitor_naturality _ := Subsingleton.elim _ _ pentagon _ _ _ _ := Subsingleton.elim _ _ triangle _ _ := Subsingleton.elim _ _
/-- A **Lawvere metric** on `X`: distances `d x y ∈ [0, ∞]` with `d x x = 0` and the triangleinequality. Symmetry, finiteness and "`d x y = 0 → x = y`" are *not* required. -/structure LawvereMetric (X : Type u) where /-- The distance from `x` to `y`. -/ d : X → X → ℝ≥0∞ /-- Every point is at distance `0` from itself. -/ self : ∀ x, d x x = 0 /-- The triangle inequality. -/ triangle : ∀ x y z, d x z ≤ d x y + d y z
LawvereMetric.exttheoremProved here from basic factspropext, Classical.choice, Quot.sound
extLean 4Proved here from basic factsFormally verified
/-- Two Lawvere metrics with the same distance function are equal. -/@[ext]theorem LawvereMetric.ext {X : Type u} {M N : LawvereMetric X} (h : M.d = N.d) : M = N := by cases M cases N cases h rfl
lawvereEquivEnricheddefProved here from basic factspropext, Classical.choice, Quot.sound
lawvereEquivEnrichedLean 4Proved here from basic factsFormally verified
/-- **Lawvere's observation: metric spaces are enriched categories.** On any type `X`,`Dist`-enriched category structures (in Mathlib's sense) correspond exactly to Lawvere metrics.* the hom-object `X(x, y)` is the distance `d x y`;* an identity `0 ⟶ X(x, x)` exists iff `0 ≥ d x x`, i.e. `d x x = 0`;* a composition `X(x, y) ⊗ X(y, z) ⟶ X(x, z)` exists iff `d x y + d y z ≥ d x z` — the triangle inequality *is* composition;* the unit and associativity axioms hold automatically, since `Dist` is thin. -/def lawvereEquivEnriched (X : Type u) : LawvereMetric X ≃ EnrichedCategory Dist X where toFun M := { Hom := fun x y => OrderDual.toDual (M.d x y) id := fun x => homOfLE (by show M.d x x ≤ 0 rw [M.self]) comp := fun x y z => homOfLE (M.triangle x y z) id_comp := fun _ _ => Subsingleton.elim _ _ comp_id := fun _ _ => Subsingleton.elim _ _ assoc := fun _ _ _ _ => Subsingleton.elim _ _ } invFun E := { d := fun x y => OrderDual.ofDual (E.Hom x y) self := fun x => le_antisymm (leOfHom (E.id x)) zero_le triangle := fun x y z => leOfHom (E.comp x y z) } left_inv M := by ext x y rfl right_inv E := by -- the hom-objects agree definitionally, and identities and compositions are arrows in a -- thin category, so `congr` closes the goal (using `Subsingleton`) rcases E with ⟨Hom, id, comp, _, _, _⟩ congr
ofPseudoEMetricdefApplies a library theorempropext, Classical.choice, Quot.sound
ofPseudoEMetricLean 4Applies a library theoremFormally verified
/-- **Every (pseudo-extended) metric space is a Lawvere metric space**, using Mathlib's`edist_self` and `edist_triangle`. Lawvere's notion drops symmetry and allows `d x y = 0` for`x ≠ y`. -/def ofPseudoEMetric (X : Type u) [PseudoEMetricSpace X] : LawvereMetric X where d := edist self := edist_self triangle := edist_triangle
/-- The **uphill distance** on `ℝ` (think of heights): going from `x` up to `y` costs `y - x`,going down is free. In `ℝ≥0∞`, `d x y = ofReal (y - x)`, where `ofReal` truncates negativenumbers to `0`. -/noncomputable def uphill : LawvereMetric ℝ where d x y := ENNReal.ofReal (y - x) self x := by simp triangle x y z := by calc ENNReal.ofReal (z - x) = ENNReal.ofReal ((y - x) + (z - y)) := by ring_nf _ ≤ ENNReal.ofReal (y - x) + ENNReal.ofReal (z - y) := ENNReal.ofReal_add_le
underlying_preordertheoremProved here from basic factspropext, Classical.choice, Quot.sound
underlying_preorderLean 4Proved here from basic factsFormally verified
/-- **The underlying ordinary category of a Lawvere metric space** is a preorder: there is anarrow `x → y` (an arrow `0 ⟶ X(x, y)` in `Dist`) exactly when `d x y = 0`, and this relation isreflexive and transitive by `d x x = 0` and the triangle inequality. -/theorem underlying_preorder {X : Type u} (M : LawvereMetric X) : (∀ x, M.d x x = 0) ∧ (∀ x y z, M.d x y = 0 → M.d y z = 0 → M.d x z = 0) := by refine ⟨M.self, fun x y z hxy hyz => ?_⟩ apply le_antisymm _ zero_le calc M.d x z ≤ M.d x y + M.d y z := M.triangle x y z _ = 0 := by rw [hxy, hyz, add_zero]
yoneda_isometrytheoremProved here from basic factspropext, Classical.choice, Quot.sound
yoneda_isometryLean 4Proved here from basic factsFormally verified
/-- **The enriched Yoneda lemma for Lawvere metric spaces.** Send `x` to the "distance-to"function `d(-, x)`. Comparing these functions with the closed structure of `Dist` (truncatedsubtraction) recovers the metric:`d x y = sup_z (d z y - d z x)`.So `x ↦ d(-, x)` is an isometric embedding of `X` into a space of functions — the Yonedaembedding, which for symmetric metric spaces is the Kuratowski–Fréchet embedding.Proof: each term is `≤ d x y` because `d z y ≤ d z x + d x y` (triangle inequality, via`tsub_le_iff_left`), and the term `z = x` equals `d x y - 0 = d x y`. -/theorem yoneda_isometry {X : Type u} (M : LawvereMetric X) (x y : X) : ⨆ z, (M.d z y - M.d z x) = M.d x y := by apply le_antisymm · exact iSup_le fun z => tsub_le_iff_left.mpr (M.triangle z x y) · exact le_iSup_of_le x (by rw [M.self, tsub_zero])
nonExpansiveEquivdefProved here from basic factspropext, Classical.choice, Quot.sound
nonExpansiveEquivLean 4Proved here from basic factsFormally verified
/-- **`Dist`-enriched functors are exactly non-expansive (1-Lipschitz) maps.** A `Dist`-functor`F : X → Y` consists of a map on points with an arrow `X(x, y) ⟶ Y(F x, F y)` in `Dist` for all`x, y`, i.e. `d (F x) (F y) ≤ d x y`; the functor axioms are automatic. -/def nonExpansiveEquiv {X : Type u} {Y : Type v} [EnrichedCategory Dist X] [EnrichedCategory Dist Y] : { f : X → Y // ∀ x x', OrderDual.ofDual (EnrichedCategory.Hom (V := Dist) (f x) (f x')) ≤ OrderDual.ofDual (EnrichedCategory.Hom (V := Dist) x x') } ≃ EnrichedFunctor Dist X Y where toFun f := { obj := f.1 map := fun x x' => homOfLE (f.2 x x') map_id := fun _ => Subsingleton.elim _ _ map_comp := fun _ _ _ => Subsingleton.elim _ _ } invFun F := ⟨F.obj, fun x x' => leOfHom (F.map x x')⟩ left_inv _ := rfl right_inv F := by rcases F with ⟨obj, map, _, _⟩ simp only [EnrichedFunctor.mk.injEq, heq_eq_eq, true_and] funext x x' exact Subsingleton.elim _ _
dist_closedtheoremApplies a library theorempropext, Classical.choice, Quot.sound
dist_closedLean 4Applies a library theoremFormally verified
/-- **`Dist` is closed**: the internal hom is truncated subtraction, `[a, b] = b - a`, because`a + c ≥ b ↔ c ≥ b - a` (Mathlib's `tsub_le_iff_left` in `ℝ≥0∞`). So `Dist`-categories can beenriched over themselves, which is what makes `supMetric` a hom-object. -/theorem dist_closed (a b c : ℝ≥0∞) : b - a ≤ c ↔ b ≤ a + c := tsub_le_iff_left
/-- **Truth values as a monoidal category.** `Prop` is a preorder under implication, hence acategory with an arrow `p ⟶ q` exactly when `p → q`; the tensor is `∧` and the unit is `True`.Again all coherence axioms hold because the category is thin. -/instance truthMonoidal : MonoidalCategory Prop where tensorObj p q := p ∧ q whiskerLeft p _ _ f := homOfLE fun h => ⟨h.1, leOfHom f h.2⟩ whiskerRight f q := homOfLE fun h => ⟨leOfHom f h.1, h.2⟩ tensorUnit := True associator p q r := eqToIso (propext and_assoc) leftUnitor p := eqToIso (true_and p) rightUnitor p := eqToIso (and_true p) id_tensorHom_id _ _ := Subsingleton.elim _ _ tensorHom_comp_tensorHom _ _ _ _ := Subsingleton.elim _ _ whiskerLeft_id _ _ := Subsingleton.elim _ _ id_whiskerRight _ _ := Subsingleton.elim _ _ associator_naturality _ _ _ := Subsingleton.elim _ _ leftUnitor_naturality _ := Subsingleton.elim _ _ rightUnitor_naturality _ := Subsingleton.elim _ _ pentagon _ _ _ _ := Subsingleton.elim _ _ triangle _ _ := Subsingleton.elim _ _
preorderEquivEnricheddefProved here from basic factspropext
preorderEquivEnrichedLean 4Proved here from basic factsFormally verified
/-- **Preorders are exactly the categories enriched in truth values.** A `Prop`-enriched categoryon `X` is a relation `x ≤ y` (the hom-object) with an identity `True → (x ≤ x)` (reflexivity)and a composition `(x ≤ y) ∧ (y ≤ z) → (x ≤ z)` (transitivity). -/def preorderEquivEnriched (X : Type u) : { r : X → X → Prop // (∀ x, r x x) ∧ ∀ x y z, r x y → r y z → r x z } ≃ EnrichedCategory Prop X where toFun r := { Hom := r.1 id := fun x => homOfLE fun _ => r.2.1 x comp := fun x y z => homOfLE fun h => r.2.2 x y z h.1 h.2 id_comp := fun _ _ => Subsingleton.elim _ _ comp_id := fun _ _ => Subsingleton.elim _ _ assoc := fun _ _ _ _ => Subsingleton.elim _ _ } invFun E := ⟨E.Hom, fun x => leOfHom (E.id x) trivial, fun x y z h₁ h₂ => leOfHom (E.comp x y z) ⟨h₁, h₂⟩⟩ left_inv _ := rfl right_inv E := by -- the hom-objects agree definitionally, and identities and compositions are arrows in a -- thin category, so `congr` closes the goal (using `Subsingleton`) rcases E with ⟨Hom, id, comp, _, _, _⟩ congr
set_enrichedtheoremApplies a library theorempropext, Classical.choice, Quot.sound
set_enrichedLean 4Applies a library theoremFormally verified
/-- **Locally small categories are exactly the categories enriched in `(Type, ×, PUnit)`**(Mathlib's `enrichedCategoryTypeEquivCategory`). -/theorem set_enriched (C : Type u) : Nonempty (EnrichedCategory (Type v) C ≃ Category.{v} C) := ⟨enrichedCategoryTypeEquivCategory C⟩
end_ringtheoremApplies a library theorempropext, Quot.sound
end_ringLean 4Applies a library theoremFormally verified
/-- **In an `Ab`-enriched (preadditive) category, the endomorphisms of an object form a ring**,with addition from the enrichment and multiplication given by composition (Mathlib's instance`CategoryTheory.End` ring). A one-object `Ab`-enriched category is therefore a ring. -/theorem end_ring {C : Type u} [Category.{v} C] [Preadditive C] (X : C) : Nonempty (Ring (End X)) := ⟨inferInstance⟩
/-- In a Lawvere metric space, "distance zero" is transitive: this is composition in theunderlying ordinary category.Hint: `apply le_antisymm _ zero_le`, then use `M.triangle x y z` and rewrite with thehypotheses. -/theorem underlying_trans {X : Type u} (M : LawvereMetric X) (x y z : X) (hxy : M.d x y = 0) (hyz : M.d y z = 0) : M.d x z = 0 := by sorry
Show the compiled solution
underlying_preorderLean 4Proved here from basic factsFormally verified
/-- **The underlying ordinary category of a Lawvere metric space** is a preorder: there is anarrow `x → y` (an arrow `0 ⟶ X(x, y)` in `Dist`) exactly when `d x y = 0`, and this relation isreflexive and transitive by `d x x = 0` and the triangle inequality. -/theorem underlying_preorder {X : Type u} (M : LawvereMetric X) : (∀ x, M.d x x = 0) ∧ (∀ x y z, M.d x y = 0 → M.d y z = 0 → M.d x z = 0) := by refine ⟨M.self, fun x y z hxy hyz => ?_⟩ apply le_antisymm _ zero_le calc M.d x z ≤ M.d x y + M.d y z := M.triangle x y z _ = 0 := by rw [hxy, hyz, add_zero]