Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-01
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.

Inversion induces a bijection gH↦Hg−1gH\mapsto Hg^{-1} from left cosets to right cosets

Statement

For H≤GH\le G, the rule

gH⟼Hg−1gH\longmapsto Hg^{-1}

is a well-defined bijection from the set of left cosets of HH to the set of right cosets of HH. Its inverse sends HgHg to g−1Hg^{-1}H.

Facts & Assumptions

Given: A group GG and a subgroup H≤GH\le G.

[L1]

For left cosets, gH=kHgH=kH if and only if g−1k∈Hg^{-1}k\in H; for right cosets, Hg=HkHg=Hk if and only if gk−1∈Hgk^{-1}\in H (x∈aHx\in aH iff a−1x∈Ha^{-1}x\in H, and aH=bHaH=bH iff a−1b∈Ha^{-1}b\in H).

[L2]

In a group, (uv)−1=v−1u−1(uv)^{-1}=v^{-1}u^{-1} and (u−1)−1=u(u^{-1})^{-1}=u (In a group e−1=ee^{-1} = e, (g−1)−1=g(g^{-1})^{-1} = g and (gh)−1=h−1g−1(gh)^{-1} = h^{-1}g^{-1}, the order of the last product being essential).

[L3]

A subgroup is closed under inverses (Subgroup).

[F1]

A map with a two-sided inverse is a bijection (Injection, surjection, bijection, Equinumerous sets, A≈BA \approx B and A⪯BA \preceq B).

Proof

technique · direct
1.1

If gH=kHgH=kH, then g−1k∈Hg^{-1}k\in H by [L1], so (g−1k)−1=k−1g∈H(g^{-1}k)^{-1}=k^{-1}g\in H by subgroup inverse closure. The right-coset criterion gives Hg−1=Hk−1Hg^{-1}=Hk^{-1}, so the rule is well defined.

givenL1L2L3
1.2

Define the reverse rule by Hg↦g−1HHg\mapsto g^{-1}H. The same argument, with left and right interchanged, shows that it is well defined.

L1L2
2.1

The two composites send gHgH to (g−1)−1H=gH(g^{-1})^{-1}H=gH and HgHg to H(g−1)−1=HgH(g^{-1})^{-1}=Hg. Thus the rules are inverse bijections.

step 1.1step 1.2L2F1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 22 results over 13 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