Theorems · Definition · commutative algebra

LinearEquiv.arrowCongr

{R₁ : Type u_9} →
  {R₂ : Type u_10} →
    {R₁' : Type u_12} →
      {R₂' : Type u_13} →
        {M₁ : Type u_17} →
          {M₂ : Type u_18} →
            {M₁' : Type u_20} →
              {M₂' : Type u_21} →
                [inst : Semiring R₁] →
                  [inst_1 : Semiring R₂] →
                    [inst_2 : CommSemiring R₁'] →
                      [inst_3 : CommSemiring R₂'] →
                        [inst_4 : AddCommMonoid M₁] →
                          [inst_5 : AddCommMonoid M₂] →
                            [inst_6 : AddCommMonoid M₁'] →
                              [inst_7 : AddCommMonoid M₂'] →
                                [inst_8 : Module R₁ M₁] →
                                  [inst_9 : Module R₂ M₂] →
                                    [inst_10 : Module R₁' M₁'] →
                                      [inst_11 : Module R₂' M₂'] →
                                        {σ₁₂ : R₁ →+* R₂} →
                                          {σ₂₁ : R₂ →+* R₁} →
                                            {σ₁'₂' : R₁' →+* R₂'} →
                                              {σ₂'₁' : R₂' →+* R₁'} →
                                                {σ₁₁' : R₁ →+* R₁'} →
                                                  {σ₂₂' : R₂ →+* R₂'} →
                                                    {σ₂₁' : R₂ →+* R₁'} →
                                                      {σ₁₂' : R₁ →+* R₂'} →
                                                        [inst_12 : RingHomInvPair σ₁₂ σ₂₁] →
                                                          [inst_13 : RingHomInvPair σ₂₁ σ₁₂] →
                                                            [inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'] →
                                                              [inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'] →
                                                                [RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] →
                                                                  [RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'] →
                                                                    [RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] →
                                                                      [RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] →
                                                                        (M₁ ≃ₛₗ[σ₁₂] M₂) →
                                                                          (M₁' ≃ₛₗ[σ₁'₂'] M₂') →
                                                                            (M₁ →ₛₗ[σ₁₁'] M₁') ≃ₛₗ[σ₁'₂']
                                                                              M₂ →ₛₗ[σ₂₂'] M₂'

A linear isomorphism between the domains and codomains of two spaces of linear maps gives a linear isomorphism between the two function spaces. See LinearEquiv.arrowCongrAddEquiv for the additive version of this isomorphism that works over a not necessarily commutative semiring.

Defined in

Mathlib.Algebra.Module.Equiv.Basic

Cited by

28 results in Mathlib

Foundations

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

Assumes

SemiringSemiringCommSemiringCommSemiringAddCommMonoidAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModuleModuleRingHomInvPairRingHomInvPairRingHomInvPairRingHomInvPairRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTriple