Mathlib.Algebra.Equiv.TransferInstance

Equiv.one abbrev

[One β] : One α

Full source

/-- Transfer `One` across an `Equiv` -/
@[to_additive "Transfer `Zero` across an `Equiv`"]
protected abbrev one [One β] : One α :=
  ⟨e.symm 1⟩

Transfer of Multiplicative Identity via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ and a multiplicative identity structure on $\beta$, there exists a multiplicative identity structure on $\alpha$ induced by $e$.

Equiv.one_def theorem

 [One β] :
  letI := e.one
  1 = e.symm 1

Full source

@[to_additive]
theorem one_def [One β] :
    letI := e.one
    1 = e.symm 1 :=
  rfl

Definition of Transferred Multiplicative Identity via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ and a multiplicative identity structure on $\beta$, the multiplicative identity $1$ in $\alpha$ is defined as $e^{-1}(1)$, where $1$ is the multiplicative identity in $\beta$.

Equiv.instOneShrink instance

[Small.{v} α] [One α] : One (Shrink.{v} α)

Full source

@[to_additive]
noncomputable instance [Small.{v} α] [One α] : One (Shrink.{v} α) :=
  (equivShrink α).symm.one

Multiplicative Identity on Shrink of a Small Type

Informal description

For any type $\alpha$ that is $v$-small and has a multiplicative identity structure, the model $\operatorname{Shrink}_v \alpha$ in the universe $\operatorname{Type} v$ also has a multiplicative identity structure induced by the equivalence between $\alpha$ and its shrink.

Equiv.mul abbrev

[Mul β] : Mul α

Full source

/-- Transfer `Mul` across an `Equiv` -/
@[to_additive "Transfer `Add` across an `Equiv`"]
protected abbrev mul [Mul β] : Mul α :=
  ⟨fun x y => e.symm (e x * e y)⟩

Transfer of Multiplication via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ and a multiplication operation $*$ on $\beta$, there exists a multiplication operation on $\alpha$ defined by $x * y = e^{-1}(e(x) * e(y))$ for all $x, y \in \alpha$.

Equiv.mul_def theorem

 [Mul β] (x y : α) :
  letI := Equiv.mul e
  x * y = e.symm (e x * e y)

Full source

@[to_additive]
theorem mul_def [Mul β] (x y : α) :
    letI := Equiv.mul e
    x * y = e.symm (e x * e y) :=
  rfl

Definition of Transferred Multiplication via Equivalence: $x * y = e^{-1}(e(x) * e(y))$

Informal description

Given an equivalence $e : \alpha \simeq \beta$ and a multiplication operation $*$ on $\beta$, the induced multiplication operation on $\alpha$ satisfies $x * y = e^{-1}(e(x) * e(y))$ for all $x, y \in \alpha$.

Equiv.instMulShrink instance

[Small.{v} α] [Mul α] : Mul (Shrink.{v} α)

Full source

@[to_additive]
noncomputable instance [Small.{v} α] [Mul α] : Mul (Shrink.{v} α) :=
  (equivShrink α).symm.mul

Multiplication Structure on Shrink Types via Equivalence

Informal description

For any type $\alpha$ that is $v$-small and equipped with a multiplication operation, its model $\mathrm{Shrink}(\alpha)$ in the universe $\mathrm{Type}\,v$ inherits a multiplication operation via the equivalence $\alpha \simeq \mathrm{Shrink}(\alpha)$. The multiplication on $\mathrm{Shrink}(\alpha)$ is defined by $x * y = e(e^{-1}(x) * e^{-1}(y))$ for all $x, y \in \mathrm{Shrink}(\alpha)$, where $e$ is the equivalence between $\alpha$ and $\mathrm{Shrink}(\alpha)$.

Equiv.div abbrev

[Div β] : Div α

Full source

/-- Transfer `Div` across an `Equiv` -/
@[to_additive "Transfer `Sub` across an `Equiv`"]
protected abbrev div [Div β] : Div α :=
  ⟨fun x y => e.symm (e x / e y)⟩

Transfer of Division Operation via Equivalence

Informal description

Given a type $\beta$ equipped with a division operation and an equivalence $e : \alpha \simeq \beta$, the type $\alpha$ can be equipped with a division operation defined by $x / y = e^{-1}(e(x) / e(y))$ for all $x, y \in \alpha$.

Equiv.div_def theorem

 [Div β] (x y : α) :
  letI := Equiv.div e
  x / y = e.symm (e x / e y)

Full source

@[to_additive]
theorem div_def [Div β] (x y : α) :
    letI := Equiv.div e
    x / y = e.symm (e x / e y) :=
  rfl

Definition of Transferred Division via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, where $\beta$ is equipped with a division operation, the division operation on $\alpha$ induced by $e$ is defined by: \[ x / y = e^{-1}(e(x) / e(y)) \] for all $x, y \in \alpha$.

Equiv.instDivShrink instance

[Small.{v} α] [Div α] : Div (Shrink.{v} α)

Full source

@[to_additive]
noncomputable instance [Small.{v} α] [Div α] : Div (Shrink.{v} α) :=
  (equivShrink α).symm.div

Division Operation on the Shrink of a Small Type

Informal description

For any type $\alpha$ that is $v$-small and equipped with a division operation, the model $\mathrm{Shrink}_{v}(\alpha)$ in a smaller universe inherits a division operation via the equivalence between $\alpha$ and its shrink.

Equiv.Inv abbrev

[Inv β] : Inv α

Full source

/-- Transfer `Inv` across an `Equiv` -/
@[to_additive "Transfer `Neg` across an `Equiv`"]
protected abbrev Inv [Inv β] : Inv α :=
  ⟨fun x => e.symm (e x)⁻¹⟩

Inversion Operation Transfer via Equivalence

Informal description

Given an equivalence (bijection) $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and an inversion operation on $\beta$, we can define an inversion operation on $\alpha$ by transporting the structure from $\beta$ to $\alpha$ via $e$. Specifically, for any $x \in \alpha$, its inverse is defined as $x^{-1} = e^{-1}((e(x))^{-1})$, where $e^{-1}$ is the inverse of the equivalence $e$.

Equiv.inv_def theorem

 [Inv β] (x : α) :
  letI := Equiv.Inv e
  x⁻¹ = e.symm (e x)⁻¹

Full source

@[to_additive]
theorem inv_def [Inv β] (x : α) :
    letI := Equiv.Inv e
    x⁻¹ = e.symm (e x)⁻¹ :=
  rfl

Definition of Induced Inversion via Equivalence

Informal description

Given an equivalence (bijection) $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and an inversion operation on $\beta$, the induced inversion operation on $\alpha$ satisfies $x^{-1} = e^{-1}((e(x))^{-1})$ for any $x \in \alpha$, where $e^{-1}$ is the inverse of $e$.

Equiv.instInvShrink instance

[Small.{v} α] [Inv α] : Inv (Shrink.{v} α)

Full source

@[to_additive]
noncomputable instance [Small.{v} α] [Inv α] : Inv (Shrink.{v} α) :=
  (equivShrink α).symm.Inv

Inversion Operation on Shrink Model of a Small Type

Informal description

For any type $\alpha$ that is $v$-small and equipped with an inversion operation, the model $\mathrm{Shrink}(\alpha)$ in the universe $\mathrm{Type}\,v$ also inherits an inversion operation via the equivalence between $\alpha$ and $\mathrm{Shrink}(\alpha)$. Specifically, for any $x \in \mathrm{Shrink}(\alpha)$, its inverse is defined as $x^{-1} = e^{-1}((e(x))^{-1})$, where $e : \alpha \simeq \mathrm{Shrink}(\alpha)$ is the canonical equivalence.

Equiv.smul abbrev

(R : Type*) [SMul R β] : SMul R α

Full source

/-- Transfer `SMul` across an `Equiv` -/
protected abbrev smul (R : Type*) [SMul R β] : SMul R α :=
  ⟨fun r x => e.symm (r • e x)⟩

Induced Scalar Multiplication via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ and a scalar multiplication operation $\bullet : R \times \beta \to \beta$ for some type $R$, there exists an induced scalar multiplication operation $\bullet : R \times \alpha \to \alpha$ defined by $r \bullet x = e^{-1}(r \bullet e(x))$ for all $r \in R$ and $x \in \alpha$.

Equiv.smul_def theorem

 {R : Type*} [SMul R β] (r : R) (x : α) :
  letI := e.smul R
  r • x = e.symm (r • e x)

Full source

theorem smul_def {R : Type*} [SMul R β] (r : R) (x : α) :
    letI := e.smul R
    r • x = e.symm (r • e x) :=
  rfl

Definition of Induced Scalar Multiplication via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$, a type $R$ with a scalar multiplication operation $\bullet : R \times \beta \to \beta$, and elements $r \in R$, $x \in \alpha$, the induced scalar multiplication on $\alpha$ satisfies $r \bullet x = e^{-1}(r \bullet e(x))$.

Equiv.instSMulShrink instance

[Small.{v} α] (R : Type*) [SMul R α] : SMul R (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] (R : Type*) [SMul R α] : SMul R (Shrink.{v} α) :=
  (equivShrink α).symm.smul R

Scalar Multiplication on Shrink Types via Equivalence

Informal description

For any type $\alpha$ that is $v$-small and equipped with a scalar multiplication operation by elements of type $R$, the model $\operatorname{Shrink} \alpha$ in the smaller universe also inherits a scalar multiplication operation from $R$.

Equiv.pow definition

(N : Type*) [Pow β N] : Pow α N

Full source

/-- Transfer `Pow` across an `Equiv` -/
@[reducible, to_additive existing smul]
protected def pow (N : Type*) [Pow β N] : Pow α N :=
  ⟨fun x n => e.symm (e x ^ n)⟩

Power operation transfer via equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ and a power operation $\beta^N$ defined on $\beta$, the power operation $\alpha^N$ is defined on $\alpha$ by $x^n = e^{-1}(e(x)^n)$ for any $x \in \alpha$ and $n \in N$.

Equiv.pow_def theorem

 {N : Type*} [Pow β N] (n : N) (x : α) :
  letI := e.pow N
  x ^ n = e.symm (e x ^ n)

Full source

theorem pow_def {N : Type*} [Pow β N] (n : N) (x : α) :
    letI := e.pow N
    x ^ n = e.symm (e x ^ n) :=
  rfl

Definition of Power Operation via Equivalence: $x^n = e^{-1}(e(x)^n)$

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a power operation $\beta^N$ defined on $\beta$, then for any $x \in \alpha$ and $n \in N$, the power operation on $\alpha$ is defined by $x^n = e^{-1}(e(x)^n)$, where $e^{-1}$ is the inverse of $e$.

Equiv.instPowShrink instance

[Small.{v} α] (N : Type*) [Pow α N] : Pow (Shrink.{v} α) N

