The Skolem-Noether theorem

Let K be a field, let A be a finite-dimensional simple K-algebra and let B be a finite-dimensional central simple K-algebra. The Skolem-Noether theorem says that two K-algebra homomorphisms f g : B →ₐ[K] A differ by conjugation: there is a unit u of A with g x = u * f x * u⁻¹ for every x. Taking B = A and f the identity, every K-algebra automorphism of a finite-dimensional central simple algebra is inner.

The proof is the classical module-theoretic one. A homomorphism f : B →ₐ[K] A makes A into a module over R = B ⊗[K] Aᵐᵒᵖ, with B acting on the left through f and A on the right by multiplication; this is TauCeti.Bimodule f. Because B is central simple and Aᵐᵒᵖ is simple, R is a simple ring (TauCeti.IsSimpleRing.tensorProduct), and it is finite-dimensional over K, hence Artinian. The two modules Bimodule f and Bimodule g are carried by one and the same K-vector space A, so they have equal dimension, so they are isomorphic R-modules (TauCeti.IsSimpleRing.nonempty_linearEquiv_of_finrank_eq). An R-linear isomorphism is in particular linear for the right action of A, hence is multiplication on the left by the unit u = φ 1, and its linearity for the left action of B is exactly u * f x = g x * u.

Main results

• TauCeti.skolemNoether: the Skolem-Noether theorem.
• TauCeti.exists_unit_conj_of_algEquiv: every K-algebra automorphism of a finite-dimensional central simple K-algebra is inner.
• TauCeti.exists_unit_conj_subalgebra_val: a K-algebra homomorphism out of a central simple subalgebra B ⊆ A is conjugate to the inclusion of B. This is the form the centralizer theorem consumes.

Implementation notes

Centrality is asked of the source B, not of the target A: what the proof needs is that B ⊗[K] Aᵐᵒᵖ is simple, and TauCeti.IsSimpleRing.tensorProduct gets that from B central simple and A simple. So the statement here is slightly stronger than the usual one, which asks A to be central simple as well; the roadmap's central simple form is the case Algebra.IsCentral K A, which the statement covers because a central simple algebra is in particular simple. Finite-dimensionality of B is not assumed: the proof does need it, because the classification of modules that supplies φ needs B ⊗[K] Aᵐᵒᵖ to be finite-dimensional over K and with it Artinian, but it comes for free from the other hypotheses, since a homomorphism out of the simple ring B into the nontrivial ring A is injective and A is finite-dimensional.

Centrality of the source really is needed, and not just by this proof: the worked example at the end of the file exhibits ℂ as a simple finite-dimensional ℝ-algebra, not central over ℝ, whose complex conjugation is not conjugation by a unit. The classical theorem does hold for a merely simple B provided the ambient A is central simple, but that form needs the centralizer theorem and is a separate, later target; the central simple form pinned here is what the centralizer theorem itself consumes.

TauCeti.Bimodule f is a type synonym for A rather than a Module instance on A itself, because the whole point is to compare the two different B ⊗[K] Aᵐᵒᵖ-module structures coming from f and from g; indexing the synonym by the homomorphism keeps both available at once. It lives in TauCeti/Algebra/CentralSimple/Bimodule.lean, which documents the construction; the centralizer theorem is its second consumer. The statements exported from this file are the three theorems below, all phrased in A and B alone.

References

This implements the Layer 5 target skolemNoether of the semisimple algebras roadmap. See R. S. Pierce, Associative Algebras, GTM 88, Chapter 12, and P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, Chapter 2.

theorem TauCeti.skolemNoether (K : Type u_1) {A : Type u_2} {B : Type u_3} [Field K] [Ring A] [Algebra K A] [Ring B] [Algebra K B] [IsSimpleRing A] [FiniteDimensional K A] [Algebra.IsCentral K B] [IsSimpleRing B] (f g : B →ₐ[K] A) : ∃ (u : Aˣ), ∀ (x : B), g x = ↑u * f x * ↑u⁻¹

The Skolem-Noether theorem. Two K-algebra homomorphisms f g : B →ₐ[K] A from a finite-dimensional central simple K-algebra B to a finite-dimensional simple K-algebra A are conjugate: there is a unit u of A with g x = u * f x * u⁻¹ for all x : B.

Finite-dimensionality of B is not among the hypotheses: it follows from them, because f is injective, B being simple and A nontrivial. The proof does use it, to make B ⊗[K] Aᵐᵒᵖ Artinian, and with it the classification of modules that produces the conjugating isomorphism.

theorem TauCeti.exists_unit_conj_of_algEquiv (K : Type u_1) {A : Type u_2} [Field K] [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] (e : A ≃ₐ[K] A) : ∃ (u : Aˣ), ∀ (x : A), e x = ↑u * x * ↑u⁻¹

Every automorphism of a central simple algebra is inner. A K-algebra automorphism of a finite-dimensional central simple K-algebra A is conjugation by a unit of A.

theorem TauCeti.exists_unit_conj_subalgebra_val (K : Type u_1) {A : Type u_2} [Field K] [Ring A] [Algebra K A] [IsSimpleRing A] [FiniteDimensional K A] (B : Subalgebra K A) [Algebra.IsCentral K ↥B] [IsSimpleRing ↥B] (f : ↥B →ₐ[K] A) : ∃ (u : Aˣ), ∀ (x : ↥B), f x = ↑u * ↑x * ↑u⁻¹

A K-algebra homomorphism out of a central simple subalgebra B of a finite-dimensional simple K-algebra A is conjugate to the inclusion of B: it extends to an inner automorphism of A. This is the form the centralizer theorem consumes.

Worked examples