Documentation

Mathlib.Algebra.Module.ULift

ULift instances for module and multiplicative actions #

This file defines instances for module, mul_action and related structures on ULift types.

(Recall ULift α is just a "copy" of a type α in a higher universe.)

We also provide ULift.moduleEquiv : ULift M ≃ₗ[R] M.

source
instance ULift.smulLeft {R : Type u} {M : Type v} [SMul R M] :
SMul (ULift.{u_1, u} R) M
Equations
    source
    instance ULift.vaddLeft {R : Type u} {M : Type v} [VAdd R M] :
    VAdd (ULift.{u_1, u} R) M
    Equations
      source
      @[simp]
      theorem ULift.smul_def {R : Type u} {M : Type v} [SMul R M] (s : ULift.{u_1, u} R) (x : M) :
      s • x = s.down • x
      source
      @[simp]
      theorem ULift.vadd_def {R : Type u} {M : Type v} [VAdd R M] (s : ULift.{u_1, u} R) (x : M) :
      s +ᵥ x = s.down +ᵥ x
      source
      instance ULift.isScalarTower {R : Type u} {M : Type v} {N : Type w} [SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N] :
      IsScalarTower (ULift.{u_1, u} R) M N
      source
      instance ULift.isScalarTower' {R : Type u} {M : Type v} {N : Type w} [SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N] :
      IsScalarTower R (ULift.{u_1, v} M) N
      source
      instance ULift.isScalarTower'' {R : Type u} {M : Type v} {N : Type w} [SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N] :
      IsScalarTower R M (ULift.{u_1, w} N)
      source
      instance ULift.instIsCentralScalar {R : Type u} {M : Type v} [SMul R M] [SMul Rᵐᵒᵖ M] [IsCentralScalar R M] :
      IsCentralScalar R (ULift.{u_1, v} M)
      source
      instance ULift.mulAction {R : Type u} {M : Type v} [Monoid R] [MulAction R M] :
      MulAction (ULift.{u_1, u} R) M
      Equations
        source
        instance ULift.addAction {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] :
        AddAction (ULift.{u_1, u} R) M
        Equations
          source
          instance ULift.mulAction' {R : Type u} {M : Type v} [Monoid R] [MulAction R M] :
          MulAction R (ULift.{u_1, v} M)
          Equations
            source
            instance ULift.addAction' {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] :
            AddAction R (ULift.{u_1, v} M)
            Equations
              source
              instance ULift.smulZeroClass {R : Type u} {M : Type v} [Zero M] [SMulZeroClass R M] :
              SMulZeroClass (ULift.{u_1, u} R) M
              Equations
                source
                instance ULift.smulZeroClass' {R : Type u} {M : Type v} [Zero M] [SMulZeroClass R M] :
                SMulZeroClass R (ULift.{u_1, v} M)
                Equations
                  source
                  instance ULift.distribSMul {R : Type u} {M : Type v} [AddZeroClass M] [DistribSMul R M] :
                  DistribSMul (ULift.{u_1, u} R) M
                  Equations
                    source
                    instance ULift.distribSMul' {R : Type u} {M : Type v} [AddZeroClass M] [DistribSMul R M] :
                    DistribSMul R (ULift.{u_1, v} M)
                    Equations
                      source
                      instance ULift.distribMulAction {R : Type u} {M : Type v} [Monoid R] [AddMonoid M] [DistribMulAction R M] :
                      DistribMulAction (ULift.{u_1, u} R) M
                      Equations
                        source
                        instance ULift.distribMulAction' {R : Type u} {M : Type v} [Monoid R] [AddMonoid M] [DistribMulAction R M] :
                        DistribMulAction R (ULift.{u_1, v} M)
                        Equations
                          source
                          instance ULift.mulDistribMulAction {R : Type u} {M : Type v} [Monoid R] [Monoid M] [MulDistribMulAction R M] :
                          MulDistribMulAction (ULift.{u_1, u} R) M
                          Equations
                            source
                            instance ULift.mulDistribMulAction' {R : Type u} {M : Type v} [Monoid R] [Monoid M] [MulDistribMulAction R M] :
                            MulDistribMulAction R (ULift.{u_1, v} M)
                            Equations
                              source
                              instance ULift.smulWithZero {R : Type u} {M : Type v} [Zero R] [Zero M] [SMulWithZero R M] :
                              SMulWithZero (ULift.{u_1, u} R) M
                              Equations
                                source
                                instance ULift.smulWithZero' {R : Type u} {M : Type v} [Zero R] [Zero M] [SMulWithZero R M] :
                                SMulWithZero R (ULift.{u_1, v} M)
                                Equations
                                  source
                                  instance ULift.mulActionWithZero {R : Type u} {M : Type v} [MonoidWithZero R] [Zero M] [MulActionWithZero R M] :
                                  MulActionWithZero (ULift.{u_1, u} R) M
                                  Equations
                                    source
                                    instance ULift.mulActionWithZero' {R : Type u} {M : Type v} [MonoidWithZero R] [Zero M] [MulActionWithZero R M] :
                                    MulActionWithZero R (ULift.{u_1, v} M)
                                    Equations
                                      source
                                      instance ULift.module {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
                                      Module (ULift.{u_1, u} R) M
                                      Equations
                                        source
                                        instance ULift.module' {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
                                        Module R (ULift.{u_1, v} M)
                                        Equations
                                          source
                                          def ULift.moduleEquiv {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
                                          ULift.{w, v} M ≃ₗ[R] M

                                          The R-linear equivalence between ULift M and M.

                                          This is a linear version of AddEquiv.ulift.

                                          Equations
                                            Instances For
                                              source
                                              @[simp]
                                              theorem ULift.moduleEquiv_symm_apply {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (down : M) :
                                              moduleEquiv.symm down = { down := down }
                                              source
                                              @[simp]
                                              theorem ULift.moduleEquiv_apply {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (self : ULift.{w, v} M) :
                                              moduleEquiv self = self.down