Full source

noncomputable instance [Small.{v} α] (N : Type*) [Pow α N] : Pow (Shrink.{v} α) N :=
  (equivShrink α).symm.pow N

Power Operation on Shrink via Equivalence

Informal description

For any $v$-small type $\alpha$ with a power operation $\alpha^N$ defined for some type $N$, the model `Shrink α` in the universe `Type v` inherits a power operation $(Shrink \alpha)^N$ via the equivalence between $\alpha$ and `Shrink α`.

Equiv.mulEquiv definition

 (e : α ≃ β) [Mul β] :
  let _ := Equiv.mul e
  α ≃* β

Full source

/-- An equivalence `e : α ≃ β` gives a multiplicative equivalence `α ≃* β` where
the multiplicative structure on `α` is the one obtained by transporting a multiplicative structure
on `β` back along `e`. -/
@[to_additive "An equivalence `e : α ≃ β` gives an additive equivalence `α ≃+ β` where
the additive structure on `α` is the one obtained by transporting an additive structure
on `β` back along `e`."]
def mulEquiv (e : α ≃ β) [Mul β] :
    let _ := Equiv.mul e
    α ≃* β := by
  intros
  exact
    { e with
      map_mul' := fun x y => by
        apply e.symm.injective
        simp [mul_def] }

Multiplicative equivalence via transport

Informal description

Given an equivalence $e : \alpha \simeq \beta$ and a multiplication operation on $\beta$, this defines a multiplicative equivalence (isomorphism) between $\alpha$ and $\beta$, where the multiplication on $\alpha$ is obtained by transporting the multiplication from $\beta$ along $e$. Specifically, for any $x, y \in \alpha$, the multiplication is defined as $x * y = e^{-1}(e(x) * e(y))$.

Equiv.mulEquiv_apply theorem

(e : α ≃ β) [Mul β] (a : α) : (mulEquiv e) a = e a

Full source

@[to_additive (attr := simp)]
theorem mulEquiv_apply (e : α ≃ β) [Mul β] (a : α) : (mulEquiv e) a = e a :=
  rfl

Application of Multiplicative Equivalence via Transport: $(e^*)(a) = e(a)$

Informal description

Given an equivalence $e : \alpha \simeq \beta$ and a multiplication operation on $\beta$, the multiplicative equivalence $\alpha \simeq^* \beta$ obtained by transporting the multiplication structure satisfies $(e^*)(a) = e(a)$ for any $a \in \alpha$.

Equiv.mulEquiv_symm_apply theorem

 (e : α ≃ β) [Mul β] (b : β) :
  letI := Equiv.mul e
  (mulEquiv e).symm b = e.symm b

Full source

@[to_additive]
theorem mulEquiv_symm_apply (e : α ≃ β) [Mul β] (b : β) :
    letI := Equiv.mul e
    (mulEquiv e).symm b = e.symm b :=
  rfl

Inverse of Transported Multiplicative Equivalence: $(e^*)^{-1}(b) = e^{-1}(b)$

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$ with a multiplication operation on $\beta$, and given $b \in \beta$, the inverse of the multiplicative equivalence $(e^*)$ satisfies $(e^*)^{-1}(b) = e^{-1}(b)$, where $e^{-1}$ is the inverse of the equivalence $e$.

Shrink.mulEquiv definition

[Small.{v} α] [Mul α] : Shrink.{v} α ≃* α

Full source

/-- Shrink `α` to a smaller universe preserves multiplication. -/
@[to_additive "Shrink `α` to a smaller universe preserves addition."]
noncomputable def _root_.Shrink.mulEquiv [Small.{v} α] [Mul α] : ShrinkShrink.{v} α ≃* α :=
  (equivShrink α).symm.mulEquiv

Multiplicative equivalence between a shrunken type and its original

Informal description

For a type $\alpha$ that is $v$-small and equipped with a multiplication operation, the multiplicative equivalence $\mathrm{Shrink}(\alpha) \simeq^* \alpha$ is defined by composing the inverse of the equivalence $\alpha \simeq \mathrm{Shrink}(\alpha)$ with the multiplicative structure transport. This gives an isomorphism between the shrunken type $\mathrm{Shrink}(\alpha)$ and $\alpha$ that preserves multiplication.

Equiv.ringEquiv definition

 (e : α ≃ β) [Add β] [Mul β] : by
  let add := Equiv.add e
  let mul := Equiv.mul e
  exact α ≃+* β

Full source

/-- An equivalence `e : α ≃ β` gives a ring equivalence `α ≃+* β`
where the ring structure on `α` is
the one obtained by transporting a ring structure on `β` back along `e`.
-/
def ringEquiv (e : α ≃ β) [Add β] [Mul β] : by
    let add := Equiv.add e
    let mul := Equiv.mul e
    exact α ≃+* β := by
  intros
  exact
    { e with
      map_add' := fun x y => by
        apply e.symm.injective
        simp [add_def]
      map_mul' := fun x y => by
        apply e.symm.injective
        simp [mul_def] }

Ring equivalence via transport of structure

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and given addition and multiplication operations on $\beta$, the function `ringEquiv e` constructs a ring equivalence $\alpha \simeq+* \beta$ where the ring structure on $\alpha$ is obtained by transporting the ring structure from $\beta$ back along $e$. Specifically, the addition and multiplication on $\alpha$ are defined by: - $x + y = e^{-1}(e(x) + e(y))$ - $x * y = e^{-1}(e(x) * e(y))$ for all $x, y \in \alpha$.

Equiv.ringEquiv_apply theorem

(e : α ≃ β) [Add β] [Mul β] (a : α) : (ringEquiv e) a = e a

Full source

@[simp]
theorem ringEquiv_apply (e : α ≃ β) [Add β] [Mul β] (a : α) : (ringEquiv e) a = e a :=
  rfl

Application of Ring Equivalence via Transport of Structure

Informal description

Let $e : \alpha \simeq \beta$ be an equivalence between types $\alpha$ and $\beta$, and suppose $\beta$ is equipped with addition and multiplication operations. For any element $a \in \alpha$, the ring equivalence $\text{ringEquiv}(e)$ satisfies $\text{ringEquiv}(e)(a) = e(a)$.

Equiv.ringEquiv_symm_apply theorem

 (e : α ≃ β) [Add β] [Mul β] (b : β) : by
  letI := Equiv.add e
  letI := Equiv.mul e
  exact (ringEquiv e).symm b = e.symm b

Full source

theorem ringEquiv_symm_apply (e : α ≃ β) [Add β] [Mul β] (b : β) : by
    letI := Equiv.add e
    letI := Equiv.mul e
    exact (ringEquiv e).symm b = e.symm b := rfl

Inverse of Transported Ring Equivalence Matches Inverse Equivalence

Informal description

Let $e : \alpha \simeq \beta$ be an equivalence between types $\alpha$ and $\beta$, and suppose $\beta$ is equipped with addition and multiplication operations. Then, for any $b \in \beta$, the image of $b$ under the inverse of the ring equivalence $\text{ringEquiv}(e)$ equals the image of $b$ under the inverse equivalence $e^{-1}$, i.e., $(\text{ringEquiv}(e))^{-1}(b) = e^{-1}(b)$.

Shrink.ringEquiv definition

[Small.{v} α] [Add α] [Mul α] : Shrink.{v} α ≃+* α

Full source

/-- Shrink `α` to a smaller universe preserves ring structure. -/
noncomputable def _root_.Shrink.ringEquiv [Small.{v} α] [Add α] [Mul α] : ShrinkShrink.{v} α ≃+* α :=
  (equivShrink α).symm.ringEquiv

Ring equivalence between a small type and its model

Informal description

For a $v$-small type $\alpha$ equipped with addition and multiplication operations, the function `Shrink.ringEquiv` provides a ring equivalence between the model `Shrink α` in the universe `Type v` and $\alpha$. This equivalence transports the ring structure from $\alpha$ to `Shrink α` via the inverse of the equivalence `equivShrink α`.

Equiv.semigroup abbrev

[Semigroup β] : Semigroup α

Full source

/-- Transfer `Semigroup` across an `Equiv` -/
@[to_additive "Transfer `add_semigroup` across an `Equiv`"]
protected abbrev semigroup [Semigroup β] : Semigroup α := by
  let mul := e.mul
  apply e.injective.semigroup _; intros; exact e.apply_symm_apply _

Transfer of Semigroup Structure via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a semigroup structure on $\beta$ with multiplication $*$, then $\alpha$ can be endowed with a semigroup structure where the multiplication is defined by $x \cdot y = e^{-1}(e(x) * e(y))$ for all $x, y \in \alpha$.

Equiv.instSemigroupShrink instance

[Small.{v} α] [Semigroup α] : Semigroup (Shrink.{v} α)

Full source

@[to_additive]
noncomputable instance [Small.{v} α] [Semigroup α] : Semigroup (Shrink.{v} α) :=
  (equivShrink α).symm.semigroup

Semigroup Structure on Shrink of a Small Semigroup

Informal description

For any $v$-small type $\alpha$ with a semigroup structure, the model `Shrink.{v} α` in the universe `Type v` inherits a semigroup structure via the equivalence between $\alpha$ and `Shrink α$. The multiplication on `Shrink α` is defined by transporting the multiplication from $\alpha$ through this equivalence.

Equiv.semigroupWithZero abbrev

[SemigroupWithZero β] : SemigroupWithZero α

Full source

/-- Transfer `SemigroupWithZero` across an `Equiv` -/
protected abbrev semigroupWithZero [SemigroupWithZero β] : SemigroupWithZero α := by
  let mul := e.mul
  let zero := e.zero
  apply e.injective.semigroupWithZero _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Semigroup-with-Zero Structure via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a semigroup-with-zero structure on $\beta$, there exists a semigroup-with-zero structure on $\alpha$ where the multiplication operation is defined by $x * y = e^{-1}(e(x) * e(y))$ for all $x, y \in \alpha$ and the zero element is $e^{-1}(0)$.

Equiv.instSemigroupWithZeroShrink instance

[Small.{v} α] [SemigroupWithZero α] : SemigroupWithZero (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [SemigroupWithZero α] : SemigroupWithZero (Shrink.{v} α) :=
  (equivShrink α).symm.semigroupWithZero

Semigroup-with-Zero Structure on Shrink of a Small Type

Informal description

For any $v$-small type $\alpha$ with a semigroup-with-zero structure, the model $\mathrm{Shrink}_{v}(\alpha)$ in the smaller universe also inherits a semigroup-with-zero structure, where the multiplication and zero are transferred via the equivalence between $\alpha$ and its shrink.

Equiv.commSemigroup abbrev

[CommSemigroup β] : CommSemigroup α

Full source

/-- Transfer `CommSemigroup` across an `Equiv` -/
@[to_additive "Transfer `AddCommSemigroup` across an `Equiv`"]
protected abbrev commSemigroup [CommSemigroup β] : CommSemigroup α := by
  let mul := e.mul
  apply e.injective.commSemigroup _; intros; exact e.apply_symm_apply _

Transfer of Commutative Semigroup Structure via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a commutative semigroup structure on $\beta$, there exists a commutative semigroup structure on $\alpha$ where the multiplication is defined by $x * y = e^{-1}(e(x) * e(y))$ for all $x, y \in \alpha$.

Equiv.instCommSemigroupShrink instance

[Small.{v} α] [CommSemigroup α] : CommSemigroup (Shrink.{v} α)

Full source

@[to_additive]
noncomputable instance [Small.{v} α] [CommSemigroup α] : CommSemigroup (Shrink.{v} α) :=
  (equivShrink α).symm.commSemigroup

Commutative Semigroup Structure on Shrink of a Small Commutative Semigroup

Informal description

For any $v$-small type $\alpha$ with a commutative semigroup structure, the type $\operatorname{Shrink}_v \alpha$ (a model of $\alpha$ in a smaller universe) inherits a commutative semigroup structure via the equivalence $\alpha \simeq \operatorname{Shrink}_v \alpha$. The multiplication on $\operatorname{Shrink}_v \alpha$ is defined by transporting the multiplication from $\alpha$ through this equivalence.

Equiv.mulZeroClass abbrev

[MulZeroClass β] : MulZeroClass α

Full source

/-- Transfer `MulZeroClass` across an `Equiv` -/
protected abbrev mulZeroClass [MulZeroClass β] : MulZeroClass α := by
  let zero := e.zero
  let mul := e.mul
  apply e.injective.mulZeroClass _ <;> intros <;> exact e.apply_symm_apply _

Transfer of `MulZeroClass` structure via equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a `MulZeroClass` structure on $\beta$, there exists a `MulZeroClass` structure on $\alpha$ where: - The multiplication is defined by $x * y = e^{-1}(e(x) * e(y))$ for all $x, y \in \alpha$ - The zero element is defined as $0 = e^{-1}(0)$

Equiv.instMulZeroClassShrink instance

[Small.{v} α] [MulZeroClass α] : MulZeroClass (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [MulZeroClass α] : MulZeroClass (Shrink.{v} α) :=
  (equivShrink α).symm.mulZeroClass

Transfer of `MulZeroClass` Structure to Shrink Model

Informal description

For any type $\alpha$ that is $v$-small and has a `MulZeroClass` structure, the model `Shrink.{v} α` in the smaller universe also inherits a `MulZeroClass` structure. The multiplication and zero element on `Shrink α` are defined via the equivalence between $\alpha$ and `Shrink α$: - The multiplication is given by $x * y = e^{-1}(e(x) * e(y))$ for all $x, y \in \text{Shrink } \alpha$, where $e$ is the equivalence between $\alpha$ and $\text{Shrink } \alpha$. - The zero element is $0 = e^{-1}(0_\alpha)$.

Equiv.mulOneClass abbrev

[MulOneClass β] : MulOneClass α

Full source

/-- Transfer `MulOneClass` across an `Equiv` -/
@[to_additive "Transfer `AddZeroClass` across an `Equiv`"]
protected abbrev mulOneClass [MulOneClass β] : MulOneClass α := by
  let one := e.one
  let mul := e.mul
  apply e.injective.mulOneClass _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Multiplicative Structure with Identity via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a multiplicative structure with identity (`MulOneClass`) on $\beta$, there exists a multiplicative structure with identity on $\alpha$ induced by $e$. Specifically, the multiplication and identity on $\alpha$ are defined by: - $x * y = e^{-1}(e(x) * e(y))$ for all $x, y \in \alpha$, - $1_\alpha = e^{-1}(1_\beta)$.

Equiv.instMulOneClassShrink instance

[Small.{v} α] [MulOneClass α] : MulOneClass (Shrink.{v} α)

Full source

@[to_additive]
noncomputable instance [Small.{v} α] [MulOneClass α] : MulOneClass (Shrink.{v} α) :=
  (equivShrink α).symm.mulOneClass

Transfer of Multiplicative Structure with Identity to Shrink Type

Informal description

For any $v$-small type $\alpha$ equipped with a multiplicative structure with identity (`MulOneClass`), the model type `Shrink.{v} α` in the smaller universe `Type v` inherits a multiplicative structure with identity. Specifically, the multiplication and identity on `Shrink α` are defined via the equivalence between $\alpha$ and `Shrink α$.

Equiv.mulZeroOneClass abbrev

[MulZeroOneClass β] : MulZeroOneClass α

Full source

/-- Transfer `MulZeroOneClass` across an `Equiv` -/
protected abbrev mulZeroOneClass [MulZeroOneClass β] : MulZeroOneClass α := by
  let zero := e.zero
  let one := e.one
  let mul := e.mul
  apply e.injective.mulZeroOneClass _ <;> intros <;> exact e.apply_symm_apply _

Transfer of `MulZeroOneClass` Structure via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a `MulZeroOneClass` structure on $\beta$, there exists a `MulZeroOneClass` structure on $\alpha$ induced by $e$. This means $\alpha$ inherits a multiplication operation with zero and one from $\beta$ via the equivalence $e$.

Equiv.instMulZeroOneClassShrink instance

[Small.{v} α] [MulZeroOneClass α] : MulZeroOneClass (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [MulZeroOneClass α] : MulZeroOneClass (Shrink.{v} α) :=
  (equivShrink α).symm.mulZeroOneClass

Transfer of `MulZeroOneClass` Structure to Shrink Model

Informal description

For any $v$-small type $\alpha$ with a `MulZeroOneClass` structure, the model `Shrink.{v} α` in a smaller universe inherits a `MulZeroOneClass` structure via the equivalence between $\alpha$ and its shrink. Specifically, the multiplication, zero, and one on `Shrink α` are defined by transporting the corresponding operations from $\alpha$ through the equivalence.

Equiv.monoid abbrev

[Monoid β] : Monoid α

Full source

/-- Transfer `Monoid` across an `Equiv` -/
@[to_additive "Transfer `AddMonoid` across an `Equiv`"]
protected abbrev monoid [Monoid β] : Monoid α := by
  let one := e.one
  let mul := e.mul
  let pow := e.pow ℕ
  apply e.injective.monoid _ <;> intros <;> exact e.apply_symm_apply _

Monoid Structure Transfer via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a monoid structure on $\beta$, there exists a monoid structure on $\alpha$ induced by $e$. Specifically: - The multiplication on $\alpha$ is defined by $x \cdot y = e^{-1}(e(x) \cdot e(y))$ for all $x, y \in \alpha$. - The multiplicative identity on $\alpha$ is $1_\alpha = e^{-1}(1_\beta)$. - The natural number power operation on $\alpha$ is defined by $x^n = e^{-1}(e(x)^n)$ for all $x \in \alpha$ and $n \in \mathbb{N}$.

Equiv.instMonoidShrink instance

[Small.{v} α] [Monoid α] : Monoid (Shrink.{v} α)

Full source

@[to_additive]
noncomputable instance [Small.{v} α] [Monoid α] : Monoid (Shrink.{v} α) :=
  (equivShrink α).symm.monoid

Monoid Structure Transfer to Shrink Model via Equivalence

Informal description

For any $v$-small type $\alpha$ equipped with a monoid structure, the model `Shrink.{v} α` in a smaller universe inherits a monoid structure via the equivalence between $\alpha$ and its model. Specifically: - The multiplication on `Shrink α` is defined by $x \cdot y = e(e^{-1}(x) \cdot e^{-1}(y))$ for all $x, y \in \text{Shrink } \alpha$, where $e : \alpha \simeq \text{Shrink } \alpha$ is the equivalence. - The multiplicative identity on `Shrink α` is $1 = e(1_\alpha)$. - The natural number power operation on `Shrink α` is defined by $x^n = e(e^{-1}(x)^n)$ for all $x \in \text{Shrink } \alpha$ and $n \in \mathbb{N}$.

Equiv.commMonoid abbrev

[CommMonoid β] : CommMonoid α

Full source

/-- Transfer `CommMonoid` across an `Equiv` -/
@[to_additive "Transfer `AddCommMonoid` across an `Equiv`"]
protected abbrev commMonoid [CommMonoid β] : CommMonoid α := by
  let one := e.one
  let mul := e.mul
  let pow := e.pow ℕ
  apply e.injective.commMonoid _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Commutative Monoid Structure via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, if $\beta$ has a commutative monoid structure, then $\alpha$ can be endowed with a commutative monoid structure via $e$. Specifically, the multiplication and identity on $\alpha$ are defined by: - $x \cdot y = e^{-1}(e(x) \cdot e(y))$ for all $x, y \in \alpha$, - $1_\alpha = e^{-1}(1_\beta)$.

Equiv.instCommMonoidShrink instance

[Small.{v} α] [CommMonoid α] : CommMonoid (Shrink.{v} α)

Full source

@[to_additive]
noncomputable instance [Small.{v} α] [CommMonoid α] : CommMonoid (Shrink.{v} α) :=
  (equivShrink α).symm.commMonoid

Commutative Monoid Structure on Shrink via Equivalence

Informal description

For any $v$-small type $\alpha$ with a commutative monoid structure, the model $\operatorname{Shrink}(\alpha)$ in a smaller universe also inherits a commutative monoid structure via the equivalence $\alpha \simeq \operatorname{Shrink}(\alpha)$. Specifically, the multiplication and identity on $\operatorname{Shrink}(\alpha)$ are defined by transporting the corresponding operations from $\alpha$ through the equivalence.

Equiv.group abbrev

[Group β] : Group α

Full source

/-- Transfer `Group` across an `Equiv` -/
@[to_additive "Transfer `AddGroup` across an `Equiv`"]
protected abbrev group [Group β] : Group α := by
  let one := e.one
  let mul := e.mul
  let inv := e.Inv
  let div := e.div
  let npow := e.pow ℕ
  let zpow := e.pow ℤ
  apply e.injective.group _ <;> intros <;> exact e.apply_symm_apply _

Group Structure Transfer via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a group structure on $\beta$, the type $\alpha$ can be endowed with a group structure where: - The multiplication is defined by $x \cdot y = e^{-1}(e(x) \cdot e(y))$ for all $x, y \in \alpha$, - The identity element is $1_\alpha = e^{-1}(1_\beta)$, - The inverse operation is $x^{-1} = e^{-1}((e(x))^{-1})$ for all $x \in \alpha$.

Equiv.instGroupShrink instance

[Small.{v} α] [Group α] : Group (Shrink.{v} α)

Full source

@[to_additive]
noncomputable instance [Small.{v} α] [Group α] : Group (Shrink.{v} α) :=
  (equivShrink α).symm.group

Group Structure on Shrink via Equivalence

Informal description

For any $v$-small type $\alpha$ equipped with a group structure, the model $\operatorname{Shrink}(\alpha)$ in a smaller universe inherits a group structure via the equivalence $\alpha \simeq \operatorname{Shrink}(\alpha)$. Specifically, the group operations on $\operatorname{Shrink}(\alpha)$ are defined by transporting the corresponding operations from $\alpha$ through the equivalence.

Equiv.commGroup abbrev

[CommGroup β] : CommGroup α

Full source

/-- Transfer `CommGroup` across an `Equiv` -/
@[to_additive "Transfer `AddCommGroup` across an `Equiv`"]
protected abbrev commGroup [CommGroup β] : CommGroup α := by
  let one := e.one
  let mul := e.mul
  let inv := e.Inv
  let div := e.div
  let npow := e.pow ℕ
  let zpow := e.pow ℤ
  apply e.injective.commGroup _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Commutative Group Structure via Equivalence

Informal description

Given a commutative group structure on a type $\beta$ and an equivalence (bijection) $e : \alpha \simeq \beta$, the type $\alpha$ can be endowed with a commutative group structure where: - The multiplication is defined by $x \cdot y = e^{-1}(e(x) \cdot e(y))$ for all $x, y \in \alpha$, - The identity element is $1_\alpha = e^{-1}(1_\beta)$, - The inverse operation is $x^{-1} = e^{-1}((e(x))^{-1})$ for all $x \in \alpha$, - The division operation is $x / y = e^{-1}(e(x) / e(y))$ for all $x, y \in \alpha$, - The power operations (natural and integer) are defined by $x^n = e^{-1}(e(x)^n)$ for all $x \in \alpha$ and $n \in \mathbb{N}$ or $n \in \mathbb{Z}$.

Equiv.instCommGroupShrink instance

[Small.{v} α] [CommGroup α] : CommGroup (Shrink.{v} α)

Full source

@[to_additive]
noncomputable instance [Small.{v} α] [CommGroup α] : CommGroup (Shrink.{v} α) :=
  (equivShrink α).symm.commGroup

Commutative Group Structure on Shrink Models via Equivalence

Informal description

For any $v$-small type $\alpha$ equipped with a commutative group structure, the model $\operatorname{Shrink}(\alpha)$ in a smaller universe inherits a commutative group structure via the equivalence $\alpha \simeq \operatorname{Shrink}(\alpha)$. Specifically, the group operations on $\operatorname{Shrink}(\alpha)$ are defined by transporting the corresponding operations from $\alpha$ through the equivalence.

Equiv.nonUnitalNonAssocSemiring abbrev

[NonUnitalNonAssocSemiring β] : NonUnitalNonAssocSemiring α

Full source

/-- Transfer `NonUnitalNonAssocSemiring` across an `Equiv` -/
protected abbrev nonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring β] :
    NonUnitalNonAssocSemiring α := by
  let zero := e.zero
  let add := e.add
  let mul := e.mul
  let nsmul := e.smul ℕ
  apply e.injective.nonUnitalNonAssocSemiring _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Non-Unital Non-Associative Semiring Structure via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a non-unital non-associative semiring structure on $\beta$, there exists an induced non-unital non-associative semiring structure on $\alpha$ defined by transporting the operations from $\beta$ via $e$.

Equiv.instNonUnitalNonAssocSemiringShrink instance

[Small.{v} α] [NonUnitalNonAssocSemiring α] : NonUnitalNonAssocSemiring (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [NonUnitalNonAssocSemiring α] :
    NonUnitalNonAssocSemiring (Shrink.{v} α) :=
  (equivShrink α).symm.nonUnitalNonAssocSemiring

Non-Unital Non-Associative Semiring Structure on Shrink Models

Informal description

For any type $\alpha$ that is $v$-small and equipped with a non-unital non-associative semiring structure, the model $\mathrm{Shrink}_v(\alpha)$ in the same universe also inherits a non-unital non-associative semiring structure via the canonical equivalence $\alpha \simeq \mathrm{Shrink}_v(\alpha)$.

Equiv.nonUnitalSemiring abbrev

[NonUnitalSemiring β] : NonUnitalSemiring α

Full source

/-- Transfer `NonUnitalSemiring` across an `Equiv` -/
protected abbrev nonUnitalSemiring [NonUnitalSemiring β] : NonUnitalSemiring α := by
  let zero := e.zero
  let add := e.add
  let mul := e.mul
  let nsmul := e.smul ℕ
  apply e.injective.nonUnitalSemiring _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Non-Unital Semiring Structure via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a non-unital semiring structure on $\beta$, there exists a non-unital semiring structure on $\alpha$ induced by $e$. The operations on $\alpha$ are defined by: - Addition: $x + y = e^{-1}(e(x) + e(y))$ - Multiplication: $x * y = e^{-1}(e(x) * e(y))$ - Zero: $0 = e^{-1}(0)$ - Scalar multiplication: $r \cdot x = e^{-1}(r \cdot e(x))$ (for $r \in \mathbb{N}$)

Equiv.instNonUnitalSemiringShrink instance

[Small.{v} α] [NonUnitalSemiring α] : NonUnitalSemiring (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [NonUnitalSemiring α] : NonUnitalSemiring (Shrink.{v} α) :=
  (equivShrink α).symm.nonUnitalSemiring

Non-Unital Semiring Structure on Shrink of a Small Non-Unital Semiring

Informal description

For any $v$-small type $\alpha$ equipped with a non-unital semiring structure, the model `Shrink.{v} α` in a smaller universe also inherits a non-unital semiring structure. The operations on `Shrink α` are defined by transporting the operations from $\alpha$ via the equivalence between $\alpha$ and `Shrink α$.

Equiv.addMonoidWithOne abbrev

[AddMonoidWithOne β] : AddMonoidWithOne α

Full source

/-- Transfer `AddMonoidWithOne` across an `Equiv` -/
protected abbrev addMonoidWithOne [AddMonoidWithOne β] : AddMonoidWithOne α :=
  { e.addMonoid, e.one with
    natCast := fun n => e.symm n
    natCast_zero := e.injective (by simp [zero_def])
    natCast_succ := fun n => e.injective (by simp [add_def, one_def]) }

Transfer of Additive Monoid with One Structure via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and an additive monoid with one structure on $\beta$, there exists an additive monoid with one structure on $\alpha$ induced by $e$. The operations on $\alpha$ are defined by: - Addition: $x + y = e^{-1}(e(x) + e(y))$ - Zero: $0 = e^{-1}(0)$ - One: $1 = e^{-1}(1)$ - Natural number cast: $\text{NatCast}(n) = e^{-1}(\text{NatCast}(n))$ for $n \in \mathbb{N}$

Equiv.instAddMonoidWithOneShrink instance

[Small.{v} α] [AddMonoidWithOne α] : AddMonoidWithOne (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [AddMonoidWithOne α] : AddMonoidWithOne (Shrink.{v} α) :=
  (equivShrink α).symm.addMonoidWithOne

Additive Monoid with One Structure on Shrink of a Small Type

Informal description

For any $v$-small type $\alpha$ equipped with an additive monoid with one structure, the model `Shrink.{v} α` in a smaller universe also inherits an additive monoid with one structure. The operations on `Shrink α` are defined by transporting the operations from $\alpha$ via the equivalence between $\alpha$ and `Shrink α$.

Equiv.addGroupWithOne abbrev

[AddGroupWithOne β] : AddGroupWithOne α

Full source

/-- Transfer `AddGroupWithOne` across an `Equiv` -/
protected abbrev addGroupWithOne [AddGroupWithOne β] : AddGroupWithOne α :=
  { e.addMonoidWithOne,
    e.addGroup with
    intCast := fun n => e.symm n
    intCast_ofNat := fun n => by simp only [Int.cast_natCast]; rfl
    intCast_negSucc := fun _ =>
      congr_arg e.symm <| (Int.cast_negSucc _).trans <| congr_arg _ (e.apply_symm_apply _).symm }

Transfer of Additive Group with One Structure via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and an additive group with one structure on $\beta$, there exists an additive group with one structure on $\alpha$ induced by $e$. The operations on $\alpha$ are defined by: - Addition: $x + y = e^{-1}(e(x) + e(y))$ - Zero: $0 = e^{-1}(0)$ - One: $1 = e^{-1}(1)$ - Negation: $-x = e^{-1}(-e(x))$ - Integer cast: $\text{IntCast}(n) = e^{-1}(\text{IntCast}(n))$ for $n \in \mathbb{Z}$

Equiv.instAddGroupWithOneShrink instance

[Small.{v} α] [AddGroupWithOne α] : AddGroupWithOne (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [AddGroupWithOne α] : AddGroupWithOne (Shrink.{v} α) :=
  (equivShrink α).symm.addGroupWithOne

Additive Group with One Structure on Shrink of a Small Type

Informal description

For any $v$-small type $\alpha$ equipped with an additive group with one structure, the model `Shrink.{v} α` in a smaller universe also inherits an additive group with one structure. The operations on `Shrink α` are defined by transporting the operations from $\alpha$ via the equivalence between $\alpha$ and `Shrink α$.

Equiv.nonAssocSemiring abbrev

[NonAssocSemiring β] : NonAssocSemiring α

Full source

/-- Transfer `NonAssocSemiring` across an `Equiv` -/
protected abbrev nonAssocSemiring [NonAssocSemiring β] : NonAssocSemiring α := by
  let mul := e.mul
  let add_monoid_with_one := e.addMonoidWithOne
  apply e.injective.nonAssocSemiring _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Non-Associative Semiring Structure via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a non-associative semiring structure on $\beta$, there exists a non-associative semiring structure on $\alpha$ induced by $e$. The operations on $\alpha$ are defined by: - Addition: $x + y = e^{-1}(e(x) + e(y))$ - Multiplication: $x * y = e^{-1}(e(x) * e(y))$ - Zero: $0 = e^{-1}(0)$ - One: $1 = e^{-1}(1)$ - Natural number scalar multiplication: $n \cdot x = e^{-1}(n \cdot e(x))$ for $n \in \mathbb{N}$

Equiv.instNonAssocSemiringShrink instance

[Small.{v} α] [NonAssocSemiring α] : NonAssocSemiring (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [NonAssocSemiring α] : NonAssocSemiring (Shrink.{v} α) :=
  (equivShrink α).symm.nonAssocSemiring

Non-Associative Semiring Structure on Shrink Models

Informal description

For any $v$-small type $\alpha$ with a non-associative semiring structure, the model $\mathrm{Shrink}_v(\alpha)$ in a smaller universe inherits a non-associative semiring structure via the equivalence $\alpha \simeq \mathrm{Shrink}_v(\alpha)$. The operations on $\mathrm{Shrink}_v(\alpha)$ are defined by transporting the operations from $\alpha$ through this equivalence.

Equiv.semiring abbrev

[Semiring β] : Semiring α

Full source

/-- Transfer `Semiring` across an `Equiv` -/
protected abbrev semiring [Semiring β] : Semiring α := by
  let mul := e.mul
  let add_monoid_with_one := e.addMonoidWithOne
  let npow := e.pow ℕ
  apply e.injective.semiring _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Semiring Structure via Equivalence

Informal description

Given an equivalence (bijection with inverse) $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a semiring structure on $\beta$, there exists a semiring structure on $\alpha$ induced by $e$. The operations are defined as: - Addition: $x + y = e^{-1}(e(x) + e(y))$ - Multiplication: $x \cdot y = e^{-1}(e(x) \cdot e(y))$ - Zero: $0 = e^{-1}(0)$ - One: $1 = e^{-1}(1)$ - Natural number scalar multiplication: $n \cdot x = e^{-1}(n \cdot e(x))$ for $n \in \mathbb{N}$

Equiv.instSemiringShrink instance

[Small.{v} α] [Semiring α] : Semiring (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [Semiring α] : Semiring (Shrink.{v} α) :=
  (equivShrink α).symm.semiring

Semiring Structure on Shrink of a Small Semiring

Informal description

For any $v$-small type $\alpha$ equipped with a semiring structure, the model $\mathrm{Shrink}_v(\alpha)$ in the universe $\mathrm{Type}\,v$ inherits a semiring structure via the equivalence $\alpha \simeq \mathrm{Shrink}_v(\alpha)$. The operations are defined by transporting the operations from $\alpha$ through this equivalence.

Equiv.nonUnitalCommSemiring abbrev

[NonUnitalCommSemiring β] : NonUnitalCommSemiring α

Full source

/-- Transfer `NonUnitalCommSemiring` across an `Equiv` -/
protected abbrev nonUnitalCommSemiring [NonUnitalCommSemiring β] : NonUnitalCommSemiring α := by
  let zero := e.zero
  let add := e.add
  let mul := e.mul
  let nsmul := e.smul ℕ
  apply e.injective.nonUnitalCommSemiring _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Non-Unital Commutative Semiring Structure via Equivalence

Informal description

Given an equivalence (bijection with inverse) $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a non-unital commutative semiring structure on $\beta$, there exists a non-unital commutative semiring structure on $\alpha$ induced by $e$. The operations are defined as: - Addition: $x + y = e^{-1}(e(x) + e(y))$ - Multiplication: $x * y = e^{-1}(e(x) * e(y))$ - Scalar multiplication: $r \cdot x = e^{-1}(r \cdot e(x))$ (for any scalar $r$ in the appropriate type)

Equiv.instNonUnitalCommSemiringShrink instance

[Small.{v} α] [NonUnitalCommSemiring α] : NonUnitalCommSemiring (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [NonUnitalCommSemiring α] :
    NonUnitalCommSemiring (Shrink.{v} α) :=
  (equivShrink α).symm.nonUnitalCommSemiring

Non-Unital Commutative Semiring Structure on Shrink of a Small Type

Informal description

For any $v$-small type $\alpha$ with a non-unital commutative semiring structure, the model $\mathrm{Shrink}_v(\alpha)$ in the universe $\mathrm{Type}\,v$ inherits a non-unital commutative semiring structure via the equivalence $\alpha \simeq \mathrm{Shrink}_v(\alpha)$. The operations are defined by transporting the operations from $\alpha$ through this equivalence.

Equiv.commSemiring abbrev

[CommSemiring β] : CommSemiring α

Full source

/-- Transfer `CommSemiring` across an `Equiv` -/
protected abbrev commSemiring [CommSemiring β] : CommSemiring α := by
  let mul := e.mul
  let add_monoid_with_one := e.addMonoidWithOne
  let npow := e.pow ℕ
  apply e.injective.commSemiring _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Commutative Semiring Structure via Equivalence

Informal description

Given an equivalence (bijection with inverse) $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a commutative semiring structure on $\beta$, there exists a commutative semiring structure on $\alpha$ induced by $e$. The operations are defined as: - Addition: $x + y = e^{-1}(e(x) + e(y))$ - Multiplication: $x \cdot y = e^{-1}(e(x) \cdot e(y))$ - Zero: $0 = e^{-1}(0)$ - One: $1 = e^{-1}(1)$ - Natural number scalar multiplication: $n \cdot x = e^{-1}(n \cdot e(x))$ for $n \in \mathbb{N}$

Equiv.instCommSemiringShrink instance

[Small.{v} α] [CommSemiring α] : CommSemiring (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [CommSemiring α] : CommSemiring (Shrink.{v} α) :=
  (equivShrink α).symm.commSemiring

Commutative Semiring Structure on Shrink of a Small Commutative Semiring

Informal description

For any $v$-small type $\alpha$ with a commutative semiring structure, the model $\mathrm{Shrink}_v(\alpha)$ in the universe $\mathrm{Type}\,v$ inherits a commutative semiring structure via the equivalence $\alpha \simeq \mathrm{Shrink}_v(\alpha)$. The operations are defined by transporting the operations from $\alpha$ through this equivalence: - Addition: $x + y = e^{-1}(e(x) + e(y))$ - Multiplication: $x \cdot y = e^{-1}(e(x) \cdot e(y))$ - Zero: $0 = e^{-1}(0)$ - One: $1 = e^{-1}(1)$ - Natural number scalar multiplication: $n \cdot x = e^{-1}(n \cdot e(x))$ for $n \in \mathbb{N}$

Equiv.nonUnitalNonAssocRing abbrev

[NonUnitalNonAssocRing β] : NonUnitalNonAssocRing α

Full source

/-- Transfer `NonUnitalNonAssocRing` across an `Equiv` -/
protected abbrev nonUnitalNonAssocRing [NonUnitalNonAssocRing β] : NonUnitalNonAssocRing α := by
  let zero := e.zero
  let add := e.add
  let mul := e.mul
  let neg := e.Neg
  let sub := e.sub
  let nsmul := e.smul ℕ
  let zsmul := e.smul ℤ
  apply e.injective.nonUnitalNonAssocRing _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Non-Unital Non-Associative Ring Structure via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a non-unital non-associative ring structure on $\beta$, there exists a non-unital non-associative ring structure on $\alpha$ induced by $e$. The operations on $\alpha$ are defined by: - Addition: $x + y = e^{-1}(e(x) + e(y))$ - Multiplication: $x * y = e^{-1}(e(x) * e(y))$ - Negation: $-x = e^{-1}(-e(x))$ - Zero: $0 = e^{-1}(0)$

Equiv.instNonUnitalNonAssocRingShrink instance

[Small.{v} α] [NonUnitalNonAssocRing α] : NonUnitalNonAssocRing (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [NonUnitalNonAssocRing α] :
    NonUnitalNonAssocRing (Shrink.{v} α) :=
  (equivShrink α).symm.nonUnitalNonAssocRing

Transfer of Non-Unital Non-Associative Ring Structure to Shrink Model

Informal description

For any $v$-small type $\alpha$ equipped with a non-unital non-associative ring structure, the model `Shrink.{v} α` in a smaller universe inherits a non-unital non-associative ring structure via the equivalence between $\alpha$ and its shrink. The operations on `Shrink.{v} α` are defined by transporting the operations from $\alpha$ through the equivalence: - Addition: $x + y = e^{-1}(e(x) + e(y))$ - Multiplication: $x * y = e^{-1}(e(x) * e(y))$ - Negation: $-x = e^{-1}(-e(x))$ - Zero: $0 = e^{-1}(0)$

Equiv.nonUnitalRing abbrev

[NonUnitalRing β] : NonUnitalRing α

Full source

/-- Transfer `NonUnitalRing` across an `Equiv` -/
protected abbrev nonUnitalRing [NonUnitalRing β] : NonUnitalRing α := by
  let zero := e.zero
  let add := e.add
  let mul := e.mul
  let neg := e.Neg
  let sub := e.sub
  let nsmul := e.smul ℕ
  let zsmul := e.smul ℤ
  apply e.injective.nonUnitalRing _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Non-Unital Ring Structure via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, if $\beta$ has a non-unital ring structure, then $\alpha$ can be equipped with a non-unital ring structure via $e$. Specifically, the operations on $\alpha$ are defined by transporting the operations from $\beta$ through $e$: - Addition: $x + y = e^{-1}(e(x) + e(y))$ - Multiplication: $x * y = e^{-1}(e(x) * e(y))$ - Negation: $-x = e^{-1}(-e(x))$ - Zero: $0 = e^{-1}(0)$

Equiv.instNonUnitalRingShrink instance

[Small.{v} α] [NonUnitalRing α] : NonUnitalRing (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [NonUnitalRing α] : NonUnitalRing (Shrink.{v} α) :=
  (equivShrink α).symm.nonUnitalRing

Non-Unital Ring Structure on Shrink of a Non-Unital Ring

Informal description

For any $v$-small type $\alpha$ equipped with a non-unital ring structure, the model $\mathrm{Shrink}_v(\alpha)$ in a smaller universe can be equipped with a non-unital ring structure by transporting the operations from $\alpha$ via the equivalence $\alpha \simeq \mathrm{Shrink}_v(\alpha)$.

Equiv.nonAssocRing abbrev

[NonAssocRing β] : NonAssocRing α

Full source

/-- Transfer `NonAssocRing` across an `Equiv` -/
protected abbrev nonAssocRing [NonAssocRing β] : NonAssocRing α := by
  let add_group_with_one := e.addGroupWithOne
  let mul := e.mul
  apply e.injective.nonAssocRing _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Non-Associative Ring Structure via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a non-associative ring structure on $\beta$, there exists a non-associative ring structure on $\alpha$ induced by $e$. The operations on $\alpha$ are defined by: - Addition: $x + y = e^{-1}(e(x) + e(y))$ - Multiplication: $x * y = e^{-1}(e(x) * e(y))$ - Zero: $0 = e^{-1}(0)$ - One: $1 = e^{-1}(1)$ - Negation: $-x = e^{-1}(-e(x))$ - Integer cast: $\text{IntCast}(n) = e^{-1}(\text{IntCast}(n))$ for $n \in \mathbb{Z}$

Equiv.instNonAssocRingShrink instance

[Small.{v} α] [NonAssocRing α] : NonAssocRing (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [NonAssocRing α] : NonAssocRing (Shrink.{v} α) :=
  (equivShrink α).symm.nonAssocRing

Non-Associative Ring Structure on Shrink of a Non-Associative Ring

Informal description

For any $v$-small type $\alpha$ equipped with a non-associative ring structure, the model $\mathrm{Shrink}_v(\alpha)$ in a smaller universe can be equipped with a non-associative ring structure by transporting the operations from $\alpha$ via the equivalence $\alpha \simeq \mathrm{Shrink}_v(\alpha)$. Specifically: - Addition: $x + y = e^{-1}(e(x) + e(y))$ - Multiplication: $x * y = e^{-1}(e(x) * e(y))$ - Zero: $0 = e^{-1}(0)$ - One: $1 = e^{-1}(1)$ - Negation: $-x = e^{-1}(-e(x))$ - Integer cast: $\text{IntCast}(n) = e^{-1}(\text{IntCast}(n))$ for $n \in \mathbb{Z}$

Equiv.ring abbrev

[Ring β] : Ring α

Full source

/-- Transfer `Ring` across an `Equiv` -/
protected abbrev ring [Ring β] : Ring α := by
  let mul := e.mul
  let add_group_with_one := e.addGroupWithOne
  let npow := e.pow ℕ
  apply e.injective.ring _ <;> intros <;> exact e.apply_symm_apply _

Ring Structure Transfer via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a ring structure on $\beta$, there exists an induced ring structure on $\alpha$ where: - Addition is defined by $x + y = e^{-1}(e(x) + e(y))$ - Multiplication is defined by $x * y = e^{-1}(e(x) * e(y))$ - Zero is $0 = e^{-1}(0)$ - One is $1 = e^{-1}(1)$ - Negation is $-x = e^{-1}(-e(x))$

Equiv.instRingShrink instance

[Small.{v} α] [Ring α] : Ring (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [Ring α] : Ring (Shrink.{v} α) :=
  (equivShrink α).symm.ring

Ring Structure on Shrink Model via Equivalence

Informal description

For any $v$-small type $\alpha$ with a ring structure, the model $\mathrm{Shrink}(\alpha)$ in the universe $\mathrm{Type}\,v$ inherits a ring structure via the equivalence between $\alpha$ and $\mathrm{Shrink}(\alpha)$. The operations are defined by transporting the ring structure from $\alpha$ to $\mathrm{Shrink}(\alpha)$ through this equivalence.

Equiv.nonUnitalCommRing abbrev

[NonUnitalCommRing β] : NonUnitalCommRing α

Full source

/-- Transfer `NonUnitalCommRing` across an `Equiv` -/
protected abbrev nonUnitalCommRing [NonUnitalCommRing β] : NonUnitalCommRing α := by
  let zero := e.zero
  let add := e.add
  let mul := e.mul
  let neg := e.Neg
  let sub := e.sub
  let nsmul := e.smul ℕ
  let zsmul := e.smul ℤ
  apply e.injective.nonUnitalCommRing _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Non-Unital Commutative Ring Structure via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ and a non-unital commutative ring structure on $\beta$, there exists an induced non-unital commutative ring structure on $\alpha$ where the operations are defined via transport through $e$.

Equiv.instNonUnitalCommRingShrink instance

[Small.{v} α] [NonUnitalCommRing α] : NonUnitalCommRing (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [NonUnitalCommRing α] : NonUnitalCommRing (Shrink.{v} α) :=
  (equivShrink α).symm.nonUnitalCommRing

Non-Unital Commutative Ring Structure on Shrink Model

Informal description

For any $v$-small type $\alpha$ with a non-unital commutative ring structure, the model $\mathrm{Shrink}(\alpha)$ in the universe $\mathrm{Type}\,v$ inherits a non-unital commutative ring structure via the equivalence between $\alpha$ and $\mathrm{Shrink}(\alpha)$.

Equiv.commRing abbrev

[CommRing β] : CommRing α

Full source

/-- Transfer `CommRing` across an `Equiv` -/
protected abbrev commRing [CommRing β] : CommRing α := by
  let mul := e.mul
  let add_group_with_one := e.addGroupWithOne
  let npow := e.pow ℕ
  apply e.injective.commRing _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Commutative Ring Structure via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a commutative ring structure on $\beta$, there exists an induced commutative ring structure on $\alpha$ where the operations are defined via transport through $e$. Specifically: - Addition: $x + y = e^{-1}(e(x) + e(y))$ - Multiplication: $x \cdot y = e^{-1}(e(x) \cdot e(y))$ - Zero: $0 = e^{-1}(0)$ - One: $1 = e^{-1}(1)$ - Negation: $-x = e^{-1}(-e(x))$

Equiv.instCommRingShrink instance

[Small.{v} α] [CommRing α] : CommRing (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [CommRing α] : CommRing (Shrink.{v} α) :=
  (equivShrink α).symm.commRing

Transfer of Commutative Ring Structure to Shrink Model

Informal description

For any $v$-small type $\alpha$ with a commutative ring structure, the model $\mathrm{Shrink}(\alpha)$ in the universe $\mathrm{Type}\,v$ inherits a commutative ring structure via the equivalence between $\alpha$ and $\mathrm{Shrink}(\alpha)$. Specifically, the operations are defined by transporting the commutative ring structure from $\alpha$ to $\mathrm{Shrink}(\alpha)$ through the equivalence.

Equiv.instNontrivialShrink instance

[Small.{v} α] [Nontrivial α] : Nontrivial (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [Nontrivial α] : Nontrivial (Shrink.{v} α) :=
  (equivShrink α).symm.nontrivial

Nontriviality Preservation under Shrinking

Informal description

For any $v$-small type $\alpha$ that is nontrivial, its model $\text{Shrink}_{v}(\alpha)$ in a smaller universe is also nontrivial.

Equiv.isDomain theorem

[Semiring α] [Semiring β] [IsDomain β] (e : α ≃+* β) : IsDomain α

Full source

/-- Transfer `IsDomain` across an `Equiv` -/
protected theorem isDomain [Semiring α] [Semiring β] [IsDomain β] (e : α ≃+* β) : IsDomain α :=
  Function.Injective.isDomain e.toRingHom e.injective

Transfer of Domain Property via Ring Equivalence

Informal description

Let $\alpha$ and $\beta$ be semirings, and suppose $\beta$ is a domain (i.e., has no zero divisors and is nontrivial). Given a ring equivalence $e: \alpha \simeq \beta$ (a bijective ring homomorphism in both directions), then $\alpha$ is also a domain.

Equiv.instIsDomainShrink instance

[Small.{v} α] [Semiring α] [IsDomain α] : IsDomain (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [Semiring α] [IsDomain α] : IsDomain (Shrink.{v} α) :=
  Equiv.isDomain (Shrink.ringEquiv α)

Domain Property Preservation under Shrinking

Informal description

For any $v$-small type $\alpha$ equipped with a semiring structure that is a domain, the model $\mathrm{Shrink}_v(\alpha)$ in the universe $\mathrm{Type}\,v$ is also a domain. This means that the domain property (no zero divisors and nontriviality) is preserved when transferring the structure via the equivalence $\alpha \simeq \mathrm{Shrink}_v(\alpha)$.

Equiv.nnratCast abbrev

[NNRatCast β] : NNRatCast α

Full source

/-- Transfer `NNRatCast` across an `Equiv` -/
protected abbrev nnratCast [NNRatCast β] : NNRatCast α where nnratCast q := e.symm q

Transfer of Nonnegative Rational Casting via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a canonical homomorphism from nonnegative rationals to $\beta$ (i.e., $\beta$ has a `NNRatCast` instance), this defines a canonical homomorphism from nonnegative rationals to $\alpha$ by transferring the structure via $e$.

Equiv.ratCast abbrev

[RatCast β] : RatCast α

Full source

/-- Transfer `RatCast` across an `Equiv` -/
protected abbrev ratCast [RatCast β] : RatCast α where ratCast n := e.symm n

Transfer of Rational Casting Operation via Equivalence

Informal description

Given a type $\beta$ with a rational casting operation (denoted by `[RatCast β]`), and an equivalence $\alpha \simeq \beta$, this defines a rational casting operation on $\alpha$ by transferring the structure from $\beta$ via the equivalence.

Shrink.instNNRatCast instance

[Small.{v} α] [NNRatCast α] : NNRatCast (Shrink.{v} α)

Full source

noncomputable instance _root_.Shrink.instNNRatCast [Small.{v} α] [NNRatCast α] :
    NNRatCast (Shrink.{v} α) := (equivShrink α).symm.nnratCast

Transfer of Nonnegative Rational Casting to Shrink Type

Informal description

For any $v$-small type $\alpha$ equipped with a canonical homomorphism from nonnegative rationals (i.e., $\alpha$ has a `NNRatCast` instance), the model `Shrink α` in the universe `Type v` also inherits a canonical homomorphism from nonnegative rationals.

Shrink.instRatCast instance

[Small.{v} α] [RatCast α] : RatCast (Shrink.{v} α)

Full source

noncomputable instance _root_.Shrink.instRatCast [Small.{v} α] [RatCast α] :
    RatCast (Shrink.{v} α) := (equivShrink α).symm.ratCast

Rational Casting Operation on Shrink Model

Informal description

For any $v$-small type $\alpha$ equipped with a rational casting operation, the model $\operatorname{Shrink} \alpha$ in the universe $\operatorname{Type} v$ also inherits a rational casting operation via the equivalence between $\alpha$ and $\operatorname{Shrink} \alpha$.

Equiv.divisionRing abbrev

[DivisionRing β] : DivisionRing α

Full source

/-- Transfer `DivisionRing` across an `Equiv` -/
protected abbrev divisionRing [DivisionRing β] : DivisionRing α := by
  let add_group_with_one := e.addGroupWithOne
  let inv := e.Inv
  let div := e.div
  let mul := e.mul
  let npow := e.pow ℕ
  let zpow := e.pow ℤ
  let nnratCast := e.nnratCast
  let ratCast := e.ratCast
  let nnqsmul := e.smul ℚ≥0
  let qsmul := e.smul ℚ
  apply e.injective.divisionRing _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Division Ring Structure via Equivalence

Informal description

Given an equivalence (bijection) $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a division ring structure on $\beta$, there exists a division ring structure on $\alpha$ induced by $e$. The operations on $\alpha$ are defined by: - Addition: $x + y = e^{-1}(e(x) + e(y))$ - Multiplication: $x \cdot y = e^{-1}(e(x) \cdot e(y))$ - Zero: $0 = e^{-1}(0)$ - One: $1 = e^{-1}(1)$ - Negation: $-x = e^{-1}(-e(x))$ - Division: $x / y = e^{-1}(e(x) / e(y))$ for $y \neq 0$ - Rational casting: $\text{ratCast}(q) = e^{-1}(\text{ratCast}(q))$ for $q \in \mathbb{Q}$

Equiv.instDivisionRingShrink instance

[Small.{v} α] [DivisionRing α] : DivisionRing (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [DivisionRing α] : DivisionRing (Shrink.{v} α) :=
  (equivShrink α).symm.divisionRing

Division Ring Structure on Shrink Model

Informal description

For any $v$-small type $\alpha$ equipped with a division ring structure, the model $\operatorname{Shrink} \alpha$ in the universe $\operatorname{Type} v$ also inherits a division ring structure via the equivalence between $\alpha$ and $\operatorname{Shrink} \alpha$.

Equiv.field abbrev

[Field β] : Field α

Full source

/-- Transfer `Field` across an `Equiv` -/
protected abbrev field [Field β] : Field α := by
  let add_group_with_one := e.addGroupWithOne
  let neg := e.Neg
  let inv := e.Inv
  let div := e.div
  let mul := e.mul
  let npow := e.pow ℕ
  let zpow := e.pow ℤ
  let nnratCast := e.nnratCast
  let ratCast := e.ratCast
  let nnqsmul := e.smul ℚ≥0
  let qsmul := e.smul ℚ
  apply e.injective.field _ <;> intros <;> exact e.apply_symm_apply _

Transfer of Field Structure via Equivalence

Informal description

Given an equivalence (bijection) $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a field structure on $\beta$, there exists a field structure on $\alpha$ induced by $e$. The operations on $\alpha$ are defined by: - Addition: $x + y = e^{-1}(e(x) + e(y))$ - Multiplication: $x \cdot y = e^{-1}(e(x) \cdot e(y))$ - Zero: $0 = e^{-1}(0)$ - One: $1 = e^{-1}(1)$ - Negation: $-x = e^{-1}(-e(x))$ - Division: $x / y = e^{-1}(e(x) / e(y))$ for $y \neq 0$ - Rational casting: $\text{ratCast}(q) = e^{-1}(\text{ratCast}(q))$ for $q \in \mathbb{Q}$

Equiv.instFieldShrink instance

[Small.{v} α] [Field α] : Field (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [Field α] : Field (Shrink.{v} α) :=
  (equivShrink α).symm.field

Field Structure on Shrink Model of a Small Type

Informal description

For any $v$-small type $\alpha$ equipped with a field structure, the model $\mathrm{Shrink}_{v}(\alpha)$ in the universe $\mathrm{Type}\, v$ inherits a field structure. The operations on $\mathrm{Shrink}_{v}(\alpha)$ are defined via the equivalence $e : \alpha \simeq \mathrm{Shrink}_{v}(\alpha)$ by: - Addition: $x + y = e(e^{-1}(x) + e^{-1}(y))$ - Multiplication: $x \cdot y = e(e^{-1}(x) \cdot e^{-1}(y))$ - Zero: $0 = e(0)$ - One: $1 = e(1)$ - Negation: $-x = e(-e^{-1}(x))$ - Division: $x / y = e(e^{-1}(x) / e^{-1}(y))$ for $y \neq 0$ - Rational casting: $\text{ratCast}(q) = e(\text{ratCast}(q))$ for $q \in \mathbb{Q}$

Equiv.mulAction abbrev

(e : α ≃ β) [MulAction R β] : MulAction R α

Full source

/-- Transfer `MulAction` across an `Equiv` -/
protected abbrev mulAction (e : α ≃ β) [MulAction R β] : MulAction R α :=
  { e.smul R with
    one_smul := by simp [smul_def]
    mul_smul := by simp [smul_def, mul_smul] }

Induced Multiplicative Action via Bijection

Informal description

Given a bijection $e : \alpha \simeq \beta$ and a multiplicative action of a monoid $R$ on $\beta$, there exists an induced multiplicative action of $R$ on $\alpha$ defined by $r \cdot x = e^{-1}(r \cdot e(x))$ for all $r \in R$ and $x \in \alpha$.

Equiv.instMulActionShrink instance

[Small.{v} α] [MulAction R α] : MulAction R (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [MulAction R α] : MulAction R (Shrink.{v} α) :=
  (equivShrink α).symm.mulAction R

Multiplicative Action on Shrink Model of a Small Type

Informal description

For any type $\alpha$ that is $v$-small and equipped with a multiplicative action of a monoid $R$, the model $\mathrm{Shrink}_{v}(\alpha)$ in the universe $\mathrm{Type}\, v$ inherits a multiplicative action of $R$.

Equiv.distribMulAction abbrev

 (e : α ≃ β) [AddCommMonoid β] :
  letI := Equiv.addCommMonoid e
  ∀ [DistribMulAction R β], DistribMulAction R α

Full source

/-- Transfer `DistribMulAction` across an `Equiv` -/
protected abbrev distribMulAction (e : α ≃ β) [AddCommMonoid β] :
    letI := Equiv.addCommMonoid e
    ∀ [DistribMulAction R β], DistribMulAction R α := by
  intros
  letI := Equiv.addCommMonoid e
  exact
    ({ Equiv.mulAction R e with
        smul_zero := by simp [zero_def, smul_def]
        smul_add := by simp [add_def, smul_def, smul_add] } :
      DistribMulAction R α)

Induced Distributive Multiplicative Action via Bijection

Informal description

Given a bijection $e : \alpha \simeq \beta$ and an additive commutative monoid structure on $\beta$, there exists an induced distributive multiplicative action of a monoid $R$ on $\alpha$ whenever $\beta$ is equipped with such an action. Specifically, for any $r \in R$ and $x \in \alpha$, the action is defined by $r \cdot x = e^{-1}(r \cdot e(x))$.

Equiv.instDistribMulActionShrink instance

[Small.{v} α] [AddCommMonoid α] [DistribMulAction R α] : DistribMulAction R (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [AddCommMonoid α] [DistribMulAction R α] :
    DistribMulAction R (Shrink.{v} α) :=
  (equivShrink α).symm.distribMulAction R

Distributive Multiplicative Action on Shrink Model of a Small Type

Informal description

For any $v$-small type $\alpha$ equipped with an additive commutative monoid structure and a distributive multiplicative action of a monoid $R$, the model $\mathrm{Shrink}_{v}(\alpha)$ in the universe $\mathrm{Type}\, v$ inherits a distributive multiplicative action of $R$.

Equiv.module abbrev

 (e : α ≃ β) [AddCommMonoid β] :
  let _ := Equiv.addCommMonoid e
  ∀ [Module R β], Module R α

Full source

/-- Transfer `Module` across an `Equiv` -/
protected abbrev module (e : α ≃ β) [AddCommMonoid β] :
    let _ := Equiv.addCommMonoid e
    ∀ [Module R β], Module R α := by
  intros
  exact
    ({ Equiv.distribMulAction R e with
        zero_smul := by simp [smul_def, zero_smul, zero_def]
        add_smul := by simp [add_def, smul_def, add_smul] } :
      Module R α)

Induced Module Structure via Bijection

Informal description

Given a bijection $e : \alpha \simeq \beta$ and an additive commutative monoid structure on $\beta$, there exists an induced module structure of a ring $R$ on $\alpha$ whenever $\beta$ is equipped with such a module structure. Specifically, for any $r \in R$ and $x \in \alpha$, the scalar multiplication is defined by $r \cdot x = e^{-1}(r \cdot e(x))$.

Equiv.instModuleShrink instance

[Small.{v} α] [AddCommMonoid α] [Module R α] : Module R (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [AddCommMonoid α] [Module R α] : Module R (Shrink.{v} α) :=
  (equivShrink α).symm.module R

Module Structure on Shrink Model of a Small Type

Informal description

For any $v$-small type $\alpha$ equipped with an additive commutative monoid structure and a module structure over a ring $R$, the model $\mathrm{Shrink}_{v}(\alpha)$ in the universe $\mathrm{Type}\, v$ inherits a module structure over $R$.

Equiv.linearEquiv definition

 (e : α ≃ β) [AddCommMonoid β] [Module R β] :
  by
  let addCommMonoid := Equiv.addCommMonoid e
  let module := Equiv.module R e
  exact α ≃ₗ[R] β

Full source

/-- An equivalence `e : α ≃ β` gives a linear equivalence `α ≃ₗ[R] β`
where the `R`-module structure on `α` is
the one obtained by transporting an `R`-module structure on `β` back along `e`.
-/
def linearEquiv (e : α ≃ β) [AddCommMonoid β] [Module R β] : by
    let addCommMonoid := Equiv.addCommMonoid e
    let module := Equiv.module R e
    exact α ≃ₗ[R] β := by
  intros
  exact
    { Equiv.addEquiv e with
      map_smul' := fun r x => by
        apply e.symm.injective
        simp only [toFun_as_coe, RingHom.id_apply, EmbeddingLike.apply_eq_iff_eq]
        exact Iff.mpr (apply_eq_iff_eq_symm_apply _) rfl }

Linear equivalence induced by a bijection

Informal description

Given a bijection $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, where $\beta$ is equipped with an additive commutative monoid structure and a module structure over a ring $R$, there exists an induced linear equivalence $\alpha \simeq_{R} \beta$. This linear equivalence preserves both the additive structure and the scalar multiplication, meaning that for any $r \in R$ and $x \in \alpha$, we have $e(r \cdot x) = r \cdot e(x)$.

Shrink.linearEquiv definition

[Small.{v} α] [AddCommMonoid α] [Module R α] : Shrink.{v} α ≃ₗ[R] α

Full source

/-- Shrink `α` to a smaller universe preserves module structure. -/
@[simps!]
noncomputable def _root_.Shrink.linearEquiv [Small.{v} α] [AddCommMonoid α] [Module R α] :
    ShrinkShrink.{v} α ≃ₗ[R] α :=
  Equiv.linearEquiv _ (equivShrink α).symm

Linear equivalence between a small type and its shrink model

Informal description

For any $v$-small type $\alpha$ equipped with an additive commutative monoid structure and a module structure over a ring $R$, there exists a linear equivalence between the model $\mathrm{Shrink}_{v}(\alpha)$ and $\alpha$ itself. This equivalence preserves both the additive structure and the scalar multiplication, meaning that for any $r \in R$ and $x \in \mathrm{Shrink}_{v}(\alpha)$, the equivalence maps $r \cdot x$ to $r \cdot e(x)$, where $e$ is the equivalence map.

Equiv.algebra abbrev

 (e : α ≃ β) [Semiring β] :
  let _ := Equiv.semiring e
  ∀ [Algebra R β], Algebra R α

Full source

/-- Transfer `Algebra` across an `Equiv` -/
protected abbrev algebra (e : α ≃ β) [Semiring β] :
    let _ := Equiv.semiring e
    ∀ [Algebra R β], Algebra R α := by
  intros
  letI : Module R α := e.module R
  fapply Algebra.ofModule
  · intro r x y
    show e.symm (e (e.symm (r • e x)) * e y) = e.symm (r • e.ringEquiv (x * y))
    simp only [apply_symm_apply, Algebra.smul_mul_assoc, map_mul, ringEquiv_apply]
  · intro r x y
    show e.symm (e x * e (e.symm (r • e y))) = e.symm (r • e (e.symm (e x * e y)))
    simp only [apply_symm_apply, Algebra.mul_smul_comm]

Transfer of Algebra Structure via Bijection

Informal description

Given a bijection $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a semiring structure on $\beta$, there exists an induced algebra structure of a commutative ring $R$ on $\alpha$ whenever $\beta$ is equipped with such an algebra structure. Specifically: - The algebra map $\text{algebraMap}_R \alpha$ is defined by $\text{algebraMap}_R \alpha(r) = e^{-1}(\text{algebraMap}_R \beta(r))$ for $r \in R$. - The semiring structure on $\alpha$ is transferred from $\beta$ via $e$ as in `Equiv.semiring`.

Equiv.algebraMap_def theorem

 (e : α ≃ β) [Semiring β] [Algebra R β] (r : R) :
  (@algebraMap R α _ (Equiv.semiring e) (Equiv.algebra R e)) r = e.symm ((algebraMap R β) r)

Full source

lemma algebraMap_def (e : α ≃ β) [Semiring β] [Algebra R β] (r : R) :
    (@algebraMap R α _ (Equiv.semiring e) (Equiv.algebra R e)) r = e.symm ((algebraMap R β) r) := by
  let _ := Equiv.semiring e
  let _ := Equiv.algebra R e
  simp only [Algebra.algebraMap_eq_smul_one]
  show e.symm (r • e 1) = e.symm (r • 1)
  simp only [Equiv.one_def, apply_symm_apply]

Definition of Transferred Algebra Map via Equivalence

Informal description

Given a bijection $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, where $\beta$ is equipped with a semiring structure and an algebra structure over a commutative ring $R$, the algebra map on $\alpha$ induced by $e$ satisfies the following property for any $r \in R$: \[ \text{algebraMap}_R \alpha(r) = e^{-1}(\text{algebraMap}_R \beta(r)). \] Here, the algebra structure on $\alpha$ is transferred from $\beta$ via $e$.

Equiv.instAlgebraShrink instance

[Small.{v} α] [Semiring α] [Algebra R α] : Algebra R (Shrink.{v} α)

Full source

noncomputable instance [Small.{v} α] [Semiring α] [Algebra R α] :
    Algebra R (Shrink.{v} α) :=
  (equivShrink α).symm.algebra _

Algebra Structure on Shrink of a Small Algebra

Informal description

For any $v$-small type $\alpha$ equipped with a semiring structure and an algebra structure over a commutative ring $R$, the model $\mathrm{Shrink}_v(\alpha)$ in the universe $\mathrm{Type}\,v$ inherits an algebra structure over $R$ via the equivalence $\alpha \simeq \mathrm{Shrink}_v(\alpha)$. The algebra operations are defined by transporting the operations from $\alpha$ through this equivalence.

Equiv.algEquiv definition

 (e : α ≃ β) [Semiring β] [Algebra R β] : by
  let semiring := Equiv.semiring e
  let algebra := Equiv.algebra R e
  exact α ≃ₐ[R] β

Full source

/-- An equivalence `e : α ≃ β` gives an algebra equivalence `α ≃ₐ[R] β`
where the `R`-algebra structure on `α` is
the one obtained by transporting an `R`-algebra structure on `β` back along `e`.
-/
def algEquiv (e : α ≃ β) [Semiring β] [Algebra R β] : by
    let semiring := Equiv.semiring e
    let algebra := Equiv.algebra R e
    exact α ≃ₐ[R] β := by
  intros
  exact
    { Equiv.ringEquiv e with
      commutes' := fun r => by
        apply e.symm.injective
        simp only [RingEquiv.toEquiv_eq_coe, toFun_as_coe, EquivLike.coe_coe, ringEquiv_apply,
          symm_apply_apply, algebraMap_def] }

Algebra equivalence via transport of structure

Informal description

Given a bijection $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, where $\beta$ is equipped with a semiring structure and an algebra structure over a commutative ring $R$, there exists an induced algebra equivalence $\alpha \simeq_{R} \beta$. This equivalence preserves both the ring structure and the algebra structure, with operations defined by: - The ring operations on $\alpha$ are transported from $\beta$ via $e$ as in `Equiv.ringEquiv`. - The algebra map $\text{algebraMap}_R \alpha$ is defined by $\text{algebraMap}_R \alpha(r) = e^{-1}(\text{algebraMap}_R \beta(r))$ for $r \in R$.

Equiv.algEquiv_apply theorem

(e : α ≃ β) [Semiring β] [Algebra R β] (a : α) : (algEquiv R e) a = e a

Full source

@[simp]
theorem algEquiv_apply (e : α ≃ β) [Semiring β] [Algebra R β] (a : α) : (algEquiv R e) a = e a :=
  rfl

Application of Algebra Equivalence via Bijection: $(\text{algEquiv}_R e)(a) = e(a)$

Informal description

Given a bijection $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, where $\beta$ is equipped with a semiring structure and an algebra structure over a commutative ring $R$, the algebra equivalence $\text{algEquiv}_R e$ satisfies $(\text{algEquiv}_R e)(a) = e(a)$ for any $a \in \alpha$.

Equiv.algEquiv_symm_apply theorem

 (e : α ≃ β) [Semiring β] [Algebra R β] (b : β) :
  by
  letI := Equiv.semiring e
  letI := Equiv.algebra R e
  exact (algEquiv R e).symm b = e.symm b

Full source

theorem algEquiv_symm_apply (e : α ≃ β) [Semiring β] [Algebra R β] (b : β) : by
    letI := Equiv.semiring e
    letI := Equiv.algebra R e
    exact (algEquiv R e).symm b = e.symm b := rfl

Inverse of Transported Algebra Equivalence via Bijection

Informal description

Given a bijection $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, where $\beta$ is equipped with a semiring structure and an algebra structure over a commutative ring $R$, the inverse of the induced algebra equivalence $(e_{R})^{-1} : \beta \to \alpha$ satisfies $(e_{R})^{-1}(b) = e^{-1}(b)$ for all $b \in \beta$.

Shrink.algEquiv definition

[Small.{v} α] [Semiring α] [Algebra R α] : Shrink.{v} α ≃ₐ[R] α

Full source

/-- Shrink `α` to a smaller universe preserves algebra structure. -/
@[simps!]
noncomputable def _root_.Shrink.algEquiv [Small.{v} α] [Semiring α] [Algebra R α] :
    ShrinkShrink.{v} α ≃ₐ[R] α :=
  Equiv.algEquiv _ (equivShrink α).symm

Algebra equivalence between a small algebra and its shrink model

Informal description

For a $v$-small type $\alpha$ equipped with a semiring structure and an algebra structure over a commutative ring $R$, there exists an algebra equivalence between the model $\mathrm{Shrink}_v(\alpha)$ in the universe $\mathrm{Type}\,v$ and $\alpha$ itself. This equivalence preserves both the ring structure and the algebra structure, with operations defined by transporting the operations from $\alpha$ through the equivalence $\alpha \simeq \mathrm{Shrink}_v(\alpha)$.

Finite.exists_type_univ_nonempty_mulEquiv theorem

(G : Type u) [Group G] [Finite G] : ∃ (G' : Type v) (_ : Group G') (_ : Fintype G'), Nonempty (G ≃* G')

Full source

/-- Any finite group in universe `u` is equivalent to some finite group in universe `v`. -/
lemma exists_type_univ_nonempty_mulEquiv (G : Type u) [Group G] [Finite G] :
    ∃ (G' : Type v) (_ : Group G') (_ : Fintype G'), Nonempty (G ≃* G') := by
  obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin G
  let f : FinFin n ≃ ULift (Fin n) := Equiv.ulift.symm
  let e : G ≃ ULift (Fin n) := e.trans f
  letI groupH : Group (ULift (Fin n)) := e.symm.group
  exact ⟨ULift (Fin n), groupH, inferInstance, ⟨MulEquiv.symm <| e.symm.mulEquiv⟩⟩

Existence of Universe-Independent Finite Group Isomorphism

Informal description

For any finite group $G$ (in any universe level $u$), there exists a finite group $G'$ (in any other universe level $v$) with a multiplicative equivalence (group isomorphism) $G \simeq^* G'$. Moreover, $G'$ can be chosen to have an explicit finite type structure (i.e., it is equipped with a `Fintype` instance).

AddEquiv.module abbrev

(e : α ≃+ β) : Module A α

Full source

/-- Transport a module instance via an isomorphism of the underlying abelian groups.
This has better definitional properties than `Equiv.module` since here
the abelian group structure remains unmodified. -/
abbrev AddEquiv.module (e : α ≃+ β) :
    Module A α where
  toSMul := e.toEquiv.smul A
  one_smul := by simp [Equiv.smul_def]
  mul_smul := by simp [Equiv.smul_def, mul_smul]
  smul_zero := by simp [Equiv.smul_def]
  smul_add := by simp [Equiv.smul_def]
  add_smul := by simp [Equiv.smul_def, add_smul]
  zero_smul := by simp [Equiv.smul_def]

Module Structure Transport via Additive Equivalence

Informal description

Given an additive equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, where $\beta$ has an $A$-module structure, this defines an $A$-module structure on $\alpha$ by transporting the module operations through $e$. Specifically, for $a \in A$ and $x \in \alpha$, the scalar multiplication is defined as $a \cdot x = e^{-1}(a \cdot e(x))$.

LinearEquiv.isScalarTower theorem

 [Module R α] [Module R β] [IsScalarTower R A β] (e : α ≃ₗ[R] β) :
  letI := e.toAddEquiv.module A
  IsScalarTower R A α

Full source

/-- The module instance from `AddEquiv.module` is compatible with the `R`-module structures,
if the `AddEquiv` is induced by an `R`-module isomorphism. -/
lemma LinearEquiv.isScalarTower [Module R α] [Module R β] [IsScalarTower R A β]
    (e : α ≃ₗ[R] β) :
    letI := e.toAddEquiv.module A
    IsScalarTower R A α := by
  letI := e.toAddEquiv.module A
  constructor
  intro x y z
  simp only [Equiv.smul_def, AddEquiv.toEquiv_eq_coe, smul_assoc]
  apply e.symm.map_smul

Scalar Tower Property Preservation under Linear Equivalence

Informal description

Let $R$ and $A$ be scalar types, and let $\alpha$ and $\beta$ be modules over $R$. Suppose $\beta$ has an $A$-module structure such that the scalar multiplications form a tower, i.e., for any $r \in R$, $a \in A$, and $b \in \beta$, we have $(r \cdot a) \cdot b = r \cdot (a \cdot b)$. Given a linear equivalence $e : \alpha \simeq \beta$ of $R$-modules, then the transported $A$-module structure on $\alpha$ (via $e$) also satisfies the scalar tower property with respect to $R$ and $A$.

Mathlib.Algebra.Equiv.TransferInstance

Implementation details

Tags