Algebra automorphisms in End K V are inner #
This file shows that given any algebra equivalence f : End K V ≃ₐ[K] End K V,
there exists a linear equivalence T : V ≃ₗ[K] V such that f x = T ∘ₗ x ∘ₗ T.symm.
In other words, the map MulSemiringAction.toAlgEquiv from GeneralLinearGroup K V to
End K V ≃ₐ[K] End K V is surjective.
theorem
AlgEquiv.eq_linearEquivConjAlgEquiv
{K : Type u_1}
{V : Type u_2}
[Semifield K]
[AddCommMonoid V]
[Module K V]
[Module.Projective K V]
(f : Module.End K V ≃ₐ[K] Module.End K V)
:
∃ (T : V ≃ₗ[K] V), f = LinearEquiv.conjAlgEquiv K T
Given an algebra automorphism f in End K V, there exists a linear isomorphism T
such that f is given by x ↦ T ∘ₗ x ∘ₗ T.symm.
theorem
Module.End.mulSemiringActionToAlgEquiv_conjAct_surjective
{K : Type u_1}
{V : Type u_2}
[Semifield K]
[AddCommMonoid V]
[Module K V]
[Projective K V]
:
Alternate statement of eq_linearEquivAlgConj.