Documentation

Mathlib.Algebra.Ring.ULift

ULift instances for ring #

This file defines instances for ring, semiring and related structures on ULift types.

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

We also provide ULift.ringEquiv : ULift R ≃+* R.

source
@[implicit_reducible]
instance ULift.mulZeroClass {M₀ : Type u_1} [MulZeroClass M₀] :
MulZeroClass (ULift M₀)
source
@[implicit_reducible]
instance ULift.distrib {R : Type u} [Distrib R] :
Distrib (ULift R)
source
@[implicit_reducible]
instance ULift.instNatCast {R : Type u} [NatCast R] :
NatCast (ULift R)
source
@[implicit_reducible]
instance ULift.instIntCast {R : Type u} [IntCast R] :
IntCast (ULift R)
source
@[simp]
theorem ULift.up_natCast {R : Type u} [NatCast R] (n : ℕ) :
{ down := ↑n } = ↑n
source
@[simp]
theorem ULift.up_ofNat {R : Type u} [NatCast R] (n : ℕ) [n.AtLeastTwo] :
{ down := OfNat.ofNat n } = OfNat.ofNat n
source
@[simp]
theorem ULift.up_intCast {R : Type u} [IntCast R] (n : ℤ) :
{ down := ↑n } = ↑n
source
@[simp]
theorem ULift.down_natCast {R : Type u} [NatCast R] (n : ℕ) :
(↑n).down = ↑n
source
@[simp]
theorem ULift.down_ofNat {R : Type u} [NatCast R] (n : ℕ) [n.AtLeastTwo] :
(OfNat.ofNat n).down = OfNat.ofNat n
source
@[simp]
theorem ULift.down_intCast {R : Type u} [IntCast R] (n : ℤ) :
(↑n).down = ↑n
source
@[implicit_reducible]
instance ULift.addMonoidWithOne {R : Type u} [AddMonoidWithOne R] :
AddMonoidWithOne (ULift R)
source
@[implicit_reducible]
instance ULift.addCommMonoidWithOne {R : Type u} [AddCommMonoidWithOne R] :
AddCommMonoidWithOne (ULift R)
source
@[implicit_reducible]
instance ULift.addGroupWithOne {R : Type u} [AddGroupWithOne R] :
AddGroupWithOne (ULift R)
source
@[implicit_reducible]
instance ULift.addCommGroupWithOne {R : Type u} [AddCommGroupWithOne R] :
AddCommGroupWithOne (ULift R)
source
@[implicit_reducible]
instance ULift.nonUnitalNonAssocSemiring {R : Type u} [NonUnitalNonAssocSemiring R] :
NonUnitalNonAssocSemiring (ULift R)
source
@[implicit_reducible]
instance ULift.nonAssocSemiring {R : Type u} [NonAssocSemiring R] :
NonAssocSemiring (ULift R)
source
@[implicit_reducible]
instance ULift.nonUnitalSemiring {R : Type u} [NonUnitalSemiring R] :
NonUnitalSemiring (ULift R)
source
@[implicit_reducible]
instance ULift.semiring {R : Type u} [Semiring R] :
Semiring (ULift R)
source
def ULift.ringEquiv {R : Type u} [NonUnitalNonAssocSemiring R] :
ULift R ≃+* R

The ring equivalence between ULift R and R.

Instances For
    source
    @[implicit_reducible]
    instance ULift.nonUnitalCommSemiring {R : Type u} [NonUnitalCommSemiring R] :
    NonUnitalCommSemiring (ULift R)
    source
    @[implicit_reducible]
    instance ULift.commSemiring {R : Type u} [CommSemiring R] :
    CommSemiring (ULift R)
    source
    @[implicit_reducible]
    instance ULift.nonUnitalNonAssocRing {R : Type u} [NonUnitalNonAssocRing R] :
    NonUnitalNonAssocRing (ULift R)
    source
    @[implicit_reducible]
    instance ULift.nonUnitalRing {R : Type u} [NonUnitalRing R] :
    NonUnitalRing (ULift R)
    source
    @[implicit_reducible]
    instance ULift.nonAssocRing {R : Type u} [NonAssocRing R] :
    NonAssocRing (ULift R)
    source
    @[implicit_reducible]
    instance ULift.ring {R : Type u} [Ring R] :
    Ring (ULift R)
    source
    @[implicit_reducible]
    instance ULift.nonUnitalCommRing {R : Type u} [NonUnitalCommRing R] :
    NonUnitalCommRing (ULift R)
    source
    @[implicit_reducible]
    instance ULift.commRing {R : Type u} [CommRing R] :
    CommRing (ULift R)
    source
    def RingHom.ulift {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) :
    ULift R →+* ULift S

    ULift is functorial for ring homomorphisms.

    Instances For
      source
      theorem RingHom.ulift_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (x : ULift R) :
      (ulift.{u₁, u_3, u_1, u_2} f) x = { down := f x.down }
      source
      @[simp]
      theorem RingHom.down_ulift_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (x : ULift R) :
      ((ulift.{u₁, u_3, u_1, u_2} f) x).down = f x.down
      source
      theorem RingHom.comp_ulift_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) :
      ULift.ringEquiv.toRingHom.comp ((ulift.{u₁, u₂, u_1, u_2} f).comp ULift.ringEquiv.symm.toRingHom) = f