The product of two groups is a categorical product in CatS.grp, and it costs no congruence bookkeeping

Identifier: F:cats-grp-product
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For any two AlgS.Groups G and H, CatS.grpProd G H is an AlgS.Group whose carrier is Sigma.{0,0} G.carrier (fun _ => H.carrier), whose equiv is the conjunction of the two component equivs, and whose op, e and inv are componentwise; CatS.grpProdFst G H and CatS.grpProdSnd G H are the two Subtype-bundled projections; CatS.grpProdMed G H X u v is the bundled pairing; and CatS.grp_isProduct proves CatS.IsProductLarge CatS.grp G H (CatS.grpProd G H) with those three as its projections and mediating family. The setoid price is measured and is the lowest in this layer: all TEN law fields of the product object are literally And.intro (G.law ...) (H.law ...) with no congruence bookkeeping at all, because the product setoid's equiv IS the conjunction of the two component equivs; and BOTH triangles of grp_isProduct are equivRefl, free because pr1 . (pairing f g) unfolds to fun x => Sigma.fst (Sigma.mk (f x) (g x)) and Sigma.fst ι-reduces on a Sigma.mk. Uniqueness is one And.intro for the same reason.

Formal statement

theorem CatS.grp_isProduct : ((x0 : AlgS.Group) -> ((x1 : AlgS.Group) -> CatS.IsProductLarge CatS.grp x0 x1 (CatS.grpProd x0 x1) (CatS.grpProdFst x0 x1) (CatS.grpProdSnd x0 x1) (CatS.grpProdMed x0 x1)))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

2 direct dependencies 0 direct dependents

Evidence

cats-grp-product-1

Kind: kernel-term
Status: checked

Supports: CatS.grpProd, CatS.grpProdFst, CatS.grpProdSnd, CatS.grpProdMed and CatS.grp_isProduct admit through the trusted Kernel::add_declaration gate with an empty Kernel::axiom_footprint, asserted after Environment::contains; grp_isProduct is read back from the environment as a Declaration::Theorem. Every Definition carries an evaluation test at CONCRETE, discriminating, SMALL arguments: two groups on a Nat carrier whose equiv is the total relation (so every law field is True.intro and the operations are free to differ) with op a b = a / op a b = b, e = 0 / e = 1, and inv a = a / inv a = a+1. Measured: op (1,2) (3,4) IS (1,4) and is NOT (3,2), (1,2), (3,4) or (4,1); e IS (0,1) and is NOT (1,0); inv (1,2) IS (1,3) and is NOT (2,2), (1,2) or (3,1); grpProdFst applied to (1,2) IS 1 and is NOT 2, and grpProdSnd IS 2 and is NOT 1. Symbolically: the mediating map's underlying function at x IS (u x, v x) and is NOT a pairing that drops v; each triangle's composite ι-reduces to its OWN component morphism and NOT to the other's; and the product's equiv IS the conjunction of the two component equivs and is NOT the first conjunct alone.

Checker command

out=$(RUST_MIN_STACK=1073741824 cargo test -p axeyum-lean-kernel --lib --release category_setoid -- --test-threads=4 2>&1) && test "$(printf "%s\n" "$out" | grep -cE 'test result: ok\. 41 passed; 0 failed')" -ge 1

Evidence notes

The pinned count is 41, RECOUNTED from the suite's own output. The tests that carry this fact are products_tests::the_product_group_computes_componentwise, products_tests::the_projections_read_their_own_component, products_tests::the_mediating_map_is_the_pairing, products_tests::the_group_products_triangles_are_free_by_iota and products_tests::the_group_products_uniqueness_conjunct_is_pointwise. The two chaotic groups exist so that a component SWAP type-checks at all: with two distinct symbolic groups the kernel's dependent typing refuses a swap outright, so the concrete fixture is the only place a swap can be observed rather than rejected.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum-lean-kernel nat_prelude::category_setoid::products, lane cat-products, ADR-1632 (roadmap W3-4).",
  "source": "crates/axeyum-lean-kernel/src/nat_prelude/category_setoid/products.rs (declare_grp_prod, declare_grp_prod_proj, declare_grp_prod_med, declare_grp_is_product); tests nat_prelude::category_setoid::products::products_tests::*."
}