4.1. Relative pushouts🔗

Definition4.1.1

uses 0

Used by 3

Reverse dependency previews

Preview

Theorem 4.1.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsfrom source

In a precategory, composition is partial, and an equation between composites asserts that both are defined. A bound for a span f_0, f_1 is a pair with g_0 \circ f_0 = g_1 \circ f_1. A relative pushout (RPO) for \vec f relative to a bound \vec g is a triple (h_0, h_1, h) with \vec h a bound and h \circ h_i = g_i, having a unique mediating arrow to every other such triple. The bound \vec h is an idem pushout, \mathrm{IPO}(f_0, f_1; h_0, h_1), when (\vec h, \mathrm{id}) is an RPO relative to \vec h.

Lean code for Definition4.1.1●4 definitions

structure(8 fields)defined in Bigraph/Concrete/PreCat.lean

complete

structure PreCat.{u, v} : Type (max (u + 1) (v + 1))

structure PreCat.{u, v} : Type (max (u + 1) (v + 1))

**A precategory** (TR-580 Def 3.1).

Fields

Obj : Type u

Hom : self.Obj → self.Obj → Type v

id : (a : self.Obj) → self.Hom a a

Comp : {a b c : self.Obj} → self.Hom b c → self.Hom a b → self.Hom a c → Prop

`g ∘ f` is defined and is `h`.

