Mathlib.Algebra.Ring.ULift

ULift.mulZeroClass instance

{M₀ : Type*} [MulZeroClass M₀] : MulZeroClass (ULift M₀)

Full source

instance mulZeroClass {M₀ : Type*} [MulZeroClass M₀] : MulZeroClass (ULift M₀) :=
  { zero := (0 : ULift M₀), mul := (· * ·), zero_mul := fun _ => (Equiv.ulift).injective (by simp),
    mul_zero := fun _ => (Equiv.ulift).injective (by simp) }

Multiplication with Zero Structure on Lifted Types

Informal description

For any type $M_0$ with a multiplication operation and a zero element satisfying $0 \cdot a = 0$ and $a \cdot 0 = 0$ for all $a \in M_0$, the lifted type $\mathrm{ULift}\,M_0$ also inherits this structure, with multiplication and zero defined by lifting the operations from $M_0$.

ULift.distrib instance

[Distrib R] : Distrib (ULift R)

Full source

instance distrib [Distrib R] : Distrib (ULift R) :=
  { add := (· + ·), mul := (· * ·),
    left_distrib := fun _ _ _ => (Equiv.ulift).injective (by simp [left_distrib]),
    right_distrib := fun _ _ _ => (Equiv.ulift).injective (by simp [right_distrib]) }

Distributive Structure on Lifted Types

Informal description

For any type $R$ equipped with a distributive structure (i.e., operations of addition and multiplication satisfying the distributive laws), the lifted type $\mathrm{ULift}\,R$ also inherits a distributive structure, where the operations are defined by lifting those from $R$.

ULift.nonUnitalNonAssocSemiring instance

[NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (ULift R)

Full source

instance nonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring R] :
    NonUnitalNonAssocSemiring (ULift R) :=
  { zero := (0 : ULift R), add := (· + ·), mul := (· * ·), nsmul := AddMonoid.nsmul,
    zero_add, add_zero, zero_mul, mul_zero, left_distrib, right_distrib,
    nsmul_zero := fun _ => AddMonoid.nsmul_zero _,
    nsmul_succ := fun _ _ => AddMonoid.nsmul_succ _ _,
    add_assoc, add_comm }

Non-Unital Non-Associative Semiring Structure on Lifted Types

Informal description

For any type $R$ equipped with the structure of a non-unital non-associative semiring, the lifted type $\mathrm{ULift}\,R$ also inherits this structure, with addition and multiplication defined by lifting the operations from $R$.

ULift.nonAssocSemiring instance

[NonAssocSemiring R] : NonAssocSemiring (ULift R)

Full source

instance nonAssocSemiring [NonAssocSemiring R] : NonAssocSemiring (ULift R) :=
  { ULift.addMonoidWithOne with
      nsmul := AddMonoid.nsmul, natCast := fun n => ULift.up n, add_comm, left_distrib,
      right_distrib, zero_mul, mul_zero, one_mul, mul_one }

Non-Associative Semiring Structure on Lifted Types

Informal description

For any type $R$ that is a non-associative semiring, the lifted type $\mathrm{ULift}\,R$ is also a non-associative semiring, with addition and multiplication operations defined by lifting those from $R$.

ULift.nonUnitalSemiring instance

[NonUnitalSemiring R] : NonUnitalSemiring (ULift R)

Full source

instance nonUnitalSemiring [NonUnitalSemiring R] : NonUnitalSemiring (ULift R) :=
  { zero := (0 : ULift R), add := (· + ·), mul := (· * ·), nsmul := AddMonoid.nsmul,
    add_assoc, zero_add, add_zero, add_comm, left_distrib, right_distrib, zero_mul, mul_zero,
    mul_assoc, nsmul_zero := fun _ => AddMonoid.nsmul_zero _,
    nsmul_succ := fun _ _ => AddMonoid.nsmul_succ _ _ }

Non-Unital Semiring Structure on Lifted Types

Informal description

For any type $R$ equipped with the structure of a non-unital semiring, the lifted type $\mathrm{ULift}\,R$ also inherits this structure, with addition and multiplication defined by lifting the operations from $R$.

ULift.semiring instance

[Semiring R] : Semiring (ULift R)

Full source

instance semiring [Semiring R] : Semiring (ULift R) :=
  { ULift.addMonoidWithOne with
      nsmul := AddMonoid.nsmul,
      npow := Monoid.npow, natCast := fun n => ULift.up n, add_comm, left_distrib, right_distrib,
      zero_mul, mul_zero, mul_assoc, one_mul, mul_one, npow_zero := fun _ => Monoid.npow_zero _,
      npow_succ := fun _ _ => Monoid.npow_succ _ _ }

Semiring Structure on Lifted Types

Informal description

For any semiring $R$, the lifted type $\mathrm{ULift}\,R$ is also a semiring with operations inherited from $R$.

