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

Restriction partitions embeddings in a finite tower into extension fibres

Statement

Let FKL be a finite tower and let Ω be an algebraic closure of F. Restriction defines a surjection

HomF(L,Ω)HomF(K,Ω).

For every F-embedding σ:KΩ, its fibre is nonempty and has cardinality [L:K]s after transporting the K-structure along σ.

Facts & Assumptions

Given: A finite tower FKL, an algebraic closure Ω/F, and an F-embedding σ:KΩ.

[L1]

Relative embeddings are field embeddings fixing the specified base map (F-homomorphisms and F-embeddings of field extensions).

[L2]

A finite extension has a finite basis over its base (The degree [K:F]=dimFK of a finite field extension).

[L4]

A chosen root of a transported irreducible polynomial induces the unique embedding of the corresponding simple root extension (Universal property of adjoining a root of an irreducible polynomial).

[L5]

Every nonconstant polynomial over an algebraically closed field has a root (An algebraically closed field: every nonconstant polynomial has a root in the field).

[L6]

For a finite extension, the number of base-field embeddings into an algebraic closure is independent of the chosen algebraic closure (The separable degree is independent of the chosen algebraic closure).

Proof

technique · direct
1.1

Restricting an F-embedding LΩ to K gives an F-embedding by [L1].

L1
1.2

To extend a chosen σ, take a finite K-basis a1,,ar of L by [L2] and put Ki=K(a1,,ai). Starting with τ0=σ, regard each τi1 as an isomorphism onto its image, transport the minimal polynomial of ai over Ki1 along it by [L3], choose a root in Ω by [L5], and extend τi1 to Ki by [L4]. After finitely many steps, Kr=L, so every σ has an extension and the restriction map is surjective.

L2L3L4L5construct
1.3

Identify K with σ(K). The extensions of σ are exactly the σ(K)-embeddings of the scalar-transported copy of L into Ω. Since Ω is algebraically closed and algebraic over σ(K), it is an algebraic closure of that copy of K.

L1algebra
2.1

Transporting scalars and maps along the isomorphism Kσ(K) identifies the embeddings in step 1.3 with embeddings of L/K into an algebraic closure of K. By [L6], their number is the closure-independent value [L:K]s. Thus every fibre of restriction has that cardinality.

step 1.3L6algebra
3.1

In particular, transport along an isomorphism between two embedded copies of K gives a bijection between their restriction fibres.

step 2.1

Depends on

Used by

Dependency tree · next 3 levels

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