TauLib.Topos.WedgeProduct

Wedge product (coproduct) and the bi-monoidal structure of E_τ.

Registry Cross-References

• [I.D62] Categorical Coproduct — cat_coproduct

• [I.T27] Distributivity — product_distributes_over_coproduct

• [I.D63] Bi-Monoidal Structure — BiMonoidal

Mathematical Content

The categorical coproduct in E_τ is the pointwise disjunction of presheaves. The bi-monoidal structure has product (×) distributing over coproduct (∨).

Tau.Topos.cat_coproduct

source def Tau.Topos.cat_coproduct (P Q : Presheaf) :Presheaf

[I.D62] The categorical coproduct of two presheaves: pointwise disjunction of support predicates. Equations

• Tau.Topos.cat_coproduct P Q = Tau.Topos.presheaf_coproduct P Q Instances For

Tau.Topos.coprod_inl

source **theorem Tau.Topos.coprod_inl (P Q : Presheaf)

(x : Denotation.TauIdx) :P.support x = true → (cat_coproduct P Q).support x = true**

Left injection: P → P ∨ Q.

Tau.Topos.coprod_inr

source **theorem Tau.Topos.coprod_inr (P Q : Presheaf)

(x : Denotation.TauIdx) :Q.support x = true → (cat_coproduct P Q).support x = true**

Right injection: Q → P ∨ Q.

Tau.Topos.coproduct_comm

source theorem Tau.Topos.coproduct_comm (P Q : Presheaf) :(cat_coproduct P Q).support = (cat_coproduct Q P).support

Coproduct is commutative.

Tau.Topos.coproduct_assoc

source theorem Tau.Topos.coproduct_assoc (P Q R : Presheaf) :(cat_coproduct (cat_coproduct P Q) R).support = (cat_coproduct P (cat_coproduct Q R)).support

Coproduct is associative.

Tau.Topos.coproduct_initial

source theorem Tau.Topos.coproduct_initial (P : Presheaf) :(cat_coproduct P { support := fun (x : Denotation.TauIdx) => false }).support = P.support

Coproduct with initial is identity.

Tau.Topos.product_distributes_over_coproduct

source theorem Tau.Topos.product_distributes_over_coproduct (P Q R : Presheaf) :(cat_product P (cat_coproduct Q R)).support = (cat_coproduct (cat_product P Q) (cat_product P R)).support

[I.T27] Product distributes over coproduct: P × (Q ∨ R) = (P × Q) ∨ (P × R).

Tau.Topos.product_distributes_right

source theorem Tau.Topos.product_distributes_right (P Q R : Presheaf) :(cat_product (cat_coproduct P Q) R).support = (cat_coproduct (cat_product P R) (cat_product Q R)).support

Right distributivity: (P ∨ Q) × R = (P × R) ∨ (Q × R).

Tau.Topos.BiMonoidal

source structure Tau.Topos.BiMonoidal :Type

[I.D63] The bi-monoidal structure on E_τ: product (×) and coproduct (∨) with distributivity.

• times : Presheaf → Presheaf → Presheaf
• wedge : Presheaf → Presheaf → Presheaf
• one : Presheaf
• zero : Presheaf Instances For

Tau.Topos.bi_monoidal

source def Tau.Topos.bi_monoidal :BiMonoidal

The canonical bi-monoidal structure. Equations

• Tau.Topos.bi_monoidal = { } Instances For

Tau.Topos.product_absorb

source theorem Tau.Topos.product_absorb (P : Presheaf) :(cat_product P { support := fun (x : Denotation.TauIdx) => false }).support = { support := fun (x : Denotation.TauIdx) => false }.support

Absorption: P × 0 = 0.

Tau.Topos.coproduct_terminal

source theorem Tau.Topos.coproduct_terminal (P : Presheaf) :(cat_coproduct P { support := fun (x : Denotation.TauIdx) => true }).support = { support := fun (x : Denotation.TauIdx) => true }.support

Coproduct with terminal: P ∨ 1 = 1.