Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
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.

Core⁡G(H)\operatorname{Core}_G(H) is the largest normal subgroup of GG contained in HH

Statement

For H≤GH\le G, the core K=Core⁡G(H)K=\operatorname{Core}_G(H) is a normal subgroup of GG, satisfies K≤HK\le H, and contains every normal subgroup of GG that is contained in HH. Thus it is the largest normal subgroup of GG contained in HH.

Facts & Assumptions

Given: A group GG, a subgroup H≤GH\le G, and K:=Core⁡G(H)K:=\operatorname{Core}_G(H).

[L1]

The core is K=⋂g∈GgHg−1K=\bigcap_{g\in G}gHg^{-1} (The core Core⁡G(H)=⋂g∈GgHg−1\operatorname{Core}_G(H)=\bigcap_{g\in G}gHg^{-1} of a subgroup).

[L2]

A subgroup NN is normal when gNg−1=NgNg^{-1}=N for every g∈Gg\in G (Normal subgroup: invariance under conjugation).

[L3]

Normality is equivalent to gNg−1⊆NgNg^{-1}\subseteq N for every g∈Gg\in G (Equivalent characterisations of a normal subgroup by conjugates and left and right cosets).

[L4]

A nonempty subset SS of a group is a subgroup if ab−1∈Sab^{-1}\in S for every a,b∈Sa,b\in S (One-step subgroup test: a nonempty H⊆GH \subseteq G is a subgroup iff gh−1∈Hgh^{-1} \in H for all g,h∈Hg, h \in H; the identity and the inverses of HH are then those of GG).

Proof

technique · direct
1.1

The identity belongs to every gHg−1gHg^{-1}, and if a,ba,b belong to every such conjugate then ab−1ab^{-1} does too; [L4] makes KK a subgroup. The factor for g=eg=e is HH, so K≤HK\le H.

L1L4
1.2

For t∈Gt\in G, conjugation sends the family {gHg−1:g∈G}\{gHg^{-1}:g\in G\} to {(tg)H(tg)−1:g∈G}\{(tg)H(tg)^{-1}:g\in G\}, the same family because g↦tgg\mapsto tg is a bijection; hence tKt−1=KtKt^{-1}=K, and [L2] gives K⊴GK\mathrel{\trianglelefteq}G.

L1L2L3
2.1

If N⊴GN\mathrel{\trianglelefteq}G and N≤HN\le H, then N=gNg−1≤gHg−1N=gNg^{-1}\le gHg^{-1} for every g∈Gg\in G, so N≤⋂ggHg−1=KN\le\bigcap_g gHg^{-1}=K.

L1L2L3∎

Depends on

Used by

Cited to discharge well-definedness by The core Core_G(H)=⋂_g∈ GgHg⁻¹ of a subgroup.

Dependency tree · next 3 levels

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