Category of Mereological Domains

Category with partially ordered types as objects and strictly monotone (MereoDim) maps as morphisms. StrictMono.id and StrictMono.comp from Mathlib provide the categorical identity and composition.

The DimensionChain.toMereoMor bridge connects the existing dimension chain infrastructure to categorical morphisms.

structure Core.Categorical.MereoObj : Type (u + 1)

Bundled partially ordered type: an object of the mereological category.

• α : Type u

  The carrier type.

• ord : PartialOrder self.α

  The partial order on the carrier.

structure Core.Categorical.MereoMor (A B : MereoObj) : Type u

A morphism in the mereological category: a bundled strictly monotone map. Corresponds to MereoDim in Core/MereoDim.lean.

• toFun : A.α → B.α

  The underlying function.

• strict_mono' : StrictMono self.toFun

  Strict monotonicity witness.

theorem Core.Categorical.MereoMor.ext {A B : MereoObj} {f g : MereoMor A B} (h : ∀ (x : A.α), f.toFun x = g.toFun x) : f = g

theorem Core.Categorical.MereoMor.ext_iff {A B : MereoObj} {f g : MereoMor A B} : f = g ↔ ∀ (x : A.α), f.toFun x = g.toFun x

def Core.Categorical.MereoMor.id (A : MereoObj) : MereoMor A A

Identity morphism: the identity function is strictly monotone.

Equations

• Core.Categorical.MereoMor.id A = { toFun := id, strict_mono' := ⋯ }

def Core.Categorical.MereoMor.comp {A B C : MereoObj} (f : MereoMor A B) (g : MereoMor B C) : MereoMor A C

Composition of morphisms (diagrammatic order: f then g).

Equations

• f.comp g = { toFun := g.toFun ∘ f.toFun, strict_mono' := ⋯ }

theorem Core.Categorical.MereoMor.monotone {A B : MereoObj} (f : MereoMor A B) : Monotone f.toFun

A MereoMor is monotone (forgetful map to the category of preorders).

@[implicit_reducible]

instance Core.Categorical.instCategoryMereoObj : CategoryTheory.Category.{u, u + 1} MereoObj

Equations

• One or more equations did not get rendered due to their size.

def Mereology.DimensionChain.toMereoMor {Source Inter Measure : Type u} [PartialOrder Source] [PartialOrder Inter] [PartialOrder Measure] {f : Source → Inter} {μ : Inter → Measure} (dc : DimensionChain f μ) : Core.Categorical.MereoMor { α := Source, ord := inst✝ } { α := Measure, ord := inst✝¹ }

A DimensionChain yields a composite morphism in MereoObj.

Given a chain Source →f Inter →μ Measure where both legs are MereoDim, the composition μ ∘ f is a morphism ⟨Source⟩ ⟶ ⟨Measure⟩ in the mereological category.

Equations

• dc.toMereoMor = { toFun := μ ∘ f, strict_mono' := ⋯ }

def Mereology.DimensionChain.leg₁ToMereoMor {Source Inter Measure : Type u} [PartialOrder Source] [PartialOrder Inter] [PartialOrder Measure] {f : Source → Inter} {μ : Inter → Measure} (dc : DimensionChain f μ) : Core.Categorical.MereoMor { α := Source, ord := inst✝ } { α := Inter, ord := inst✝¹ }

Each leg of a DimensionChain is individually a MereoMor.

Equations

• dc.leg₁ToMereoMor = { toFun := f, strict_mono' := ⋯ }

def Mereology.DimensionChain.leg₂ToMereoMor {Source Inter Measure : Type u} [PartialOrder Source] [PartialOrder Inter] [PartialOrder Measure] {f : Source → Inter} {μ : Inter → Measure} (dc : DimensionChain f μ) : Core.Categorical.MereoMor { α := Inter, ord := inst✝ } { α := Measure, ord := inst✝¹ }

Equations

• dc.leg₂ToMereoMor = { toFun := μ, strict_mono' := ⋯ }

theorem Mereology.DimensionChain.comp_eq {Source Inter Measure : Type u} [PartialOrder Source] [PartialOrder Inter] [PartialOrder Measure] {f : Source → Inter} {μ : Inter → Measure} (dc : DimensionChain f μ) : dc.toMereoMor = dc.leg₁ToMereoMor.comp dc.leg₂ToMereoMor

The composite morphism equals the categorical composition of the legs.