ULift.ringEquiv definition

[NonUnitalNonAssocSemiring R] : ULift R ≃+* R

Full source

/-- The ring equivalence between `ULift R` and `R`. -/
def ringEquiv [NonUnitalNonAssocSemiring R] : ULiftULift R ≃+* R where
  toFun := ULift.down
  invFun := ULift.up
  map_mul' _ _ := rfl
  map_add' _ _ := rfl
  left_inv := fun _ => rfl
  right_inv := fun _ => rfl

Ring equivalence between lifted type and original type

Informal description

The ring equivalence between the lifted type $\mathrm{ULift}\,R$ and $R$ is given by the pair of functions $\mathrm{ULift.down}$ and $\mathrm{ULift.up}$, which are mutual inverses. This equivalence preserves both the multiplicative and additive structures of the rings.

ULift.nonUnitalCommSemiring instance

[NonUnitalCommSemiring R] : NonUnitalCommSemiring (ULift R)

Full source

instance nonUnitalCommSemiring [NonUnitalCommSemiring R] : NonUnitalCommSemiring (ULift R) :=
  { zero := (0 : ULift R), add := (· + ·), mul := (· * ·), nsmul := AddMonoid.nsmul, add_assoc,
    zero_add, add_zero, add_comm, left_distrib, right_distrib, zero_mul, mul_zero, mul_assoc,
    mul_comm, nsmul_zero := fun _ => AddMonoid.nsmul_zero _,
    nsmul_succ := fun _ _ => AddMonoid.nsmul_succ _ _ }

Lifted Non-Unital Commutative Semiring Structure

Informal description

For any non-unital commutative semiring $R$, the lifted type $\mathrm{ULift}\,R$ is also a non-unital commutative semiring, with operations inherited from $R$.

ULift.commSemiring instance

[CommSemiring R] : CommSemiring (ULift R)

Full source

instance commSemiring [CommSemiring R] : CommSemiring (ULift R) :=
  { ULift.semiring with
      nsmul := AddMonoid.nsmul, natCast := fun n => ULift.up n, npow := Monoid.npow, mul_comm }

Commutative Semiring Structure on Lifted Types

Informal description

For any commutative semiring $R$, the lifted type $\mathrm{ULift}\,R$ is also a commutative semiring with operations inherited from $R$.

ULift.nonUnitalNonAssocRing instance

[NonUnitalNonAssocRing R] : NonUnitalNonAssocRing (ULift R)

Full source

instance nonUnitalNonAssocRing [NonUnitalNonAssocRing R] : NonUnitalNonAssocRing (ULift R) :=
  { zero := (0 : ULift R), add := (· + ·), mul := (· * ·), sub := Sub.sub, neg := Neg.neg,
    nsmul := AddMonoid.nsmul, zsmul := SubNegMonoid.zsmul, add_assoc, zero_add, add_zero,
    neg_add_cancel, add_comm, left_distrib, right_distrib, zero_mul, mul_zero, sub_eq_add_neg,
    nsmul_zero := fun _ => AddMonoid.nsmul_zero _,
    nsmul_succ := fun _ _ => AddMonoid.nsmul_succ _ _,
    zsmul_zero' := SubNegMonoid.zsmul_zero', zsmul_succ' := SubNegMonoid.zsmul_succ',
    zsmul_neg' := SubNegMonoid.zsmul_neg' }

Lifted Non-Unital Non-Associative Ring Structure

Informal description

For any non-unital non-associative ring $R$, the lifted type $\mathrm{ULift}\,R$ is also a non-unital non-associative ring, with operations inherited from $R$.

ULift.nonUnitalRing instance

[NonUnitalRing R] : NonUnitalRing (ULift R)

Full source

instance nonUnitalRing [NonUnitalRing R] : NonUnitalRing (ULift R) :=
  { zero := (0 : ULift R), add := (· + ·), mul := (· * ·), sub := Sub.sub, neg := Neg.neg,
    nsmul := AddMonoid.nsmul, zsmul := SubNegMonoid.zsmul, add_assoc, zero_add, add_zero, add_comm,
    neg_add_cancel, left_distrib, right_distrib, zero_mul, mul_zero, mul_assoc, sub_eq_add_neg
    nsmul_zero := fun _ => AddMonoid.nsmul_zero _,
    nsmul_succ := fun _ _ => AddMonoid.nsmul_succ _ _,
    zsmul_zero' := SubNegMonoid.zsmul_zero', zsmul_succ' := SubNegMonoid.zsmul_succ',
    zsmul_neg' := SubNegMonoid.zsmul_neg' }

Non-Unital Ring Structure on Lifted Types

Informal description

For any non-unital ring $R$, the lifted type $\mathrm{ULift}\,R$ is also a non-unital ring, with operations inherited from $R$.

ULift.nonAssocRing instance

