Theorems · Definition · commutative algebra

LinearEquiv.conj

{R₁' : Type u_12} →
  {R₂' : Type u_13} →
    {M₁' : Type u_20} →
      {M₂' : Type u_21} →
        [inst : CommSemiring R₁'] →
          [inst_1 : CommSemiring R₂'] →
            [inst_2 : AddCommMonoid M₁'] →
              [inst_3 : AddCommMonoid M₂'] →
                [inst_4 : Module R₁' M₁'] →
                  [inst_5 : Module R₂' M₂'] →
                    {σ₁'₂' : R₁' →+* R₂'} →
                      {σ₂'₁' : R₂' →+* R₁'} →
                        [inst_6 : RingHomInvPair σ₁'₂' σ₂'₁'] →
                          [inst_7 : RingHomInvPair σ₂'₁' σ₁'₂'] →
                            (M₁' ≃ₛₗ[σ₁'₂'] M₂') → Module.End R₁' M₁' ≃ₛₗ[σ₁'₂'] Module.End R₂' M₂'

If M and M₂ are linearly isomorphic then the two spaces of linear maps from M and M₂ to themselves are linearly isomorphic. See LinearEquiv.conjRingEquiv for the isomorphism between endomorphism rings, which works over a not necessarily commutative semiring.

Defined in

Mathlib.Algebra.Module.Equiv.Basic

Cited by

38 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringCommSemiringAddCommMonoidAddCommMonoidModuleModuleRingHomInvPairRingHomInvPair