Algebra isomorphisms between endomorphisms of projective modules are inner

This file shows that given any algebra equivalence f : End K V ≃ₐ[K] End K W, there exists a linear equivalence T : V ≃ₗ[K] W such that f x = T ∘ₗ x ∘ₗ T.symm. In other words, for V = W, the map MulSemiringAction.toAlgEquiv from GeneralLinearGroup K V to End K V ≃ₐ[K] End K V is surjective.

For the continuous versions, see Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean.

theorem AlgEquiv.eq_linearEquivConjAlgEquiv {K : Type u_1} {V : Type u_2} {W : Type u_3} [Semifield K] [AddCommMonoid V] [Module K V] [Module.Projective K V] [AddCommMonoid W] [Module K W] [Module.Projective K W] (f : Module.End K V ≃ₐ[K] Module.End K W) : ∃ (T : V ≃ₗ[K] W), f = LinearEquiv.conjAlgEquiv K T

Given an algebra isomorphism f : End K V ≃ₐ[K] End K W, there exists a linear isomorphism T such that f is given by x ↦ T ∘ₗ x ∘ₗ T.symm.

theorem LinearEquiv.conjAlgEquiv_surjective (K : Type u_1) (V : Type u_2) (W : Type u_3) [Semifield K] [AddCommMonoid V] [Module K V] [Module.Projective K V] [AddCommMonoid W] [Module K W] [Module.Projective K W] : Function.Surjective (conjAlgEquiv K)

theorem Module.End.mulSemiringActionToAlgEquiv_conjAct_surjective {K : Type u_1} {V : Type u_2} [Semifield K] [AddCommMonoid V] [Module K V] [Projective K V] : Function.Surjective (MulSemiringAction.toAlgEquiv K (End K V))

Alternate statement of AlgEquiv.eq_linearEquivConjAlgEquiv for when V = W.