The forgetful projection from groups to monoids is a functor

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

Recorded description

CatS.forgetGrpMon is a CatS.FunctorLarge from CatS.grp to CatS.mon whose object map is AlgS.Group.toMonoidS and whose morphism map keeps the underlying function, and CatS.forgetGrpMon_isFunctor proves its three laws (mapCongr, mapId, mapComp) as CatS.IsFunctorLarge. The object map is free: every one of the eleven monoid fields is a group selector, though it is NOT a prefix projection -- monoid field 8 is assoc where group field 8 is inv, so indices 8, 9 and 10 of the monoid come from indices 10, 11 and 12 of the group. The morphism map's only real content is the third conjunct a monoid morphism carries and a group morphism does not, unit preservation, and that is exactly AlgS.Hom.mapOne.

Formal statement

theorem CatS.forgetGrpMon_isFunctor : CatS.IsFunctorLarge (CatS.FunctorLarge.src CatS.forgetGrpMon) (CatS.FunctorLarge.tgt CatS.forgetGrpMon) (CatS.FunctorLarge.obj CatS.forgetGrpMon) (CatS.FunctorLarge.map CatS.forgetGrpMon)

Dependencies

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

1 direct dependencies 0 direct dependents

Evidence

cats-forget-grp-mon-1

Kind: kernel-term
Status: checked

Supports: AlgS.Group.toMonoidS, CatS.FunctorLarge, CatS.IsFunctorLarge, CatS.functorLarge_isFunctor, CatS.forgetGrpMon and CatS.forgetGrpMon_isFunctor admit through the trusted Kernel::add_declaration gate with an empty Kernel::axiom_footprint. Read from the kernel by def_eq in both directions: forgetGrpMon.src IS CatS.grp and is NOT CatS.mon, forgetGrpMon.tgt IS CatS.mon and is NOT CatS.grp, forgetGrpMon.obj IS AlgS.Group.toMonoidS, and the forgotten morphism's underlying function is the SAME function (not the identity). All eleven fields of AlgS.Group.toMonoidS are checked against the group's own selector, each with a DIFFERENT group as the discriminating negative twin, including the three whose index moves.

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\. 29 passed; 0 failed')" -ge 1

Evidence notes

The pinned count is 29 and is RECOUNTED from the suite's own output. The two tests that carry this fact are groups_tests::the_forgetful_projection_is_the_group_s_own_fields and groups_tests::the_forgetful_functor_names_its_two_categories; the record's own universe is pinned at Sort 3 and refused at Sort 2 in groups_tests::the_types_render_and_pin_their_universes.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum-lean-kernel nat_prelude::category_setoid::groups, lane group-category, ADR-1626 (roadmap W3-3 residue).",
  "source": "crates/axeyum-lean-kernel/src/nat_prelude/category_setoid/groups.rs (declare_to_monoid_s, declare_forget_grp_mon); tests nat_prelude::category_setoid::groups::groups_tests::*."
}