Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Two elements have the same image under a homomorphism if and only if they lie in the same coset of its kernel

Statement

Two elements have the same image under a homomorphism if and only if they lie in the same coset of its kernel.

For a homomorphism f:G→Hf:G\to H and g,h∈Gg,h\in G,

f(g)=f(h)⟺gker⁡f=hker⁡f.f(g)=f(h)\quad\Longleftrightarrow\quad g\ker f=h\ker f.

Facts & Assumptions

Given: A group homomorphism f:G→Hf:G\to H and elements g,h∈Gg,h\in G.

[L1]

ker⁡f\ker f is the set of elements sent to eHe_H (The kernel and image of a group homomorphism).

[L2]

f(h−1g)=f(h)−1f(g)f(h^{-1}g)=f(h)^{-1}f(g) (A group homomorphism automatically satisfies f(e)=e′f(e) = e' and f(g−1)=f(g)−1f(g^{-1}) = f(g)^{-1}, and f(gn)=f(g)nf(g^{n}) = f(g)^{n} for every n∈Zn \in \mathbb{Z}; for monoid homomorphisms preservation of the identity must be assumed).

[L3]

For K≤GK\le G, gK=hKgK=hK if and only if h−1g∈Kh^{-1}g\in K (x∈aHx\in aH iff a−1x∈Ha^{-1}x\in H, and aH=bHaH=bH iff a−1b∈Ha^{-1}b\in H).

Proof

technique · direct
1.1

If f(g)=f(h)f(g)=f(h), then [L2] gives f(h−1g)=eHf(h^{-1}g)=e_H, so h−1g∈ker⁡fh^{-1}g\in\ker f and [L3] gives gker⁡f=hker⁡fg\ker f=h\ker f.

L1L2L3givenalgebra
2.1

If gker⁡f=hker⁡fg\ker f=h\ker f, then [L3] gives h−1g∈ker⁡fh^{-1}g\in\ker f, so f(h)−1f(g)=eHf(h)^{-1}f(g)=e_H and f(g)=f(h)f(g)=f(h).

step 1.1L1L2L3givenalgebra
3.1

This proves the stated equivalence.

step 1.1step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 47 results over 16 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources