Documentation

Mathlib.Algebra.Module.Equiv.Basic

Further results on (semi)linear equivalences. #

@[simp]
theorem LinearEquiv.restrictScalars_symm_apply (R : Type u_1) {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f : M ≃ₗ[S] M₂) (a : M₂) :
(LinearEquiv.restrictScalars R f).symm a = f.symm a
@[simp]
theorem LinearEquiv.restrictScalars_apply (R : Type u_1) {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f : M ≃ₗ[S] M₂) (a : M) :
def LinearEquiv.restrictScalars (R : Type u_1) {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f : M ≃ₗ[S] M₂) :
M ≃ₗ[R] M₂

If M and M₂ are both R-semimodules and S-semimodules and R-semimodule structures are defined by an action of R on S (formally, we have two scalar towers), then any S-linear equivalence from M to M₂ is also an R-linear equivalence.

See also LinearMap.restrictScalars.

Equations
  • LinearEquiv.restrictScalars R f = { toFun := f, map_add' := , map_smul' := , invFun := f.symm, left_inv := , right_inv := }
Instances For
    theorem LinearEquiv.restrictScalars_injective (R : Type u_1) {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] :
    @[simp]
    theorem LinearEquiv.restrictScalars_inj (R : Type u_1) {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f : M ≃ₗ[S] M₂) (g : M ≃ₗ[S] M₂) :
    theorem Module.End_isUnit_iff {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) :
    instance LinearEquiv.automorphismGroup {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] :
    Equations
    @[simp]
    theorem LinearEquiv.coe_one {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] :
    1 = id
    @[simp]
    theorem LinearEquiv.coe_toLinearMap_one {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] :
    1 = LinearMap.id
    @[simp]
    theorem LinearEquiv.coe_toLinearMap_mul {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] {e₁ : M ≃ₗ[R] M} {e₂ : M ≃ₗ[R] M} :
    (e₁ * e₂) = e₁ * e₂
    theorem LinearEquiv.coe_pow {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] M) (n : ) :
    (e ^ n) = (⇑e)^[n]
    theorem LinearEquiv.pow_apply {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] M) (n : ) (m : M) :
    (e ^ n) m = (⇑e)^[n] m
    @[simp]
    theorem LinearEquiv.automorphismGroup.toLinearMapMonoidHom_apply {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] M) :
    LinearEquiv.automorphismGroup.toLinearMapMonoidHom e = e

    Restriction from R-linear automorphisms of M to R-linear endomorphisms of M, promoted to a monoid hom.

    Equations
    • LinearEquiv.automorphismGroup.toLinearMapMonoidHom = { toFun := fun (e : M ≃ₗ[R] M) => e, map_one' := , map_mul' := }
    Instances For

      The tautological action by M ≃ₗ[R] M on M.

      This generalizes Function.End.applyMulAction.

      Equations
      @[simp]
      theorem LinearEquiv.smul_def {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] (f : M ≃ₗ[R] M) (a : M) :
      f a = f a
      instance LinearEquiv.apply_faithfulSMul {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] :

      LinearEquiv.applyDistribMulAction is faithful.

      Equations
      • =
      instance LinearEquiv.apply_smulCommClass {R : Type u_1} {S : Type u_7} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [SMul S M] [IsScalarTower S R M] :
      Equations
      • =
      instance LinearEquiv.apply_smulCommClass' {R : Type u_1} {S : Type u_7} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [SMul S M] [IsScalarTower S R M] :
      Equations
      • =
      @[simp]
      theorem LinearEquiv.ofSubsingleton_symm_apply {R : Type u_1} (M : Type u_8) (M₂ : Type u_10) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Subsingleton M] [Subsingleton M₂] :
      ∀ (x : M₂), (LinearEquiv.ofSubsingleton M M₂).symm x = 0
      @[simp]
      theorem LinearEquiv.ofSubsingleton_apply {R : Type u_1} (M : Type u_8) (M₂ : Type u_10) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Subsingleton M] [Subsingleton M₂] :
      ∀ (x : M), (LinearEquiv.ofSubsingleton M M₂) x = 0
      def LinearEquiv.ofSubsingleton {R : Type u_1} (M : Type u_8) (M₂ : Type u_10) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Subsingleton M] [Subsingleton M₂] :
      M ≃ₗ[R] M₂

      Any two modules that are subsingletons are isomorphic.

      Equations
      • LinearEquiv.ofSubsingleton M M₂ = { toFun := fun (x : M) => 0, map_add' := , map_smul' := , invFun := fun (x : M₂) => 0, left_inv := , right_inv := }
      Instances For
        @[simp]
        theorem Module.compHom.toLinearEquiv_symm_apply {R : Type u_17} {S : Type u_18} [Semiring R] [Semiring S] (g : R ≃+* S) (a : S) :
        (Module.compHom.toLinearEquiv g).symm a = g.symm a
        @[simp]
        theorem Module.compHom.toLinearEquiv_apply {R : Type u_17} {S : Type u_18} [Semiring R] [Semiring S] (g : R ≃+* S) (a : R) :
        def Module.compHom.toLinearEquiv {R : Type u_17} {S : Type u_18} [Semiring R] [Semiring S] (g : R ≃+* S) :

        g : R ≃+* S is R-linear when the module structure on S is Module.compHom S g .

        Equations
        Instances For
          @[simp]
          theorem DistribMulAction.toLinearEquiv_apply (R : Type u_1) {S : Type u_7} (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) :
          ∀ (a : M), (DistribMulAction.toLinearEquiv R M s) a = s a
          @[simp]
          theorem DistribMulAction.toLinearEquiv_symm_apply (R : Type u_1) {S : Type u_7} (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) :
          ∀ (a : M), (DistribMulAction.toLinearEquiv R M s).symm a = s⁻¹ a
          def DistribMulAction.toLinearEquiv (R : Type u_1) {S : Type u_7} (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) :

          Each element of the group defines a linear equivalence.

          This is a stronger version of DistribMulAction.toAddEquiv.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def DistribMulAction.toModuleAut (R : Type u_1) {S : Type u_7} (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [SMulCommClass S R M] :
            S →* M ≃ₗ[R] M

            Each element of the group defines a module automorphism.

            This is a stronger version of DistribMulAction.toAddAut.

            Equations
            Instances For
              def AddEquiv.toLinearEquiv {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃+ M₂) (h : ∀ (c : R) (x : M), e (c x) = c e x) :
              M ≃ₗ[R] M₂

              An additive equivalence whose underlying function preserves smul is a linear equivalence.

              Equations
              • e.toLinearEquiv h = { toFun := e.toFun, map_add' := , map_smul' := h, invFun := e.invFun, left_inv := , right_inv := }
              Instances For
                @[simp]
                theorem AddEquiv.coe_toLinearEquiv {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃+ M₂) (h : ∀ (c : R) (x : M), e (c x) = c e x) :
                (e.toLinearEquiv h) = e
                @[simp]
                theorem AddEquiv.coe_toLinearEquiv_symm {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃+ M₂) (h : ∀ (c : R) (x : M), e (c x) = c e x) :
                (e.toLinearEquiv h).symm = e.symm
                def AddEquiv.toNatLinearEquiv {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃+ M₂) :

                An additive equivalence between commutative additive monoids is a linear equivalence between ℕ-modules

                Equations
                • e.toNatLinearEquiv = e.toLinearEquiv
                Instances For
                  @[simp]
                  theorem AddEquiv.coe_toNatLinearEquiv {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃+ M₂) :
                  e.toNatLinearEquiv = e
                  @[simp]
                  theorem AddEquiv.toNatLinearEquiv_toAddEquiv {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃+ M₂) :
                  e.toNatLinearEquiv = e
                  @[simp]
                  theorem LinearEquiv.toAddEquiv_toNatLinearEquiv {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃ₗ[] M₂) :
                  (↑e).toNatLinearEquiv = e
                  @[simp]
                  theorem AddEquiv.toNatLinearEquiv_symm {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃+ M₂) :
                  e.toNatLinearEquiv.symm = e.symm.toNatLinearEquiv
                  @[simp]
                  @[simp]
                  theorem AddEquiv.toNatLinearEquiv_trans {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃) :
                  e.toNatLinearEquiv ≪≫ₗ e₂.toNatLinearEquiv = (e.trans e₂).toNatLinearEquiv
                  def AddEquiv.toIntLinearEquiv {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃+ M₂) :

                  An additive equivalence between commutative additive groups is a linear equivalence between ℤ-modules

                  Equations
                  • e.toIntLinearEquiv = e.toLinearEquiv
                  Instances For
                    @[simp]
                    theorem AddEquiv.coe_toIntLinearEquiv {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃+ M₂) :
                    e.toIntLinearEquiv = e
                    @[simp]
                    theorem AddEquiv.toIntLinearEquiv_toAddEquiv {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃+ M₂) :
                    e.toIntLinearEquiv = e
                    @[simp]
                    theorem LinearEquiv.toAddEquiv_toIntLinearEquiv {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃ₗ[] M₂) :
                    (↑e).toIntLinearEquiv = e
                    @[simp]
                    theorem AddEquiv.toIntLinearEquiv_symm {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃+ M₂) :
                    e.toIntLinearEquiv.symm = e.symm.toIntLinearEquiv
                    @[simp]
                    @[simp]
                    theorem AddEquiv.toIntLinearEquiv_trans {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] [AddCommGroup M₃] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃) :
                    e.toIntLinearEquiv ≪≫ₗ e₂.toIntLinearEquiv = (e.trans e₂).toIntLinearEquiv
                    @[simp]
                    theorem LinearMap.ringLmapEquivSelf_symm_apply (R : Type u_1) (S : Type u_7) (M : Type u_8) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] (x : M) :
                    @[simp]
                    theorem LinearMap.ringLmapEquivSelf_apply (R : Type u_1) (S : Type u_7) (M : Type u_8) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] (f : R →ₗ[R] M) :
                    def LinearMap.ringLmapEquivSelf (R : Type u_1) (S : Type u_7) (M : Type u_8) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] :
                    (R →ₗ[R] M) ≃ₗ[S] M

                    The equivalence between R-linear maps from R to M, and points of M itself. This says that the forgetful functor from R-modules to types is representable, by R.

                    This is an S-linear equivalence, under the assumption that S acts on M commuting with R. When R is commutative, we can take this to be the usual action with S = R. Otherwise, S = ℕ shows that the equivalence is additive. See note [bundled maps over different rings].

                    Equations
                    Instances For
                      @[simp]
                      theorem addMonoidHomLequivNat_apply {A : Type u_17} {B : Type u_18} (R : Type u_19) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R B] (f : A →+ B) :
                      (addMonoidHomLequivNat R) f = f.toNatLinearMap
                      @[simp]
                      theorem addMonoidHomLequivNat_symm_apply {A : Type u_17} {B : Type u_18} (R : Type u_19) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R B] (f : A →ₗ[] B) :
                      (addMonoidHomLequivNat R).symm f = f.toAddMonoidHom
                      def addMonoidHomLequivNat {A : Type u_17} {B : Type u_18} (R : Type u_19) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R B] :

                      The R-linear equivalence between additive morphisms A →+ B and -linear morphisms A →ₗ[ℕ] B.

                      Equations
                      • addMonoidHomLequivNat R = { toFun := AddMonoidHom.toNatLinearMap, map_add' := , map_smul' := , invFun := LinearMap.toAddMonoidHom, left_inv := , right_inv := }
                      Instances For
                        @[simp]
                        theorem addMonoidHomLequivInt_symm_apply {A : Type u_17} {B : Type u_18} (R : Type u_19) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] (f : A →ₗ[] B) :
                        (addMonoidHomLequivInt R).symm f = f.toAddMonoidHom
                        @[simp]
                        theorem addMonoidHomLequivInt_apply {A : Type u_17} {B : Type u_18} (R : Type u_19) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] (f : A →+ B) :
                        (addMonoidHomLequivInt R) f = f.toIntLinearMap
                        def addMonoidHomLequivInt {A : Type u_17} {B : Type u_18} (R : Type u_19) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] :

                        The R-linear equivalence between additive morphisms A →+ B and -linear morphisms A →ₗ[ℤ] B.

                        Equations
                        • addMonoidHomLequivInt R = { toFun := AddMonoidHom.toIntLinearMap, map_add' := , map_smul' := , invFun := LinearMap.toAddMonoidHom, left_inv := , right_inv := }
                        Instances For
                          @[simp]
                          theorem addMonoidEndRingEquivInt_apply (A : Type u_17) [AddCommGroup A] :
                          ∀ (a : A →+ A), (addMonoidEndRingEquivInt A) a = (↑(addMonoidHomLequivInt )).toFun a

                          Ring equivalence between additive group endomorphisms of an AddCommGroup A and -module endomorphisms of A.

                          Equations
                          Instances For
                            instance LinearEquiv.instZero {R : Type u_1} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] :
                            Zero (M ≃ₛₗ[σ₁₂] M₂)

                            Between two zero modules, the zero map is an equivalence.

                            Equations
                            • LinearEquiv.instZero = { zero := let __src := 0; { toFun := 0, map_add' := , map_smul' := , invFun := 0, left_inv := , right_inv := } }
                            @[simp]
                            theorem LinearEquiv.zero_symm {R : Type u_1} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] :
                            @[simp]
                            theorem LinearEquiv.coe_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] :
                            0 = 0
                            theorem LinearEquiv.zero_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] (x : M) :
                            0 x = 0
                            instance LinearEquiv.instUnique {R : Type u_1} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] :
                            Unique (M ≃ₛₗ[σ₁₂] M₂)

                            Between two zero modules, the zero map is the only equivalence.

                            Equations
                            • LinearEquiv.instUnique = { default := 0, uniq := }
                            instance LinearEquiv.uniqueOfSubsingleton {R : Type u_1} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton R] [Subsingleton R₂] :
                            Unique (M ≃ₛₗ[σ₁₂] M₂)
                            Equations
                            • LinearEquiv.uniqueOfSubsingleton = inferInstance
                            def LinearEquiv.curry (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] (V : Type u_17) (V₂ : Type u_18) :
                            (V × V₂M) ≃ₗ[R] VV₂M

                            Linear equivalence between a curried and uncurried function. Differs from TensorProduct.curry.

                            Equations
                            Instances For
                              @[simp]
                              theorem LinearEquiv.coe_curry (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] (V : Type u_18) (V₂ : Type u_17) :
                              (LinearEquiv.curry R M V V₂) = Function.curry
                              @[simp]
                              theorem LinearEquiv.coe_curry_symm (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] (V : Type u_18) (V₂ : Type u_17) :
                              (LinearEquiv.curry R M V V₂).symm = Function.uncurry
                              def LinearEquiv.ofLinear {R : Type u_1} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) (h₁ : f.comp g = LinearMap.id) (h₂ : g.comp f = LinearMap.id) :
                              M ≃ₛₗ[σ₁₂] M₂

                              If a linear map has an inverse, it is a linear equivalence.

                              Equations
                              • LinearEquiv.ofLinear f g h₁ h₂ = { toLinearMap := f, invFun := g, left_inv := , right_inv := }
                              Instances For
                                @[simp]
                                theorem LinearEquiv.ofLinear_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f.comp g = LinearMap.id} {h₂ : g.comp f = LinearMap.id} (x : M) :
                                (LinearEquiv.ofLinear f g h₁ h₂) x = f x
                                @[simp]
                                theorem LinearEquiv.ofLinear_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f.comp g = LinearMap.id} {h₂ : g.comp f = LinearMap.id} (x : M₂) :
                                (LinearEquiv.ofLinear f g h₁ h₂).symm x = g x
                                @[simp]
                                theorem LinearEquiv.ofLinear_toLinearMap {R : Type u_1} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f.comp g = LinearMap.id} {h₂ : g.comp f = LinearMap.id} :
                                (LinearEquiv.ofLinear f g h₁ h₂) = f
                                @[simp]
                                theorem LinearEquiv.ofLinear_symm_toLinearMap {R : Type u_1} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f.comp g = LinearMap.id} {h₂ : g.comp f = LinearMap.id} :
                                (LinearEquiv.ofLinear f g h₁ h₂).symm = g
                                def LinearEquiv.neg (R : Type u_1) {M : Type u_8} [Semiring R] [AddCommGroup M] [Module R M] :

                                x ↦ -x as a LinearEquiv

                                Equations
                                Instances For
                                  @[simp]
                                  theorem LinearEquiv.coe_neg {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommGroup M] [Module R M] :
                                  theorem LinearEquiv.neg_apply {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommGroup M] [Module R M] (x : M) :
                                  @[simp]
                                  theorem LinearEquiv.symm_neg {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommGroup M] [Module R M] :
                                  def LinearEquiv.smulOfUnit {R : Type u_1} {M : Type u_8} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : Rˣ) :

                                  Multiplying by a unit a of the ring R is a linear equivalence.

                                  Equations
                                  Instances For
                                    def LinearEquiv.arrowCongr {R : Type u_17} {M₁ : Type u_18} {M₂ : Type u_19} {M₂₁ : Type u_20} {M₂₂ : Type u_21} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) :
                                    (M₁ →ₗ[R] M₂₁) ≃ₗ[R] M₂ →ₗ[R] M₂₂

                                    A linear isomorphism between the domains and codomains of two spaces of linear maps gives a linear isomorphism between the two function spaces.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]
                                      theorem LinearEquiv.arrowCongr_apply {R : Type u_17} {M₁ : Type u_18} {M₂ : Type u_19} {M₂₁ : Type u_20} {M₂₂ : Type u_21} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₁ →ₗ[R] M₂₁) (x : M₂) :
                                      ((e₁.arrowCongr e₂) f) x = e₂ (f (e₁.symm x))
                                      @[simp]
                                      theorem LinearEquiv.arrowCongr_symm_apply {R : Type u_17} {M₁ : Type u_18} {M₂ : Type u_19} {M₂₁ : Type u_20} {M₂₂ : Type u_21} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₂ →ₗ[R] M₂₂) (x : M₁) :
                                      ((e₁.arrowCongr e₂).symm f) x = e₂.symm (f (e₁ x))
                                      theorem LinearEquiv.arrowCongr_comp {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] {N : Type u_17} {N₂ : Type u_18} {N₃ : Type u_19} [AddCommMonoid N] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R N] [Module R N₂] [Module R N₃] (e₁ : M ≃ₗ[R] N) (e₂ : M₂ ≃ₗ[R] N₂) (e₃ : M₃ ≃ₗ[R] N₃) (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :
                                      (e₁.arrowCongr e₃) (g ∘ₗ f) = (e₂.arrowCongr e₃) g ∘ₗ (e₁.arrowCongr e₂) f
                                      theorem LinearEquiv.arrowCongr_trans {R : Type u_1} [CommSemiring R] {M₁ : Type u_17} {M₂ : Type u_18} {M₃ : Type u_19} {N₁ : Type u_20} {N₂ : Type u_21} {N₃ : Type u_22} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] [AddCommMonoid N₁] [Module R N₁] [AddCommMonoid N₂] [Module R N₂] [AddCommMonoid N₃] [Module R N₃] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : N₁ ≃ₗ[R] N₂) (e₃ : M₂ ≃ₗ[R] M₃) (e₄ : N₂ ≃ₗ[R] N₃) :
                                      e₁.arrowCongr e₂ ≪≫ₗ e₃.arrowCongr e₄ = (e₁ ≪≫ₗ e₃).arrowCongr (e₂ ≪≫ₗ e₄)
                                      def LinearEquiv.congrRight {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M₂ ≃ₗ[R] M₃) :
                                      (M →ₗ[R] M₂) ≃ₗ[R] M →ₗ[R] M₃

                                      If M₂ and M₃ are linearly isomorphic then the two spaces of linear maps from M into M₂ and M into M₃ are linearly isomorphic.

                                      Equations
                                      Instances For
                                        def LinearEquiv.conj {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[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.

                                        Equations
                                        • e.conj = e.arrowCongr e
                                        Instances For
                                          theorem LinearEquiv.conj_apply {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M) :
                                          e.conj f = (e ∘ₗ f) ∘ₗ e.symm
                                          theorem LinearEquiv.conj_apply_apply {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M) (x : M₂) :
                                          (e.conj f) x = e (f (e.symm x))
                                          theorem LinearEquiv.symm_conj_apply {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M₂) :
                                          e.symm.conj f = (e.symm ∘ₗ f) ∘ₗ e
                                          theorem LinearEquiv.conj_comp {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M) (g : Module.End R M) :
                                          e.conj (g ∘ₗ f) = e.conj g ∘ₗ e.conj f
                                          theorem LinearEquiv.conj_trans {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) :
                                          e₁.conj ≪≫ₗ e₂.conj = (e₁ ≪≫ₗ e₂).conj
                                          @[simp]
                                          theorem LinearEquiv.conj_id {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) :
                                          e.conj LinearMap.id = LinearMap.id
                                          def LinearEquiv.congrLeft (M : Type u_8) {M₂ : Type u_10} {M₃ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] {R : Type u_17} (S : Type u_18) [Semiring R] [Semiring S] [Module R M₂] [Module R M₃] [Module R M] [Module S M] [SMulCommClass R S M] (e : M₂ ≃ₗ[R] M₃) :
                                          (M₂ →ₗ[R] M) ≃ₗ[S] M₃ →ₗ[R] M

                                          An R-linear isomorphism between two R-modules M₂ and M₃ induces an S-linear isomorphism between M₂ →ₗ[R] M and M₃ →ₗ[R] M, if M is both an R-module and an S-module and their actions commute.

                                          Equations
                                          • LinearEquiv.congrLeft M S e = { toFun := fun (f : M₂ →ₗ[R] M) => f ∘ₗ e.symm, map_add' := , map_smul' := , invFun := fun (f : M₃ →ₗ[R] M) => f ∘ₗ e, left_inv := , right_inv := }
                                          Instances For
                                            @[simp]
                                            theorem LinearEquiv.smulOfNeZero_apply (K : Type u_6) (M : Type u_8) [Field K] [AddCommGroup M] [Module K M] (a : K) (ha : a 0) :
                                            ∀ (a_1 : M), (LinearEquiv.smulOfNeZero K M a ha) a_1 = Units.mk0 a ha a_1
                                            @[simp]
                                            theorem LinearEquiv.smulOfNeZero_symm_apply (K : Type u_6) (M : Type u_8) [Field K] [AddCommGroup M] [Module K M] (a : K) (ha : a 0) :
                                            ∀ (a_1 : M), (LinearEquiv.smulOfNeZero K M a ha).symm a_1 = (Units.mk0 a ha)⁻¹ a_1
                                            def LinearEquiv.smulOfNeZero (K : Type u_6) (M : Type u_8) [Field K] [AddCommGroup M] [Module K M] (a : K) (ha : a 0) :

                                            Multiplying by a nonzero element a of the field K is a linear equivalence.

                                            Equations
                                            Instances For
                                              def Equiv.toLinearEquiv {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] (e : M M₂) (h : IsLinearMap R e) :
                                              M ≃ₗ[R] M₂

                                              An equivalence whose underlying function is linear is a linear equivalence.

                                              Equations
                                              • e.toLinearEquiv h = { toFun := e.toFun, map_add' := , map_smul' := , invFun := e.invFun, left_inv := , right_inv := }
                                              Instances For
                                                def LinearMap.funLeft (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} (f : mn) :
                                                (nM) →ₗ[R] mM

                                                Given an R-module M and a function m → n between arbitrary types, construct a linear map (n → M) →ₗ[R] (m → M)

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem LinearMap.funLeft_apply (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} (f : mn) (g : nM) (i : m) :
                                                  (LinearMap.funLeft R M f) g i = g (f i)
                                                  @[simp]
                                                  theorem LinearMap.funLeft_id (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {n : Type u_18} (g : nM) :
                                                  (LinearMap.funLeft R M id) g = g
                                                  theorem LinearMap.funLeft_comp (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} {p : Type u_19} (f₁ : np) (f₂ : mn) :
                                                  LinearMap.funLeft R M (f₁ f₂) = LinearMap.funLeft R M f₂ ∘ₗ LinearMap.funLeft R M f₁
                                                  theorem LinearMap.funLeft_surjective_of_injective (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} (f : mn) (hf : Function.Injective f) :
                                                  theorem LinearMap.funLeft_injective_of_surjective (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} (f : mn) (hf : Function.Surjective f) :
                                                  def LinearEquiv.funCongrLeft (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} (e : m n) :
                                                  (nM) ≃ₗ[R] mM

                                                  Given an R-module M and an equivalence m ≃ n between arbitrary types, construct a linear equivalence (n → M) ≃ₗ[R] (m → M)

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem LinearEquiv.funCongrLeft_apply (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} (e : m n) (x : nM) :
                                                    @[simp]
                                                    theorem LinearEquiv.funCongrLeft_id (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {n : Type u_18} :
                                                    @[simp]
                                                    theorem LinearEquiv.funCongrLeft_comp (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} {p : Type u_19} (e₁ : m n) (e₂ : n p) :
                                                    LinearEquiv.funCongrLeft R M (e₁.trans e₂) = LinearEquiv.funCongrLeft R M e₂ ≪≫ₗ LinearEquiv.funCongrLeft R M e₁
                                                    @[simp]
                                                    theorem LinearEquiv.funCongrLeft_symm (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} (e : m n) :