Module.End R M is a central algebra

This file shows that the algebra of endomorphisms on a free module is central.

theorem Module.End.mem_subsemiringCenter_iff {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] {f : End R M} : f ∈ Subsemiring.center (End R M) ↔ ∃ (α : R) (hα : α ∈ Subsemiring.center R), f = smulLeft α hα

theorem Module.End.mem_subalgebraCenter_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] [CommSemiring S] [Module S M] [SMulCommClass R S M] [Algebra S R] [IsScalarTower S R M] {f : End R M} : f ∈ Subalgebra.center S (End R M) ↔ ∃ (α : R) (hα : α ∈ Subalgebra.center S R), f = smulLeft α hα

instance Algebra.IsCentral.instEnd {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [CommSemiring S] [Module S M] [SMulCommClass R S M] [Algebra S R] [IsScalarTower S R M] [IsCentral S R] : IsCentral S (Module.End R M)

The center of endomorphisms on a free module is trivial, in other words, it is a central algebra.

theorem LinearEquiv.conjAlgEquiv_ext_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [CommSemiring S] [Module S M] [SMulCommClass R S M] [Algebra S R] [IsScalarTower S R M] {M₂ : Type u_4} [AddCommMonoid M₂] [Module R M₂] [Module S M₂] [SMulCommClass R S M₂] [IsScalarTower S R M₂] [Algebra.IsCentral S R] {f g : M ≃ₗ[R] M₂} : conjAlgEquiv S f = conjAlgEquiv S g ↔ ∃ (α : S), ⇑f = α • ⇑g

theorem LinearEquiv.conjAlgEquiv_ext_iff' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] {S : Type u_4} {M₂ : Type u_5} [CommRing S] [IsCancelMulZero S] [Module S M] [SMulCommClass R S M] [Algebra S R] [IsScalarTower S R M] [AddCommGroup M₂] [Module R M₂] [Module S M₂] [SMulCommClass R S M₂] [IsScalarTower S R M₂] [Algebra.IsCentral S R] [Module.IsTorsionFree S M₂] (f g : M ≃ₗ[R] M₂) : conjAlgEquiv S f = conjAlgEquiv S g ↔ ∃ (α : Sˣ), f = α • g