[NonAssocRing R] : NonAssocRing (ULift R)

Full source

instance nonAssocRing [NonAssocRing R] : NonAssocRing (ULift R) :=
  { zero := (0 : ULift R), one := (1 : ULift R), add := (· + ·), mul := (· * ·), sub := Sub.sub,
    neg := Neg.neg, nsmul := AddMonoid.nsmul, natCast := fun n => ULift.up n,
    intCast := fun n => ULift.up n, zsmul := SubNegMonoid.zsmul,
    intCast_ofNat := addGroupWithOne.intCast_ofNat, add_assoc, zero_add,
    add_zero, neg_add_cancel, add_comm, left_distrib, right_distrib, zero_mul, mul_zero, one_mul,
    mul_one, sub_eq_add_neg, nsmul_zero := fun _ => AddMonoid.nsmul_zero _,
    nsmul_succ := fun _ _ => AddMonoid.nsmul_succ _ _,
    zsmul_zero' := SubNegMonoid.zsmul_zero', zsmul_succ' := SubNegMonoid.zsmul_succ',
    zsmul_neg' := SubNegMonoid.zsmul_neg',
    natCast_zero := AddMonoidWithOne.natCast_zero, natCast_succ := AddMonoidWithOne.natCast_succ,
    intCast_negSucc := AddGroupWithOne.intCast_negSucc }

Lifted Non-Associative Ring Structure

Informal description

For any non-associative ring $R$, the lifted type $\mathrm{ULift}\,R$ is also a non-associative ring, with operations inherited from $R$.

ULift.ring instance

[Ring R] : Ring (ULift R)

Full source

instance ring [Ring R] : Ring (ULift R) :=
  { zero := (0 : ULift R), one := (1 : ULift R), add := (· + ·), mul := (· * ·), sub := Sub.sub,
    neg := Neg.neg, nsmul := AddMonoid.nsmul, npow := Monoid.npow, zsmul := SubNegMonoid.zsmul,
    intCast_ofNat := addGroupWithOne.intCast_ofNat, add_assoc, zero_add, add_zero, add_comm,
    left_distrib, right_distrib, zero_mul, mul_zero, mul_assoc, one_mul, mul_one, sub_eq_add_neg,
    neg_add_cancel, nsmul_zero := fun _ => AddMonoid.nsmul_zero _, natCast := fun n => ULift.up n,
    intCast := fun n => ULift.up n, nsmul_succ := fun _ _ => AddMonoid.nsmul_succ _ _,
    natCast_zero := AddMonoidWithOne.natCast_zero, natCast_succ := AddMonoidWithOne.natCast_succ,
    npow_zero := fun _ => Monoid.npow_zero _, npow_succ := fun _ _ => Monoid.npow_succ _ _,
    zsmul_zero' := SubNegMonoid.zsmul_zero', zsmul_succ' := SubNegMonoid.zsmul_succ',
    zsmul_neg' := SubNegMonoid.zsmul_neg', intCast_negSucc := AddGroupWithOne.intCast_negSucc }

Ring Structure on Lifted Types

Informal description

For any ring $R$, the lifted type $\mathrm{ULift}\,R$ is also a ring with operations lifted from $R$.

ULift.nonUnitalCommRing instance

[NonUnitalCommRing R] : NonUnitalCommRing (ULift R)

Full source

instance nonUnitalCommRing [NonUnitalCommRing R] : NonUnitalCommRing (ULift R) :=
  { zero := (0 : ULift R), add := (· + ·), mul := (· * ·), sub := Sub.sub, neg := Neg.neg,
    nsmul := AddMonoid.nsmul, zsmul := SubNegMonoid.zsmul, zero_mul, add_assoc, zero_add, add_zero,
    mul_zero, left_distrib, right_distrib, add_comm, mul_assoc, mul_comm,
    nsmul_zero := fun _ => AddMonoid.nsmul_zero _, neg_add_cancel,
    nsmul_succ := fun _ _ => AddMonoid.nsmul_succ _ _, sub_eq_add_neg,
    zsmul_zero' := SubNegMonoid.zsmul_zero',
    zsmul_succ' := SubNegMonoid.zsmul_succ',
    zsmul_neg' := SubNegMonoid.zsmul_neg'.. }

Lifted Non-Unital Commutative Ring Structure

Informal description

For any non-unital commutative ring $R$, the lifted type $\mathrm{ULift}\,R$ is also a non-unital commutative ring.

ULift.commRing instance

[CommRing R] : CommRing (ULift R)

Full source

instance commRing [CommRing R] : CommRing (ULift R) :=
  { ULift.ring with mul_comm }

Commutative Ring Structure on Lifted Types

Informal description

For any commutative ring $R$, the lifted type $\mathrm{ULift}\,R$ is also a commutative ring with operations lifted from $R$.