ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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.

For a field extension $K / F$ , one has $K \otimes_{F} M_{n} (F) ≅ M_{n} (K)$ as $K$ -algebras

Example

Let $K / F$ be a field extension and let $n$ be a natural number. Entrywise scalar extension gives an isomorphism of $K$ -algebras

$K \otimes_{F} M_{n} (F) ≅ M_{n} (K), k \otimes (a_{i j}) ⟼ (k a_{i j}) .$

The assertion includes $n = 0$ and $n = 1$ .

Facts & Assumptions

Given: A field extension $K / F$ and a natural number $n$ .

[L1]

The specified embedding $F \to K$ makes $K$ an extension field of $F$ (Field extensions, generated subrings $F [S]$ , generated subfields $F (S)$ , and simple extensions).

[L2]

$M_{n} (F)$ and $M_{n} (K)$ are the corresponding finite function spaces with entrywise vector-space operations; for $n = 0$ each is the zero space (The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations).

[L3]

For every field $E$ , $M_{n} (E)$ is a ring under matrix multiplication, including the one-element zero ring at $n = 0$ ( $M_{n} (F)$ is a ring under entrywise addition and matrix multiplication, including the zero ring $M_{0} (F)$ ).

[L4]

A prescription $Q (k \otimes A) : = q (k, A)$ extends to a homomorphism on $K \otimes_{F} M_{n} (F)$ if and only if $q$ is balanced, and the extension is then unique (A formula on elementary tensors defines a homomorphism exactly when its underlying pairing is balanced).

[L5]

Tensor products of algebras have multiplication $(a \otimes b) (a^{'} \otimes b^{'}) = a a^{'} \otimes b b^{'}$ (The tensor product of $R$ -algebras has multiplication $(a \otimes b) (a^{'} \otimes b^{'}) = a a^{'} \otimes b b^{'}$ ).

[L6]

Extension of scalars carries the $K$ -action $k^{'} (k \otimes m) = (k^{'} k) \otimes m$ , and an $F$ -scalar moves across a balanced tensor (Restriction of scalars and extension of scalars $S \otimes_{R} M$ along a ring homomorphism $R \to S$ ).

Verification

technique · direct

1.1

For $i, j < n$ , let $E_{i j}$ have entry $1$ at $(i, j)$ and $0$ elsewhere. Entrywise decomposition writes every $A \in M_{n} (F)$ uniquely as $A = \sum_{i, j < n} a_{i j} E_{i j}$ , so the $E_{i j}$ form an $F$ -basis; when $n = 0$ , this is the empty basis of the zero space.

givenL2

2.1

The pairing $(k, A) \mapsto (k a_{i j})$ is $F$ -balanced, so [L4] gives a unique additive $T : K \otimes_{F} M_{n} (F) \to M_{n} (K)$ with $T (k \otimes A) = (k a_{i j})$ , and $T$ is $K$ -linear by [L6]. Define $S : M_{n} (K) \to K \otimes_{F} M_{n} (F)$ by $S (B) = \sum_{i, j < n} b_{i j} \otimes E_{i j}$ , which is additive and $K$ -linear by [L6]. Then $T (S (B)) = \sum_{i, j < n} b_{i j} E_{i j} = B$ by step 1.1, and on a generator $S (T (k \otimes A)) = \sum_{i, j < n} k a_{i j} \otimes E_{i j} = \sum_{i, j < n} k \otimes a_{i j} E_{i j} = k \otimes A$ , moving each $F$ -scalar $a_{i j}$ across the balanced tensor by [L6] and using step 1.1. Both composites are additive and agree on generators, so $T$ and $S$ are mutually inverse and the displayed map is a $K$ -linear isomorphism.

step 1.1L1L2L4L6

2.2

Matrix multiplication gives $E_{i j} E_{ℓ r} = 0$ if $j \neq ℓ$ and $E_{i j} E_{j r} = E_{i r}$ . The displayed map preserves these products by [L5], and it sends $1 \otimes I_{n}$ to $I_{n}$ ; by bilinearity it is a unital algebra homomorphism.

step 1.1L3L5algebra

3.1

Combining steps 2.1 and 2.2 proves the algebra isomorphism. For $n = 0$ it is the unique map between one-element zero algebras, while for $n = 1$ it is the tensor-unit identification $K \otimes_{F} F ≅ K$ .

step 2.1step 2.2L2L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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

Wenqi Li, Commutative Algebra, Lecture 9 (standard reference, not scraped)

For a field extension K/FK/F, one has K⊗FMn(F)≅Mn(K)K⊗F​Mn​(F)≅Mn​(K) as KK-algebras