The kernel of a homomorphism of abstract Setoid-flavored groups is a subgroup

Identifier: F:algs-subgroup-ker
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For any two AlgS.Group records G and H, any f : G.carrier -> H.carrier, any proof fCongr that f respects the two equivalences, and any proof fMul that f carries G.op to H.op, AlgS.Subgroup.IsSub G (AlgS.Hom.ker G H f). A subgroup is a PREDICATE on the carrier, not a carrier: this kernel has no Subtype and no Sigma. IsSub bundles four conjuncts -- that S is closed under G.equiv (forall a b, G.equiv a b -> S a -> S b), that S holds at G.e, that S is closed under G.op, and that S is closed under G.inv. The first is the obligation the setoid presentation adds and an Eq-flavored one would get free from Eq.subst; here it is discharged by fCongr symm'd and composed. The remaining three are AlgS.Hom.mapOne verbatim, fMul followed by H.opCongr and H.identL, and AlgS.Hom.mapInv followed by H.invCongr and the derivation of H.equiv (H.inv H.e) H.e.

Formal statement

theorem AlgS.Subgroup.ker_isSub : ((x0 : AlgS.Group) -> ((x1 : AlgS.Group) -> ((x2 : ((x2 : AlgS.Group.carrier x0) -> AlgS.Group.carrier x1)) -> ((x3 : ((x3 : AlgS.Group.carrier x0) -> ((x4 : AlgS.Group.carrier x0) -> ((x5 : AlgS.Group.equiv x0 x3 x4) -> AlgS.Group.equiv x1 (x2 x3) (x2 x4))))) -> ((x4 : ((x4 : AlgS.Group.carrier x0) -> ((x5 : AlgS.Group.carrier x0) -> AlgS.Group.equiv x1 (x2 (AlgS.Group.op x0 x4 x5)) (AlgS.Group.op x1 (x2 x4) (x2 x5))))) -> AlgS.Subgroup.IsSub x0 (AlgS.Hom.ker x0 x1 x2))))))

Dependencies

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

2 direct dependencies 0 direct dependents

Evidence

algs-subgroup-ker-1

Kind: kernel-term
Status: checked

Supports: AlgS.Subgroup.ker_isSub and the nineteen other AlgS.Subgroup.* declarations (IsSub, le, inter, top, bot, the four accessors, le_refl, le_trans, inter_le_left, inter_le_right, le_inter, inter_isSub, top_isSub, bot_isSub, le_top, bot_le) admit through the trusted Kernel::add_declaration gate with an empty Kernel::axiom_footprint. Three rejection controls, each with a positive twin in the same test: IsSub is refused as definitionally equal to the three-conjunct Eq-flavored form with `respects` dropped; bot_le's proof term is refused against the statement with its IsSub hypothesis removed; and ker_isSub's own proof term is refused against the claim that AlgS.Hom.image is a subgroup of the SOURCE group.

Checker command

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

Evidence notes

The pinned count is 8. is_sub_carries_the_equivalence_respecting_conjunct is what makes the 'one extra field over Eq' measurement in ADR-1609 a kernel reading rather than a comment.

Provenance

{
  "date": "2026-09-04",
  "established_by": "axeyum-lean-kernel nat_prelude::subgroup_setoid, lane algebra-structures, ADR-1609 (roadmap W1-11, subobject half).",
  "source": "crates/axeyum-lean-kernel/src/nat_prelude/subgroup_setoid.rs (declare_ker_is_sub, declared as AlgS.Subgroup.ker_isSub); tests nat_prelude::subgroup_setoid::subgroup_setoid_tests::*."
}