comp_fun : ∀ {a b c : self.Obj} {g : self.Hom b c} {f : self.Hom a b} {h h' : self.Hom a c}, g ◦ f ≃ h → g ◦ f ≃ h' → h = h'

id_left : ∀ {a b : self.Obj} (f : self.Hom a b), self.id b ◦ f ≃ f

id_right : ∀ {a b : self.Obj} (f : self.Hom a b), f ◦ self.id a ≃ f

assoc : ∀ {a b c d : self.Obj} (f : self.Hom a b) (g : self.Hom b c) (h : self.Hom c d) (x : self.Hom a d),
  (∃ gf, g ◦ f ≃ gf ∧ h ◦ gf ≃ x) ↔ ∃ hg, h ◦ g ≃ hg ∧ hg ◦ f ≃ x

defdefined in Bigraph/Concrete/PreCat.lean

complete

def IsBound.{u, v} (𝒞 : PreCat) {H I₀ I₁ K : 𝒞.Obj} (f₀ : 𝒞.Hom H I₀)
  (f₁ : 𝒞.Hom H I₁) (g₀ : 𝒞.Hom I₀ K) (g₁ : 𝒞.Hom I₁ K) : Prop

def IsBound.{u, v} (𝒞 : PreCat)
  {H I₀ I₁ K : 𝒞.Obj} (f₀ : 𝒞.Hom H I₀)
  (f₁ : 𝒞.Hom H I₁) (g₀ : 𝒞.Hom I₀ K)
  (g₁ : 𝒞.Hom I₁ K) : Prop

**A bound** for the pair `(f₀, f₁)` (TR-580 Def 3.7): a pair `(g₀, g₁)` with
`g₀ ∘ f₀ = g₁ ∘ f₁`, both composites defined.

defdefined in Bigraph/Concrete/PreCat.lean

complete

def IsRPO.{u, v} (𝒞 : PreCat) {H I₀ I₁ K : 𝒞.Obj} {f₀ : 𝒞.Hom H I₀}
  {f₁ : 𝒞.Hom H I₁} {g₀ : 𝒞.Hom I₀ K} {g₁ : 𝒞.Hom I₁ K}
  (b : 𝒞.RelBound f₀ f₁ g₀ g₁) : Prop

def IsRPO.{u, v} (𝒞 : PreCat)
  {H I₀ I₁ K : 𝒞.Obj} {f₀ : 𝒞.Hom H I₀}
  {f₁ : 𝒞.Hom H I₁} {g₀ : 𝒞.Hom I₀ K}
  {g₁ : 𝒞.Hom I₁ K}
  (b : 𝒞.RelBound f₀ f₁ g₀ g₁) : Prop

**An RPO** (TR-580 Def 3.8): a relative bound with a unique mediator to
every other.

defdefined in Bigraph/Concrete/PreCat.lean

complete

def IsIPO.{u, v} (𝒞 : PreCat) {H I₀ I₁ J : 𝒞.Obj} (f₀ : 𝒞.Hom H I₀)
  (f₁ : 𝒞.Hom H I₁) (h₀ : 𝒞.Hom I₀ J) (h₁ : 𝒞.Hom I₁ J) : Prop

def IsIPO.{u, v} (𝒞 : PreCat)
  {H I₀ I₁ J : 𝒞.Obj} (f₀ : 𝒞.Hom H I₀)
  (f₁ : 𝒞.Hom H I₁) (h₀ : 𝒞.Hom I₀ J)
  (h₁ : 𝒞.Hom I₁ J) : Prop

**An IPO** (TR-580 Def 3.9): the pair `(h₀, h₁)`, with the identity, is an
RPO for `(f₀, f₁)` relative to `(h₀, h₁)`.

Theorem4.1.2

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 4.1.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

IPOs paste, and the right square of a pasted IPO is an IPO. Let the composites F \circ C, E \circ D', C \circ a be defined and let (a, l) have an RPO relative to (F \circ C, E \circ D'). If the rectangle commutes, F \circ (C \circ a) = (E \circ D') \circ l, then

\mathrm{IPO}(a, l; F', D') \;\wedge\; \mathrm{IPO}(C, F'; F, E) \;\Longrightarrow\; \mathrm{IPO}(C \circ a, l; F, E \circ D') ,

and if the right square commutes, F \circ C = E \circ F', then

\mathrm{IPO}(C \circ a, l; F, E \circ D') \;\wedge\; \mathrm{IPO}(a, l; F', D') \;\Longrightarrow\; \mathrm{IPO}(C, F'; F, E) .

Lean code for Theorem4.1.2●2 theorems

theoremdefined in Bigraph/Concrete/Paste.lean

complete

theorem ipo_paste.{u, v} {𝒞 : PreCat} {k m m₂ m' n' n : 𝒞.Obj} {a : 𝒞.Hom k m}
  {l : 𝒞.Hom k m'} {C : 𝒞.Hom m m₂} {F' : 𝒞.Hom m n'} {F : 𝒞.Hom m₂ n}
  {D' : 𝒞.Hom m' n'} {E : 𝒞.Hom n' n} {FC : 𝒞.Hom m n}
  {ED' : 𝒞.Hom m' n} {Ca : 𝒞.Hom k m₂} (hFC : F ◦ C ≃ FC)
  (hED : E ◦ D' ≃ ED') (hCa : C ◦ a ≃ Ca) (hrc : 𝒞.IsBound Ca l F ED')
  (P : 𝒞.RelBound a l FC ED') (hP : 𝒞.IsRPO P)
  (hleft : 𝒞.IsIPO a l F' D') (hright : 𝒞.IsIPO C F' F E) :
  𝒞.IsIPO Ca l F ED'

theorem ipo_paste.{u, v} {𝒞 : PreCat}
  {k m m₂ m' n' n : 𝒞.Obj} {a : 𝒞.Hom k m}
  {l : 𝒞.Hom k m'} {C : 𝒞.Hom m m₂}
  {F' : 𝒞.Hom m n'} {F : 𝒞.Hom m₂ n}
  {D' : 𝒞.Hom m' n'} {E : 𝒞.Hom n' n}
  {FC : 𝒞.Hom m n} {ED' : 𝒞.Hom m' n}
  {Ca : 𝒞.Hom k m₂} (hFC : F ◦ C ≃ FC)
  (hED : E ◦ D' ≃ ED') (hCa : C ◦ a ≃ Ca)
  (hrc : 𝒞.IsBound Ca l F ED')
  (P : 𝒞.RelBound a l FC ED')
  (hP : 𝒞.IsRPO P)
  (hleft : 𝒞.IsIPO a l F' D')
  (hright : 𝒞.IsIPO C F' F E) :
  𝒞.IsIPO Ca l F ED'

**Prop 3.10(4a), IPO pasting**: in the diagram

    k --a--> m --C--> m₂
    |l       |F'      |F
    m' -D'-> n' --E--> n

if the diagram commutes (`hrc`: the rectangle, `F ∘ (C ∘ a) = (E ∘ D') ∘ l`
with both sides defined), both squares are IPOs, and the left square's
span `(a, l)` has an RPO relative to the outer bound `(F ∘ C, E ∘ D')`,
then the rectangle is an IPO.  TR-580 assumes the commuting ("suppose that
the diagram below commutes"); without it the statement is false in a
precategory (`PasteCounter.ipo_paste_needs_commuting` below).
`isBound_rect_of_isBound` supplies `hrc` when `(F ∘ C, E ∘ D')` bounds
`(a, l)`, the presupposition of Def 3.8.

theoremdefined in Bigraph/Concrete/Paste.lean

complete

theorem ipo_unpaste.{u, v} {𝒞 : PreCat} {k m m₂ m' n' n : 𝒞.Obj} {a : 𝒞.Hom k m}
  {l : 𝒞.Hom k m'} {C : 𝒞.Hom m m₂} {F' : 𝒞.Hom m n'} {F : 𝒞.Hom m₂ n}
  {D' : 𝒞.Hom m' n'} {E : 𝒞.Hom n' n} {FC : 𝒞.Hom m n}
  {ED' : 𝒞.Hom m' n} {Ca : 𝒞.Hom k m₂} (hFC : F ◦ C ≃ FC)
  (hED : E ◦ D' ≃ ED') (hCa : C ◦ a ≃ Ca) (P : 𝒞.RelBound a l FC ED')
  (hP : 𝒞.IsRPO P) (hrect : 𝒞.IsIPO Ca l F ED')
  (hleft : 𝒞.IsIPO a l F' D') (hcomm : 𝒞.IsBound C F' F E) :
  𝒞.IsIPO C F' F E

theorem ipo_unpaste.{u, v} {𝒞 : PreCat}
  {k m m₂ m' n' n : 𝒞.Obj} {a : 𝒞.Hom k m}
  {l : 𝒞.Hom k m'} {C : 𝒞.Hom m m₂}
  {F' : 𝒞.Hom m n'} {F : 𝒞.Hom m₂ n}
  {D' : 𝒞.Hom m' n'} {E : 𝒞.Hom n' n}
  {FC : 𝒞.Hom m n} {ED' : 𝒞.Hom m' n}
  {Ca : 𝒞.Hom k m₂} (hFC : F ◦ C ≃ FC)
  (hED : E ◦ D' ≃ ED') (hCa : C ◦ a ≃ Ca)
  (P : 𝒞.RelBound a l FC ED')
  (hP : 𝒞.IsRPO P)
  (hrect : 𝒞.IsIPO Ca l F ED')
  (hleft : 𝒞.IsIPO a l F' D')
  (hcomm : 𝒞.IsBound C F' F E) :
  𝒞.IsIPO C F' F E

**Prop 3.10(4b)**: if the rectangle and the left square are IPOs, so is
the right square, given the same RPO and that the right square commutes.

Theorem4.1.3

uses 1used by 0✓L∃∀N

REFUTED: pasting without the hypothesis that the rectangle commutes. There is a precategory with the remaining hypotheses of the first implication in which

\mathrm{IPO}(a, l; F', D') \;\wedge\; \mathrm{IPO}(C, F'; F, E) \;\text{ but not }\; \mathrm{IPO}(C \circ a, l; F, E \circ D') .

Lean code for Theorem4.1.3●1 theorem

theoremdefined in Bigraph/Concrete/Paste.lean

complete

theorem ipo_paste_needs_commuting :
  ¬∀ (𝒞 : PreCat) {k m m₂ m' n' n : 𝒞.Obj} {a : 𝒞.Hom k m}
      {l : 𝒞.Hom k m'} {C : 𝒞.Hom m m₂} {F' : 𝒞.Hom m n'}
      {F : 𝒞.Hom m₂ n} {D' : 𝒞.Hom m' n'} {E : 𝒞.Hom n' n}
      {FC : 𝒞.Hom m n} {ED' : 𝒞.Hom m' n} {Ca : 𝒞.Hom k m₂},
      F ◦ C ≃ FC →
        E ◦ D' ≃ ED' →
          C ◦ a ≃ Ca →
            ∀ (P : 𝒞.RelBound a l FC ED'),
              𝒞.IsRPO P →
                𝒞.IsIPO a l F' D' →
                  𝒞.IsIPO C F' F E → 𝒞.IsIPO Ca l F ED'

theorem ipo_paste_needs_commuting :
  ¬∀ (𝒞 : PreCat) {k m m₂ m' n' n : 𝒞.Obj}
      {a : 𝒞.Hom k m} {l : 𝒞.Hom k m'}
      {C : 𝒞.Hom m m₂} {F' : 𝒞.Hom m n'}
      {F : 𝒞.Hom m₂ n} {D' : 𝒞.Hom m' n'}
      {E : 𝒞.Hom n' n} {FC : 𝒞.Hom m n}
      {ED' : 𝒞.Hom m' n}
      {Ca : 𝒞.Hom k m₂},
      F ◦ C ≃ FC →
        E ◦ D' ≃ ED' →
          C ◦ a ≃ Ca →
            ∀ (P : 𝒞.RelBound a l FC ED'),
              𝒞.IsRPO P →
                𝒞.IsIPO a l F' D' →
                  𝒞.IsIPO C F' F E →
                    𝒞.IsIPO Ca l F ED'

**`ipo_paste` needs its commuting hypothesis**: with it left out, every
other hypothesis holds in `M`, but the rectangle is not even a bound, as
there is no arrow `k → n`.  This refutes a first transcription that
dropped the hypothesis.  TR-580 Prop 3.10(4) has it ("suppose that the
diagram below commutes"), so it is not an erratum of TR-580.

Definition4.1.4

uses 0

Used by 4

Reverse dependency previews

Preview

Theorem 4.1.5

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsfrom sourcenewnot audited

A concrete bigraph G : I \to J is a place graph and a link graph on the same nodes, the nodes and edges being natural numbers; its support is the set of its nodes and edges. H \circ G is defined exactly when the supports are disjoint. A permutation \pi of the supply translates a bigraph, \pi \bullet G; G \bumpeq H when one is a translate of the other, and G \Bumpeq H when this holds after discarding idle edges.

Class: Big, BIG not audited; Big.LeanEquiv FROM SOURCE and NEW.

Lean code for Definition4.1.4●3 definitions

structure(3 fields)defined in Bigraph/Concrete/Big.lean

complete

structure Big {Ctrl : Type} (S : Bigraph.Sig Ctrl) (I J : Face) : Type

structure Big {Ctrl : Type} (S : Bigraph.Sig Ctrl)
  (I J : Face) : Type

**A concrete pure bigraph** `I → J` (TR-580 Def 9.1): a place graph and a link graph
on the same nodes, with the same controls.

Fields

P : PlG S I.width J.width

The place graph `G^P : m → n`.

L : LiG S I.names J.names

The link graph `G^L : X → Y`.

ctrl_eq : self.P.ctrl = self.L.ctrl

The same nodes, with the same controls.

defdefined in Bigraph/Concrete/Big.lean

complete

def BIG {Ctrl : Type} (S : Bigraph.Sig Ctrl) : PreCat

def BIG {Ctrl : Type} (S : Bigraph.Sig Ctrl) :
  PreCat

**The precategory ´BIG** (TR-580 Def 9.1).

defdefined in Bigraph/Concrete/BigLean.lean

complete

def LeanEquiv {Ctrl : Type} {S : Bigraph.Sig Ctrl} {I J : Face}
  (A B : Big S I J) : Prop

def LeanEquiv {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} {I J : Face}
  (A B : Big S I J) : Prop

**Lean-support equivalence** `A ≎ B` (TR-580 Def 9.12): after discarding
idle edges, one is a translation of the other.

Theorem4.1.5

Statement uses 2

Statement dependency previews

Preview

Definition 4.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Concrete place graphs, concrete link graphs and concrete bigraphs have RPOs (TR-580 Thms 7.8, 8.9, Cor 9.6): for A_i : I \to I_i and D_i : I_i \to K,

D_0 \circ A_0 = D_1 \circ A_1 \;\Longrightarrow\; \exists\, (B_0, B_1, B) \text{ an RPO for } \vec A \text{ relative to } \vec D .

Rests on not audited: BIG, Big, LIG, LiG, PLG, PlG.

Lean code for Theorem4.1.5●3 theorems

theoremdefined in Bigraph/Concrete/PlaceRPOMain.lean

complete

theorem plg_rpo {Ctrl : Type} {S : Bigraph.Sig Ctrl} {ℓ m₀ m₁ p : Nat}
  (A₀ : PlG S ℓ m₀) (A₁ : PlG S ℓ m₁) (D₀ : PlG S m₀ p)
  (D₁ : PlG S m₁ p) (hD : (PLG S).IsBound A₀ A₁ D₀ D₁) :
  ∃ b, (PLG S).IsRPO b

theorem plg_rpo {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} {ℓ m₀ m₁ p : Nat}
  (A₀ : PlG S ℓ m₀) (A₁ : PlG S ℓ m₁)
  (D₀ : PlG S m₀ p) (D₁ : PlG S m₁ p)
  (hD : (PLG S).IsBound A₀ A₁ D₀ D₁) :
  ∃ b, (PLG S).IsRPO b

**TR-580 Theorem 7.8 (RPOs in place graphs)**: whenever a pair of
concrete place graphs has a bound, it has an RPO relative to that bound,
and Construction 7.7 builds one.

theoremdefined in Bigraph/Concrete/LinkRPOMain.lean

complete

theorem lig_rpo {Ctrl : Type} {S : Bigraph.Sig Ctrl} {W X₀ X₁ Z : NSet}
  (A₀ : LiG S W X₀) (A₁ : LiG S W X₁) (D₀ : LiG S X₀ Z)
  (D₁ : LiG S X₁ Z) (hD : (LIG S).IsBound A₀ A₁ D₀ D₁) :
  ∃ b, (LIG S).IsRPO b

theorem lig_rpo {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  {W X₀ X₁ Z : NSet} (A₀ : LiG S W X₀)
  (A₁ : LiG S W X₁) (D₀ : LiG S X₀ Z)
  (D₁ : LiG S X₁ Z)
  (hD : (LIG S).IsBound A₀ A₁ D₀ D₁) :
  ∃ b, (LIG S).IsRPO b

**TR-580 Theorem 8.9 (RPOs in link graphs)**: whenever a pair of
concrete link graphs has a bound, it has an RPO relative to that bound,
and Construction 8.8 builds one.

theoremdefined in Bigraph/Concrete/BigCongr.lean

complete

theorem big_rpo {Ctrl : Type} {S : Bigraph.Sig Ctrl} {I I₀ I₁ K : Face}
  (A₀ : Big S I I₀) (A₁ : Big S I I₁) (D₀ : Big S I₀ K)
  (D₁ : Big S I₁ K) (hD : (BIG S).IsBound A₀ A₁ D₀ D₁) :
  ∃ b, (BIG S).IsRPO b

theorem big_rpo {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  {I I₀ I₁ K : Face} (A₀ : Big S I I₀)
  (A₁ : Big S I I₁) (D₀ : Big S I₀ K)
  (D₁ : Big S I₁ K)
  (hD : (BIG S).IsBound A₀ A₁ D₀ D₁) :
  ∃ b, (BIG S).IsRPO b

**TR-580 Corollary 9.6 (RPOs for bigraphs)**: whenever a pair of concrete
pure bigraphs has a bound, it has an RPO relative to that bound
(`Big.rpo`, as an `∃`).