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.

The inverse of a bijective group homomorphism is a group homomorphism

Statement

The inverse of a bijective group homomorphism is a group homomorphism.

If $f:G\to H$ is a bijective group homomorphism, then its set-theoretic inverse $f^{-1}:H\to G$ is a group homomorphism.

Facts & Assumptions

Given: A bijective group homomorphism $f:G\to H$ .

[L1]

An isomorphism is a bijective group homomorphism (Group isomorphisms, automorphisms and the set $\operatorname{Aut}(G)$ ).

[L2]

A group homomorphism preserves products, identities, and inverses (A group homomorphism automatically satisfies $f(e) = e'$ and $f(g^{-1}) = f(g)^{-1}$ , and $f(g^{n}) = f(g)^{n}$ for every $n \in \mathbb{Z}$ ; for monoid homomorphisms preservation of the identity must be assumed).

[L3]

A bijection has a two-sided set-theoretic inverse (Injection, surjection, bijection).

Proof

technique · direct

1.1

By [L3], for $u,v\in H$ choose $x,y\in G$ with $u=f(x)$ and $v=f(y)$ ; then $uv=f(xy)$ by [L2].

L1L2L3givenchoose

2.1

Therefore $f^{-1}(uv)=xy=f^{-1}(u)f^{-1}(v)$ , so the inverse preserves the group operation.

step 1.1L1L2L3givenalgebra

3.1

Hence $f^{-1}:H\to G$ is a group homomorphism.

step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 51 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

Ernst, An Inquiry-Based Approach to Abstract Algebra, Homomorphisms (standard reference, not scraped)