TauLib.Topos.CartesianProduct

Cartesian product as an earned bi-functor in E_τ.

Registry Cross-References

• [I.D60] Categorical Product — cat_product

• [I.T26] Product Universal Property — product_universal

• [I.D61] Cartesian Monoidal Structure — CartesianMonoidal

Mathematical Content

The categorical product in E_τ is the pointwise conjunction of presheaves. The terminal presheaf is the monoidal unit. Products satisfy the universal property: any pair of morphisms factors uniquely through the product.

Tau.Topos.cat_product

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

[I.D60] The categorical product of two presheaves: pointwise conjunction of support predicates. Equations

• Tau.Topos.cat_product P Q = Tau.Topos.presheaf_product P Q Instances For

Tau.Topos.cat_proj1

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

(x : Denotation.TauIdx)

(h : (cat_product P Q).support x = true) :P.support x = true**

First projection: product → first factor.

Tau.Topos.cat_proj2

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

(x : Denotation.TauIdx)

(h : (cat_product P Q).support x = true) :Q.support x = true**

Second projection: product → second factor.

Tau.Topos.product_universal

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

(hP : ∀ (x : Denotation.TauIdx), R.support x = true → P.support x = true)

(hQ : ∀ (x : Denotation.TauIdx), R.support x = true → Q.support x = true)

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

[I.T26] Product universal property: if R maps to both P and Q pointwise, then R maps to P × Q.

Tau.Topos.product_comm

source theorem Tau.Topos.product_comm (P Q : Presheaf) :(cat_product P Q).support = (cat_product Q P).support

Product is commutative up to support equality.

Tau.Topos.product_assoc

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

Product is associative up to support equality.

Tau.Topos.product_terminal

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

Product with terminal is identity.

Tau.Topos.CartesianMonoidal

source structure Tau.Topos.CartesianMonoidal :Type

[I.D61] The cartesian monoidal structure on E_τ. Unit: terminal presheaf. Tensor: pointwise product.

• unit : Presheaf
• tensor : Presheaf → Presheaf → Presheaf Instances For

Tau.Topos.cartesian_monoidal

source def Tau.Topos.cartesian_monoidal :CartesianMonoidal

The canonical cartesian monoidal structure. Equations

• Tau.Topos.cartesian_monoidal = { } Instances For

Tau.Topos.monoidal_left_unit

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

Left unit law.

Tau.Topos.monoidal_right_unit

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

Right unit law.

Tau.Topos.cantor_product_encoding

source theorem Tau.Topos.cantor_product_encoding (a b : Denotation.TauIdx) :cantor_pair a b = (a + b) * (a + b + 1) / 2 + b

Product encoding at the object level via Cantor pairing.