doc-next-gen

Mathlib.Algebra.Group.ULift

Module docstring

{"# ULift instances for groups and monoids

This file defines instances for group, monoid, semigroup and related structures on ULift types.

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

We also provide MulEquiv.ulift : ULift R ≃* R (and its additive analogue). "}

ULift.one instance
[One α] : One (ULift α)
Full source 
@[to_additive]
instance one [One α] : One (ULift α) :=
  ⟨⟨1⟩⟩
One Element in Lifted Types
Informal description
For any type $\alpha$ with a one element, the lifted type $\text{ULift}\,\alpha$ also has a one element.
ULift.one_down theorem
[One α] : (1 : ULift α).down = 1
Full source 
@[to_additive (attr := simp)]
theorem one_down [One α] : (1 : ULift α).down = 1 :=
  rfl
Projection of One in Lifted Type Equals One in Base Type
Informal description
For any type $\alpha$ with a one element, the projection of the one element in the lifted type $\mathrm{ULift}\,\alpha$ equals the one element in $\alpha$, i.e., $(1 : \mathrm{ULift}\,\alpha).\mathrm{down} = 1$.
ULift.mul instance
[Mul α] : Mul (ULift α)
Full source 
@[to_additive]
instance mul [Mul α] : Mul (ULift α) :=
  ⟨fun f g => ⟨f.down * g.down⟩⟩
Multiplication on Lifted Types
Informal description
For any type $\alpha$ equipped with a multiplication operation, the lifted type $\mathrm{ULift}\,\alpha$ also has a multiplication operation defined by lifting the operation from $\alpha$.
ULift.mul_down theorem
[Mul α] : (x * y).down = x.down * y.down
Full source 
@[to_additive (attr := simp)]
theorem mul_down [Mul α] : (x * y).down = x.down * y.down :=
  rfl
Projection of Product in Lifted Type Equals Product of Projections
Informal description
For any type $\alpha$ with a multiplication operation and for any elements $x, y$ in the lifted type $\mathrm{ULift}\,\alpha$, the projection of their product equals the product of their projections, i.e., $(x * y).\mathrm{down} = x.\mathrm{down} * y.\mathrm{down}$.
ULift.div instance
[Div α] : Div (ULift α)
Full source 
@[to_additive]
instance div [Div α] : Div (ULift α) :=
  ⟨fun f g => ⟨f.down / g.down⟩⟩
Division Operation on Lifted Types
Informal description
For any type $\alpha$ equipped with a division operation, the lifted type $\mathrm{ULift}\,\alpha$ also has a division operation defined componentwise.
ULift.div_down theorem
[Div α] : (x / y).down = x.down / y.down
Full source 
@[to_additive (attr := simp)]
theorem div_down [Div α] : (x / y).down = x.down / y.down :=
  rfl
Projection of Division in Lifted Types: $(x / y).\mathrm{down} = x.\mathrm{down} / y.\mathrm{down}$
Informal description
For any type $\alpha$ equipped with a division operation, and for any elements $x, y$ of the lifted type $\mathrm{ULift}\,\alpha$, the projection of the division $x / y$ to $\alpha$ equals the division of the projections of $x$ and $y$ in $\alpha$, i.e., $(x / y).\mathrm{down} = x.\mathrm{down} / y.\mathrm{down}$.
ULift.inv instance
[Inv α] : Inv (ULift α)
Full source 
@[to_additive]
instance inv [Inv α] : Inv (ULift α) :=
  ⟨fun f => ⟨f.down⁻¹⟩⟩
Inversion Operation on Lifted Types
Informal description
For any type $\alpha$ with an inversion operation, the lifted type $\text{ULift}(\alpha)$ also has an inversion operation defined componentwise.
ULift.inv_down theorem
[Inv α] : x⁻¹.down = x.down⁻¹
Full source 
@[to_additive (attr := simp)]
theorem inv_down [Inv α] : x⁻¹.down = x.down⁻¹ :=
  rfl
Inversion Commutes with Down-Projection in Lifted Types
Informal description
For any type $\alpha$ with an inversion operation and any element $x$ in the lifted type $\text{ULift}(\alpha)$, the down-projection of the inverse of $x$ equals the inverse of the down-projection of $x$, i.e., $(x^{-1}).\text{down} = (x.\text{down})^{-1}$.
ULift.smul instance
[SMul α β] : SMul α (ULift β)
Full source 
@[to_additive]
instance smul [SMul α β] : SMul α (ULift β) :=
  ⟨fun n x => up (n • x.down)⟩
Scalar Multiplication on Lifted Types
Informal description
For any types $\alpha$ and $\beta$ with a scalar multiplication operation $\alpha \times \beta \to \beta$, there is a scalar multiplication operation $\alpha \times \text{ULift}(\beta) \to \text{ULift}(\beta)$ defined by lifting the operation componentwise.
ULift.smul_down theorem
[SMul α β] (a : α) (b : ULift.{v} β) : (a • b).down = a • b.down
Full source 
@[to_additive (attr := simp)]
theorem smul_down [SMul α β] (a : α) (b : ULift.{v} β) : (a • b).down = a • b.down :=
  rfl
Scalar Multiplication Commutes with Down-Projection in Lifted Types
Informal description
For any types $\alpha$ and $\beta$ with a scalar multiplication operation $\alpha \times \beta \to \beta$, given an element $a \in \alpha$ and a lifted element $b \in \text{ULift}(\beta)$, the down-projection of the scalar product $a \bullet b$ equals the scalar product of $a$ with the down-projection of $b$, i.e., $(a \bullet b).\text{down} = a \bullet b.\text{down}$.
ULift.pow instance
[Pow α β] : Pow (ULift α) β
Full source 
@[to_additive existing (reorder := 1 2) smul]
instance pow [Pow α β] : Pow (ULift α) β :=
  ⟨fun x n => up (x.down ^ n)⟩
Power Operation on Lifted Types
Informal description
For any types $\alpha$ and $\beta$ with a power operation $\alpha^\beta$, there is a power operation $\text{ULift}(\alpha)^\beta$ defined by lifting the operation componentwise.
ULift.pow_down theorem
[Pow α β] (a : ULift.{v} α) (b : β) : (a ^ b).down = a.down ^ b
Full source 
@[to_additive existing (attr := simp) (reorder := 1 2) smul_down]
theorem pow_down [Pow α β] (a : ULift.{v} α) (b : β) : (a ^ b).down = a.down ^ b :=
  rfl
Power Operation Commutes with Down-Projection in Lifted Types
Informal description
For any types $\alpha$ and $\beta$ with a power operation $\alpha^\beta$, and for any lifted element $a \in \text{ULift}(\alpha)$ and exponent $b \in \beta$, the down-projection of $a^b$ equals the power of the down-projection of $a$ with exponent $b$, i.e., $(a^b).\text{down} = a.\text{down}^b$.
MulEquiv.ulift definition
[Mul α] : ULift α ≃* α
Full source 
/-- The multiplicative equivalence between `ULift α` and `α`.
-/
@[to_additive "The additive equivalence between `ULift α` and `α`."]
def _root_.MulEquiv.ulift [Mul α] : ULiftULift α ≃* α :=
  { Equiv.ulift with map_mul' := fun _ _ => rfl }
Multiplicative equivalence between $\mathrm{ULift}\,\alpha$ and $\alpha$
Informal description
The multiplicative equivalence between the lifted type $\mathrm{ULift}\,\alpha$ and the original type $\alpha$, where $\alpha$ is equipped with a multiplication operation. This equivalence preserves the multiplication structure, meaning that for any $x, y \in \mathrm{ULift}\,\alpha$, the equivalence maps the product $x \cdot y$ in $\mathrm{ULift}\,\alpha$ to the product of their images in $\alpha$.
ULift.semigroup instance
[Semigroup α] : Semigroup (ULift α)
Full source 
@[to_additive]
instance semigroup [Semigroup α] : Semigroup (ULift α) :=
  (MulEquiv.ulift.injective.semigroup _) fun _ _ => rfl
Semigroup Structure on Lifted Types
Informal description
For any semigroup $\alpha$, the lifted type $\mathrm{ULift}\,\alpha$ is also a semigroup with the multiplication operation inherited from $\alpha$.
ULift.commSemigroup instance
[CommSemigroup α] : CommSemigroup (ULift α)
Full source 
@[to_additive]
instance commSemigroup [CommSemigroup α] : CommSemigroup (ULift α) :=
  (Equiv.ulift.injective.commSemigroup _) fun _ _ => rfl
Commutative Semigroup Structure on Lifted Types
Informal description
For any commutative semigroup $\alpha$, the lifted type $\mathrm{ULift}\,\alpha$ is also a commutative semigroup with the multiplication operation inherited from $\alpha$.
ULift.mulOneClass instance
[MulOneClass α] : MulOneClass (ULift α)
Full source 
@[to_additive]
instance mulOneClass [MulOneClass α] : MulOneClass (ULift α) :=
  Equiv.ulift.injective.mulOneClass _ rfl (by intros; rfl)
Lifted Multiplication and One Element Structure
Informal description
For any type $\alpha$ with a multiplication operation and a one element (i.e., a `MulOneClass` structure), the lifted type $\mathrm{ULift}\,\alpha$ also inherits a `MulOneClass` structure, where the multiplication and one element are lifted from $\alpha$.
ULift.monoid instance
[Monoid α] : Monoid (ULift α)
Full source 
@[to_additive]
instance monoid [Monoid α] : Monoid (ULift α) :=
  Equiv.ulift.injective.monoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
Monoid Structure on Lifted Types
Informal description
For any monoid $\alpha$, the lifted type $\mathrm{ULift}\,\alpha$ is also a monoid with the operations lifted from $\alpha$.
ULift.commMonoid instance
[CommMonoid α] : CommMonoid (ULift α)
Full source 
@[to_additive]
instance commMonoid [CommMonoid α] : CommMonoid (ULift α) :=
  Equiv.ulift.injective.commMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
Commutative Monoid Structure on Lifted Types
Informal description
For any commutative monoid $\alpha$, the lifted type $\mathrm{ULift}\,\alpha$ is also a commutative monoid with the operations lifted from $\alpha$.
ULift.instNatCast instance
[NatCast α] : NatCast (ULift α)
Full source 
instance instNatCast [NatCast α] : NatCast (ULift α) := ⟨(up ·)⟩
Natural Number Casting on Lifted Types
Informal description
For any type $\alpha$ with a natural number casting operation, the lifted type $\text{ULift}\,\alpha$ also has a natural number casting operation.
ULift.instIntCast instance
[IntCast α] : IntCast (ULift α)
Full source 
instance instIntCast [IntCast α] : IntCast (ULift α) := ⟨(up ·)⟩
Integer Casting on Lifted Types
Informal description
For any type $\alpha$ with an integer casting operation, the lifted type $\mathrm{ULift}\,\alpha$ also inherits an integer casting operation. This means that for any integer $n$, the element $\mathrm{up}(n : \alpha)$ is well-defined in $\mathrm{ULift}\,\alpha$.
ULift.up_natCast theorem
[NatCast α] (n : ℕ) : up (n : α) = n
Full source 
@[simp, norm_cast]
theorem up_natCast [NatCast α] (n : ℕ) : up (n : α) = n :=
  rfl
Natural Number Casting Preserved Under Lifting
Informal description
For any type $\alpha$ with a natural number casting operation and any natural number $n$, the lifted element $\mathrm{up}(n : \alpha)$ in $\mathrm{ULift}\,\alpha$ is equal to $n$.
ULift.up_ofNat theorem
[NatCast α] (n : ℕ) [n.AtLeastTwo] : up (ofNat(n) : α) = ofNat(n)
Full source 
@[simp]
theorem up_ofNat [NatCast α] (n : ℕ) [n.AtLeastTwo] :
    up (ofNat(n) : α) = ofNat(n) :=
  rfl
Lifting Preserves Numerals $\geq 2$ in ULift Types
Informal description
For any type $\alpha$ with a natural number casting operation and any natural number $n \geq 2$, the lifting operation $\mathrm{up}$ maps the numeral $\mathrm{ofNat}(n)$ in $\alpha$ to the numeral $\mathrm{ofNat}(n)$ in $\mathrm{ULift}\,\alpha$. In other words, $\mathrm{up}(\mathrm{ofNat}(n) : \alpha) = \mathrm{ofNat}(n)$ in $\mathrm{ULift}\,\alpha$.
ULift.up_intCast theorem
[IntCast α] (n : ℤ) : up (n : α) = n
Full source 
@[simp, norm_cast]
theorem up_intCast [IntCast α] (n : ℤ) : up (n : α) = n :=
  rfl
Integer Cast Preservation under ULift: $\mathrm{up}(n : \alpha) = n$
Informal description
For any type $\alpha$ with an integer casting operation and any integer $n \in \mathbb{Z}$, the lift of the integer cast of $n$ in $\alpha$ is equal to $n$ in $\mathrm{ULift}\,\alpha$, i.e., $\mathrm{up}(n : \alpha) = n$.
ULift.down_natCast theorem
[NatCast α] (n : ℕ) : down (n : ULift α) = n
Full source 
@[simp, norm_cast]
theorem down_natCast [NatCast α] (n : ℕ) : down (n : ULift α) = n :=
  rfl
Projection Preserves Natural Number Casts in Lifted Types
Informal description
For any type $\alpha$ with a natural number casting operation, the projection `down` from the lifted type $\text{ULift}\,\alpha$ to $\alpha$ preserves natural number casts. Specifically, for any natural number $n$, the projection of the cast of $n$ in $\text{ULift}\,\alpha$ equals $n$ in $\alpha$, i.e., $\text{down}(n) = n$.
ULift.down_ofNat theorem
[NatCast α] (n : ℕ) [n.AtLeastTwo] : down (ofNat(n) : ULift α) = ofNat(n)
Full source 
@[simp]
theorem down_ofNat [NatCast α] (n : ℕ) [n.AtLeastTwo] :
    down (ofNat(n) : ULift α) = ofNat(n) :=
  rfl
Down Projection Preserves Numerals in Lifted Types
Informal description
For any type $\alpha$ with a natural number casting operation and any natural number $n$ (with $n \geq 2$), the down projection of the lifted numeral $\text{ofNat}(n)$ in $\text{ULift}\,\alpha$ equals $\text{ofNat}(n)$ in $\alpha$.
ULift.down_intCast theorem
[IntCast α] (n : ℤ) : down (n : ULift α) = n
Full source 
@[simp, norm_cast]
theorem down_intCast [IntCast α] (n : ℤ) : down (n : ULift α) = n :=
  rfl
Projection of Lifted Integer Cast Equals Original Integer
Informal description
For any type $\alpha$ with an integer casting operation and any integer $n \in \mathbb{Z}$, the projection of the lifted integer $n$ in $\mathrm{ULift}\,\alpha$ back to $\alpha$ equals $n$ itself. In other words, $\mathrm{down}(n : \mathrm{ULift}\,\alpha) = n$.
ULift.addMonoidWithOne instance
[AddMonoidWithOne α] : AddMonoidWithOne (ULift α)
Full source 
instance addMonoidWithOne [AddMonoidWithOne α] : AddMonoidWithOne (ULift α) :=
  { ULift.one, ULift.addMonoid with
      natCast := (⟨·⟩)
      natCast_zero := congr_arg ULift.up Nat.cast_zero,
      natCast_succ := fun _ => congr_arg ULift.up (Nat.cast_succ _) }
Additive Monoid with One Structure on Lifted Types
Informal description
For any type $\alpha$ that is an additive monoid with one, the lifted type $\mathrm{ULift}\,\alpha$ is also an additive monoid with one.
ULift.divInvMonoid instance
[DivInvMonoid α] : DivInvMonoid (ULift α)
Full source 
@[to_additive]
instance divInvMonoid [DivInvMonoid α] : DivInvMonoid (ULift α) :=
  Equiv.ulift.injective.divInvMonoid _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl
Division Monoid Structure on Lifted Types
Informal description
For any type $\alpha$ that is a division monoid, the lifted type $\mathrm{ULift}\,\alpha$ is also a division monoid, with the operations defined componentwise.
ULift.group instance
[Group α] : Group (ULift α)
Full source 
@[to_additive]
instance group [Group α] : Group (ULift α) :=
  Equiv.ulift.injective.group _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl
Group Structure on Lifted Types
Informal description
For any group $\alpha$, the lifted type $\mathrm{ULift}\,\alpha$ is also a group, with the group operations defined componentwise.
ULift.commGroup instance
[CommGroup α] : CommGroup (ULift α)
Full source 
@[to_additive]
instance commGroup [CommGroup α] : CommGroup (ULift α) :=
  Equiv.ulift.injective.commGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl
Commutative Group Structure on Lifted Types
Informal description
For any commutative group $\alpha$, the lifted type $\mathrm{ULift}\,\alpha$ is also a commutative group, with the group operations defined componentwise.
ULift.addGroupWithOne instance
[AddGroupWithOne α] : AddGroupWithOne (ULift α)
Full source 
instance addGroupWithOne [AddGroupWithOne α] : AddGroupWithOne (ULift α) :=
  { ULift.addMonoidWithOne, ULift.addGroup with
      intCast := (⟨·⟩),
      intCast_ofNat := fun _ => congr_arg ULift.up (Int.cast_natCast _),
      intCast_negSucc := fun _ => congr_arg ULift.up (Int.cast_negSucc _) }
Additive Group with One Structure on Lifted Types
Informal description
For any type $\alpha$ that is an additive group with one, the lifted type $\mathrm{ULift}\,\alpha$ is also an additive group with one, with the operations defined componentwise.
ULift.addCommGroupWithOne instance
[AddCommGroupWithOne α] : AddCommGroupWithOne (ULift α)
Full source 
instance addCommGroupWithOne [AddCommGroupWithOne α] : AddCommGroupWithOne (ULift α) :=
  { ULift.addGroupWithOne, ULift.addCommGroup with }
Additive Commutative Group with One Structure on Lifted Types
Informal description
For any type $\alpha$ that is an additive commutative group with one, the lifted type $\mathrm{ULift}\,\alpha$ is also an additive commutative group with one, with the operations defined componentwise.