Mathlib.Algebra.Ring.Equiv

NonUnitalRingHom.inverse definition

 [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (g : S → R) (h₁ : Function.LeftInverse g f)
  (h₂ : Function.RightInverse g f) : S →ₙ+* R

Full source

/-- makes a `NonUnitalRingHom` from the bijective inverse of a `NonUnitalRingHom` -/
@[simps] def NonUnitalRingHom.inverse
    [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S]
    (f : R →ₙ+* S) (g : S → R)
    (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : S →ₙ+* R :=
  { (f : R →+ S).inverse g h₁ h₂, (f : R →ₙ* S).inverse g h₁ h₂ with toFun := g }

Inverse of a non-unital ring homomorphism

Informal description

Given two non-unital non-associative semirings $R$ and $S$, a non-unital ring homomorphism $f : R \to S$, and a function $g : S \to R$ that is both a left and right inverse of $f$, the function $g$ can be equipped with the structure of a non-unital ring homomorphism from $S$ to $R$. This means $g$ preserves both addition and multiplication, i.e., for all $x, y \in S$: - $g(x + y) = g(x) + g(y)$ - $g(x * y) = g(x) * g(y)$ The construction combines the additive and multiplicative inverse homomorphisms while maintaining the original function $g$.

RingHom.inverse definition

 [NonAssocSemiring R] [NonAssocSemiring S] (f : RingHom R S) (g : S → R) (h₁ : Function.LeftInverse g f)
  (h₂ : Function.RightInverse g f) : S →+* R

Full source

/-- makes a `RingHom` from the bijective inverse of a `RingHom` -/
@[simps] def RingHom.inverse [NonAssocSemiring R] [NonAssocSemiring S]
    (f : RingHom R S) (g : S → R)
    (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : S →+* R :=
  { (f : OneHom R S).inverse g h₁,
    (f : MulHom R S).inverse g h₁ h₂,
    (f : R →+ S).inverse g h₁ h₂ with toFun := g }

Inverse of a ring homomorphism

Informal description

Given two non-associative semirings $R$ and $S$, a ring homomorphism $f \colon R \to S$, and a function $g \colon S \to R$ that is both a left and right inverse of $f$ (i.e., $g$ is a two-sided inverse of $f$ as a function), the function $g$ can be equipped with the structure of a ring homomorphism from $S$ to $R$. This means $g$ preserves: - The multiplicative identity: $g(1_S) = 1_R$ - Multiplication: $g(x \cdot y) = g(x) \cdot g(y)$ for all $x, y \in S$ - Addition: $g(x + y) = g(x) + g(y)$ for all $x, y \in S$ - The additive identity: $g(0_S) = 0_R$ The construction combines the inverse properties for the multiplicative and additive structures while maintaining the original function $g$.

RingEquiv structure

(R S : Type*) [Mul R] [Mul S] [Add R] [Add S] extends R ≃ S, R ≃* S, R ≃+ S

Full source

/-- An equivalence between two (non-unital non-associative semi)rings that preserves the
algebraic structure. -/
structure RingEquiv (R S : Type*) [Mul R] [Mul S] [Add R] [Add S] extends R ≃ S, R ≃* S, R ≃+ S

Ring (or Semiring) Equivalence

Informal description

A ring equivalence (or semiring equivalence) between two (non-unital non-associative semi)rings $ R $ and $ S $ is a bijective map that preserves both the multiplicative and additive structures. It extends the notions of bijection (`≃`), multiplicative equivalence (`≃*`), and additive equivalence (`≃+`).

term_≃+*_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Notation for `RingEquiv`. -/
infixl:25 " ≃+* " => RingEquiv

Ring (or Semiring) Equivalence Notation

Informal description

The notation `≃+*` represents a ring (or semiring) equivalence between two rings or semirings, which is a bijective map preserving both multiplicative and additive structures.

RingEquivClass structure

(F R S : Type*) [Mul R] [Add R] [Mul S] [Add S] [EquivLike F R S] : Prop
  extends MulEquivClass F R S

Full source

/-- `RingEquivClass F R S` states that `F` is a type of ring structure preserving equivalences.
You should extend this class when you extend `RingEquiv`. -/
class RingEquivClass (F R S : Type*) [Mul R] [Add R] [Mul S] [Add S] [EquivLike F R S] : Prop
  extends MulEquivClass F R S where
  /-- By definition, a ring isomorphism preserves the additive structure. -/
  map_add : ∀ (f : F) (a b), f (a + b) = f a + f b

Ring Equivalence Class

Informal description

The class `RingEquivClass F R S` asserts that `F` is a type of ring structure preserving equivalences between `R` and `S`. It extends `MulEquivClass` and requires that terms of type `F` can be injectively coerced to bijections that preserve both the multiplicative and additive structures of the rings `R` and `S`. This class is used as a foundation for defining various ring isomorphism and equivalence typeclasses.

RingEquivClass.toAddEquivClass instance

[Mul R] [Add R] [Mul S] [Add S] [h : RingEquivClass F R S] : AddEquivClass F R S

Full source

instance (priority := 100) toAddEquivClass [Mul R] [Add R]
    [Mul S] [Add S] [h : RingEquivClass F R S] : AddEquivClass F R S :=
  { h with }

Ring Equivalences Preserve Additive Structure

Informal description

For any types $R$ and $S$ equipped with multiplication and addition operations, if $F$ is a type of ring structure-preserving equivalences between $R$ and $S$ (i.e., $F$ satisfies `RingEquivClass F R S`), then $F$ is also a type of additive equivalence-preserving morphisms between $R$ and $S$ (i.e., $F$ satisfies `AddEquivClass F R S`). This means that every ring equivalence in $F$ preserves the additive structure of $R$ and $S$.

RingEquivClass.toRingHomClass instance

[NonAssocSemiring R] [NonAssocSemiring S] [h : RingEquivClass F R S] : RingHomClass F R S

Full source

instance (priority := 100) toRingHomClass [NonAssocSemiring R] [NonAssocSemiring S]
    [h : RingEquivClass F R S] : RingHomClass F R S :=
  { h with
    map_zero := map_zero
    map_one := map_one }

Ring Equivalences as Ring Homomorphisms

Informal description

For any non-associative semirings $R$ and $S$, if $F$ is a type of ring structure-preserving equivalences between $R$ and $S$ (i.e., $F$ satisfies `RingEquivClass F R S`), then $F$ is also a type of ring homomorphisms between $R$ and $S$ (i.e., $F$ satisfies `RingHomClass F R S`). This means that every ring equivalence in $F$ preserves both the additive and multiplicative structures of $R$ and $S$.

RingEquivClass.toNonUnitalRingHomClass instance

[NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [h : RingEquivClass F R S] : NonUnitalRingHomClass F R S

Full source

instance (priority := 100) toNonUnitalRingHomClass [NonUnitalNonAssocSemiring R]
    [NonUnitalNonAssocSemiring S] [h : RingEquivClass F R S] : NonUnitalRingHomClass F R S :=
  { h with
    map_zero := map_zero }

Ring Equivalences as Non-Unital Ring Homomorphisms

Informal description

For any non-unital non-associative semirings $R$ and $S$, if $F$ is a type of ring structure-preserving equivalences between $R$ and $S$ (i.e., $F$ satisfies `RingEquivClass F R S`), then $F$ is also a type of non-unital ring homomorphisms between $R$ and $S$ (i.e., $F$ satisfies `NonUnitalRingHomClass F R S`). This means that every ring equivalence in $F$ preserves both the additive and multiplicative structures of $R$ and $S$.

RingEquivClass.toRingEquiv definition

[Mul α] [Add α] [Mul β] [Add β] [EquivLike F α β] [RingEquivClass F α β] (f : F) : α ≃+* β

Full source

/-- Turn an element of a type `F` satisfying `RingEquivClass F α β` into an actual
`RingEquiv`. This is declared as the default coercion from `F` to `α ≃+* β`. -/
@[coe]
def toRingEquiv [Mul α] [Add α] [Mul β] [Add β] [EquivLike F α β] [RingEquivClass F α β] (f : F) :
    α ≃+* β :=
  { (f : α ≃* β), (f : α ≃+ β) with }

Conversion from ring equivalence class to explicit ring equivalence

Informal description

Given types $\alpha$ and $\beta$ equipped with multiplication and addition operations, and a type $F$ satisfying `RingEquivClass F \alpha \beta`, the function converts an element $f : F$ into an explicit ring equivalence $\alpha \simeq+* \beta$. This equivalence consists of: 1. A bijection between $\alpha$ and $\beta$ (as an $\alpha \simeq \beta$), 2. A multiplicative homomorphism preserving the operation (as an $\alpha \simeq^* \beta$), 3. An additive homomorphism preserving the operation (as an $\alpha \simeq^+ \beta$).

instCoeTCRingEquivOfRingEquivClass instance

[Mul α] [Add α] [Mul β] [Add β] [EquivLike F α β] [RingEquivClass F α β] : CoeTC F (α ≃+* β)

Full source

/-- Any type satisfying `RingEquivClass` can be cast into `RingEquiv` via
`RingEquivClass.toRingEquiv`. -/
instance [Mul α] [Add α] [Mul β] [Add β] [EquivLike F α β] [RingEquivClass F α β] :
    CoeTC F (α ≃+* β) :=
  ⟨RingEquivClass.toRingEquiv⟩

Canonical Interpretation of Ring Equivalence Class Elements as Ring Equivalences

Informal description

For any types $\alpha$ and $\beta$ equipped with multiplication and addition operations, and any type $F$ that satisfies `RingEquivClass F \alpha \beta`, there is a canonical way to interpret elements of $F$ as ring equivalences $\alpha \simeq+* \beta$. This interpretation preserves both the multiplicative and additive structures.

RingEquiv.instEquivLike instance

: EquivLike (R ≃+* S) R S

Full source

instance : EquivLike (R ≃+* S) R S where
  coe f := f.toFun
  inv f := f.invFun
  coe_injective' e f h₁ h₂ := by
    cases e
    cases f
    congr
    apply Equiv.coe_fn_injective h₁
  left_inv f := f.left_inv
  right_inv f := f.right_inv

Ring Equivalences as Bijective Structure-Preserving Maps

Informal description

For any two (semi)rings $R$ and $S$, a ring equivalence $R \simeq+* S$ can be treated as a bijective function between $R$ and $S$ that preserves both the multiplicative and additive structures. This instance establishes that ring equivalences satisfy the properties of `EquivLike`, meaning they can be coerced to bijections between $R$ and $S$ in a way that respects the equivalence-like structure.

RingEquiv.instRingEquivClass instance

: RingEquivClass (R ≃+* S) R S

Full source

instance : RingEquivClass (R ≃+* S) R S where
  map_add f := f.map_add'
  map_mul f := f.map_mul'

Ring Equivalence Class Structure on Ring Equivalences

Informal description

For any two (semi)rings $R$ and $S$, the type of ring equivalences $R \simeq+* S$ forms a `RingEquivClass`, meaning it consists of bijective maps that preserve both the multiplicative and additive structures of the rings.

RingEquiv.ext theorem

{f g : R ≃+* S} (h : ∀ x, f x = g x) : f = g

Full source

/-- Two ring isomorphisms agree if they are defined by the
    same underlying function. -/
@[ext]
theorem ext {f g : R ≃+* S} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

Extensionality of Ring Isomorphisms: $f = g$ if they agree pointwise

Informal description

For any two ring isomorphisms $f, g : R \simeq+* S$ between (semi)rings $R$ and $S$, if $f(x) = g(x)$ for all $x \in R$, then $f = g$.

RingEquiv.congr_arg theorem

{f : R ≃+* S} {x x' : R} : x = x' → f x = f x'

Full source

protected theorem congr_arg {f : R ≃+* S} {x x' : R} : x = x' → f x = f x' :=
  DFunLike.congr_arg f

Ring Equivalence Preserves Equality: $x = x' \implies f(x) = f(x')$

Informal description

For any ring equivalence $f : R \simeq+* S$ and elements $x, x' \in R$, if $x = x'$, then $f(x) = f(x')$.

RingEquiv.congr_fun theorem

{f g : R ≃+* S} (h : f = g) (x : R) : f x = g x

Full source

protected theorem congr_fun {f g : R ≃+* S} (h : f = g) (x : R) : f x = g x :=
  DFunLike.congr_fun h x

Pointwise Equality of Ring Equivalences

Informal description

For any two ring equivalences $f, g : R \simeq+* S$ between (semi)rings $R$ and $S$, if $f = g$, then for all $x \in R$, we have $f(x) = g(x)$.

RingEquiv.coe_mk theorem

(e h₃ h₄) : ⇑(⟨e, h₃, h₄⟩ : R ≃+* S) = e

Full source

@[simp]
theorem coe_mk (e h₃ h₄) : ⇑(⟨e, h₃, h₄⟩ : R ≃+* S) = e :=
  rfl

Underlying Function of Ring Equivalence Construction

Informal description

For any ring equivalence $f : R \simeq+* S$ constructed from a bijection $e : R \to S$ and proofs $h_3, h_4$ of the multiplicative and additive structure preservation, the underlying function of $f$ is equal to $e$.

RingEquiv.mk_coe theorem

(e : R ≃+* S) (e' h₁ h₂ h₃ h₄) : (⟨⟨e, e', h₁, h₂⟩, h₃, h₄⟩ : R ≃+* S) = e

Full source

@[simp]
theorem mk_coe (e : R ≃+* S) (e' h₁ h₂ h₃ h₄) : (⟨⟨e, e', h₁, h₂⟩, h₃, h₄⟩ : R ≃+* S) = e :=
  ext fun _ => rfl

Constructed Ring Equivalence Equals Original

Informal description

Given a ring equivalence $e : R \simeq+* S$ between (semi)rings $R$ and $S$, and given a function $e' : S \to R$ along with proofs $h_1$ that $e'$ is a left inverse of $e$, $h_2$ that $e'$ is a right inverse of $e$, $h_3$ that $e$ preserves multiplication, and $h_4$ that $e$ preserves addition, the constructed ring equivalence $\langle \langle e, e', h_1, h_2 \rangle, h_3, h_4 \rangle$ is equal to $e$.

RingEquiv.toEquiv_eq_coe theorem

(f : R ≃+* S) : f.toEquiv = f

Full source

@[simp]
theorem toEquiv_eq_coe (f : R ≃+* S) : f.toEquiv = f :=
  rfl

Ring equivalence coincides with its underlying equivalence

Informal description

For any ring equivalence $f : R \simeq+* S$ between (semi)rings $R$ and $S$, the underlying equivalence (bijection) $f.\text{toEquiv}$ is equal to $f$ itself when viewed as a function.

RingEquiv.coe_toEquiv theorem

(f : R ≃+* S) : ⇑(f : R ≃ S) = f

Full source

@[simp]
theorem coe_toEquiv (f : R ≃+* S) : ⇑(f : R ≃ S) = f :=
  rfl

Ring equivalence coincides with its underlying function

Informal description

For any ring equivalence $f : R \simeq+* S$ between (semi)rings $R$ and $S$, the underlying function of the equivalence $f : R \simeq S$ is equal to $f$ itself when viewed as a function.

RingEquiv.toAddEquiv_eq_coe theorem

(f : R ≃+* S) : f.toAddEquiv = ↑f

Full source

@[simp]
theorem toAddEquiv_eq_coe (f : R ≃+* S) : f.toAddEquiv = ↑f :=
  rfl

Underlying additive equivalence of a ring equivalence equals its coercion

Informal description

For any ring equivalence $f : R \simeq+* S$ between (semi)rings $R$ and $S$, the underlying additive equivalence $f.\text{toAddEquiv}$ is equal to the coercion of $f$ to an additive equivalence.

RingEquiv.toMulEquiv_eq_coe theorem

(f : R ≃+* S) : f.toMulEquiv = ↑f

Full source

@[simp]
theorem toMulEquiv_eq_coe (f : R ≃+* S) : f.toMulEquiv = ↑f :=
  rfl

Ring equivalence to multiplicative equivalence coincides with coercion

Informal description

For any ring equivalence $f : R \simeq+* S$ between (semi)rings $R$ and $S$, the multiplicative equivalence obtained from $f$ is equal to $f$ when viewed as a multiplicative equivalence.

RingEquiv.coe_toMulEquiv theorem

(f : R ≃+* S) : ⇑(f : R ≃* S) = f

Full source

@[simp, norm_cast]
theorem coe_toMulEquiv (f : R ≃+* S) : ⇑(f : R ≃* S) = f :=
  rfl

Underlying Multiplicative Equivalence of Ring Equivalence Preserves Function

Informal description

For any ring equivalence $f \colon R \simeq+* S$ between (semi)rings $R$ and $S$, the underlying multiplicative equivalence $f \colon R \simeq^* S$ has the same underlying function as $f$ itself.

RingEquiv.coe_toAddEquiv theorem

(f : R ≃+* S) : ⇑(f : R ≃+ S) = f

Full source

@[simp]
theorem coe_toAddEquiv (f : R ≃+* S) : ⇑(f : R ≃+ S) = f :=
  rfl

Ring equivalence coincides with its additive part

Informal description

For any ring equivalence $f \colon R \simeq+* S$ between (semi)rings $R$ and $S$, the underlying additive equivalence $f \colon R \simeq+ S$ coincides with $f$ itself when viewed as a function.

RingEquiv.map_mul theorem

(e : R ≃+* S) (x y : R) : e (x * y) = e x * e y

Full source

/-- A ring isomorphism preserves multiplication. -/
protected theorem map_mul (e : R ≃+* S) (x y : R) : e (x * y) = e x * e y :=
  map_mul e x y

Ring Equivalence Preserves Multiplication: $e(x * y) = e(x) * e(y)$

Informal description

For any ring equivalence $e \colon R \simeq+* S$ between (semi)rings $R$ and $S$, and for any elements $x, y \in R$, the equivalence $e$ preserves multiplication, i.e., $e(x * y) = e(x) * e(y)$.

RingEquiv.map_add theorem

(e : R ≃+* S) (x y : R) : e (x + y) = e x + e y

Full source

/-- A ring isomorphism preserves addition. -/
protected theorem map_add (e : R ≃+* S) (x y : R) : e (x + y) = e x + e y :=
  map_add e x y

Ring Equivalence Preserves Addition

Informal description

For any ring equivalence $e \colon R \simeq+* S$ between (semi)rings $R$ and $S$, and for any elements $x, y \in R$, the equivalence preserves addition, i.e., $e(x + y) = e(x) + e(y)$.

RingEquiv.bijective theorem

(e : R ≃+* S) : Function.Bijective e

Full source

protected theorem bijective (e : R ≃+* S) : Function.Bijective e :=
  EquivLike.bijective e

Bijectivity of Ring Equivalences

Informal description

For any ring equivalence $e \colon R \simeq+* S$ between (semi)rings $R$ and $S$, the underlying function $e \colon R \to S$ is bijective.

RingEquiv.injective theorem

(e : R ≃+* S) : Function.Injective e

Full source

protected theorem injective (e : R ≃+* S) : Function.Injective e :=
  EquivLike.injective e

Injectivity of Ring Equivalences

Informal description

For any ring equivalence $e \colon R \simeq+* S$ between (semi)rings $R$ and $S$, the underlying function $e \colon R \to S$ is injective.

RingEquiv.surjective theorem

(e : R ≃+* S) : Function.Surjective e

Full source

protected theorem surjective (e : R ≃+* S) : Function.Surjective e :=
  EquivLike.surjective e

Surjectivity of Ring Equivalences

Informal description

For any ring equivalence $e : R \simeq+* S$ between (semi)rings $R$ and $S$, the underlying function $e : R \to S$ is surjective.

RingEquiv.refl definition

: R ≃+* R

Full source

/-- The identity map is a ring isomorphism. -/
@[refl]
def refl : R ≃+* R :=
  { MulEquiv.refl R, AddEquiv.refl R with }

Identity ring isomorphism

Informal description

The identity map is a ring isomorphism from a (semi)ring $R$ to itself, preserving both the multiplicative and additive structures.

RingEquiv.instInhabited instance

: Inhabited (R ≃+* R)

Full source

instance : Inhabited (R ≃+* R) :=
  ⟨RingEquiv.refl R⟩

Inhabited Type of Ring Automorphisms

Informal description

For any (semi)ring $R$, the type of ring automorphisms $R \simeq+* R$ is inhabited, with the identity map as a canonical element.

RingEquiv.refl_apply theorem

(x : R) : RingEquiv.refl R x = x

Full source

@[simp]
theorem refl_apply (x : R) : RingEquiv.refl R x = x :=
  rfl

Identity Ring Isomorphism Maps Element to Itself

Informal description

For any element $x$ in a (semi)ring $R$, the identity ring isomorphism $\text{refl}_R$ maps $x$ to itself, i.e., $\text{refl}_R(x) = x$.

RingEquiv.coe_refl theorem

(R : Type*) [Mul R] [Add R] : ⇑(RingEquiv.refl R) = id

Full source

@[simp]
theorem coe_refl (R : Type*) [Mul R] [Add R] : ⇑(RingEquiv.refl R) = id :=
  rfl

Identity Ring Isomorphism as Identity Function

Informal description

For any (semi)ring $R$, the underlying function of the identity ring isomorphism $\text{RingEquiv.refl} \, R$ is equal to the identity function $\text{id}$ on $R$.

RingEquiv.coe_addEquiv_refl theorem

: (RingEquiv.refl R : R ≃+ R) = AddEquiv.refl R

Full source

@[simp]
theorem coe_addEquiv_refl : (RingEquiv.refl R : R ≃+ R) = AddEquiv.refl R :=
  rfl

Identity Ring Isomorphism Yields Identity Additive Isomorphism

Informal description

The additive equivalence underlying the identity ring isomorphism $\text{RingEquiv.refl} : R \simeq+* R$ is equal to the identity additive equivalence $\text{AddEquiv.refl} : R \simeq+ R$.

RingEquiv.coe_mulEquiv_refl theorem

: (RingEquiv.refl R : R ≃* R) = MulEquiv.refl R

Full source

@[simp]
theorem coe_mulEquiv_refl : (RingEquiv.refl R : R ≃* R) = MulEquiv.refl R :=
  rfl

Multiplicative Equivalence Component of Identity Ring Isomorphism

Informal description

The multiplicative equivalence component of the identity ring isomorphism from a (semi)ring $R$ to itself is equal to the multiplicative identity isomorphism on $R$.

RingEquiv.symm definition

(e : R ≃+* S) : S ≃+* R

Full source

/-- The inverse of a ring isomorphism is a ring isomorphism. -/
@[symm]
protected def symm (e : R ≃+* S) : S ≃+* R :=
  { e.toMulEquiv.symm, e.toAddEquiv.symm with }

Inverse of a ring isomorphism

Informal description

Given a ring isomorphism $e : R \simeq+* S$ between two (semi)rings $R$ and $S$, the inverse map $e^{-1} : S \simeq+* R$ is also a ring isomorphism, preserving both the multiplicative and additive structures.

RingEquiv.invFun_eq_symm theorem

(f : R ≃+* S) : EquivLike.inv f = f.symm

Full source

@[simp]
theorem invFun_eq_symm (f : R ≃+* S) : EquivLike.inv f = f.symm :=
  rfl

Inverse Function of Ring Isomorphism Equals Its Symmetric Counterpart

Informal description

For any ring isomorphism $f : R \simeq+* S$ between two (semi)rings $R$ and $S$, the inverse function of $f$ (as defined by `EquivLike.inv`) is equal to the ring isomorphism inverse $f.symm$.

RingEquiv.symm_symm theorem

(e : R ≃+* S) : e.symm.symm = e

Full source

@[simp]
theorem symm_symm (e : R ≃+* S) : e.symm.symm = e := rfl

Double Inverse of Ring Isomorphism is Identity

Informal description

For any ring isomorphism $e : R \simeq+* S$ between (semi)rings $R$ and $S$, the double inverse $e^{-1^{-1}}$ equals $e$, i.e., $(e^{-1})^{-1} = e$.

RingEquiv.symm_bijective theorem

: Function.Bijective (RingEquiv.symm : (R ≃+* S) → S ≃+* R)

Full source

theorem symm_bijective : Function.Bijective (RingEquiv.symm : (R ≃+* S) → S ≃+* R) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Bijectivity of the Inverse Operation on Ring Isomorphisms

Informal description

The function $\text{symm} : (R \simeq+* S) \to (S \simeq+* R)$, which maps a ring isomorphism to its inverse, is bijective. That is, it is both injective (distinct isomorphisms have distinct inverses) and surjective (every ring isomorphism from $S$ to $R$ is the inverse of some ring isomorphism from $R$ to $S$).

RingEquiv.mk_coe' theorem

(e : R ≃+* S) (f h₁ h₂ h₃ h₄) : (⟨⟨f, ⇑e, h₁, h₂⟩, h₃, h₄⟩ : S ≃+* R) = e.symm

Full source

@[simp]
theorem mk_coe' (e : R ≃+* S) (f h₁ h₂ h₃ h₄) :
    (⟨⟨f, ⇑e, h₁, h₂⟩, h₃, h₄⟩ : S ≃+* R) = e.symm :=
  symm_bijective.injective <| ext fun _ => rfl

Constructed Inverse Equals Formal Inverse in Ring Isomorphisms

Informal description

Given a ring isomorphism $e : R \simeq+* S$ between (semi)rings $R$ and $S$, and functions $f : S \to R$, $h_1 : \text{LeftInverse}\ f\ e$, $h_2 : \text{RightInverse}\ f\ e$, $h_3 : \text{AddHom}\ f$, $h_4 : \text{MulHom}\ f$, the constructed ring isomorphism $\langle \langle f, e, h_1, h_2 \rangle, h_3, h_4 \rangle : S \simeq+* R$ equals the inverse isomorphism $e^{-1}$.

RingEquiv.symm_mk.aux definition

(f : R → S) (g h₁ h₂ h₃ h₄)

Full source

/-- Auxiliary definition to avoid looping in `dsimp` with `RingEquiv.symm_mk`. -/
protected def symm_mk.aux (f : R → S) (g h₁ h₂ h₃ h₄) := (mk ⟨f, g, h₁, h₂⟩ h₃ h₄).symm

Auxiliary function for inverse ring isomorphism construction

Informal description

The auxiliary function used in the definition of the inverse of a ring isomorphism constructed via `RingEquiv.mk`. Given functions $f : R \to S$ and $g : S \to R$ with appropriate properties (bijectivity and preservation of ring operations), this function helps define the inverse isomorphism $S \simeq+* R$ by ensuring the correct mapping between the underlying sets and preserving the ring structure.

RingEquiv.symm_mk theorem

 (f : R → S) (g h₁ h₂ h₃ h₄) :
  (mk ⟨f, g, h₁, h₂⟩ h₃ h₄).symm =
    { symm_mk.aux f g h₁ h₂ h₃ h₄ with
      toFun := g
      invFun := f }

Full source

@[simp]
theorem symm_mk (f : R → S) (g h₁ h₂ h₃ h₄) :
    (mk ⟨f, g, h₁, h₂⟩ h₃ h₄).symm =
      { symm_mk.aux f g h₁ h₂ h₃ h₄ with
        toFun := g
        invFun := f } :=
  rfl

Inverse of Constructed Ring Isomorphism Equals Construction with Swapped Functions

Informal description

Let $R$ and $S$ be (semi)rings, and let $f: R \to S$ and $g: S \to R$ be functions such that: 1. $g$ is a left inverse of $f$ (i.e., $g \circ f = \text{id}_R$) 2. $f$ is a left inverse of $g$ (i.e., $f \circ g = \text{id}_S$) 3. $f$ preserves addition 4. $f$ preserves multiplication Then the inverse of the ring isomorphism constructed from $f$ and $g$ (via `RingEquiv.mk`) is equal to the ring isomorphism constructed from $g$ and $f$ with the appropriate structure-preserving properties.

RingEquiv.symm_refl theorem

: (RingEquiv.refl R).symm = RingEquiv.refl R

Full source

@[simp]
theorem symm_refl : (RingEquiv.refl R).symm = RingEquiv.refl R :=
  rfl

Inverse of Identity Ring Isomorphism is Identity

Informal description

The inverse of the identity ring isomorphism from a (semi)ring $R$ to itself is again the identity ring isomorphism, i.e., $(\text{refl}_R)^{-1} = \text{refl}_R$.

RingEquiv.coe_toEquiv_symm theorem

(e : R ≃+* S) : (e.symm : S ≃ R) = (e : R ≃ S).symm

Full source

@[simp]
theorem coe_toEquiv_symm (e : R ≃+* S) : (e.symm : S ≃ R) = (e : R ≃ S).symm :=
  rfl

Inverse of Ring Equivalence Coerces to Inverse of Underlying Bijection

Informal description

For any ring equivalence $e : R \simeq+* S$ between (semi)rings $R$ and $S$, the underlying bijection of the inverse ring equivalence $e^{-1}$ is equal to the inverse of the underlying bijection of $e$. In other words, the coercion to the equivalence type commutes with taking inverses.

RingEquiv.coe_toMulEquiv_symm theorem

(e : R ≃+* S) : (e.symm : S ≃* R) = (e : R ≃* S).symm

Full source

@[simp]
theorem coe_toMulEquiv_symm (e : R ≃+* S) : (e.symm : S ≃* R) = (e : R ≃* S).symm :=
  rfl

Inverse of Ring Isomorphism as Multiplicative Equivalence

Informal description

For any ring isomorphism $e : R \simeq+* S$ between (semi)rings $R$ and $S$, the multiplicative equivalence underlying the inverse isomorphism $e^{-1} : S \simeq+* R$ is equal to the inverse of the multiplicative equivalence underlying $e$. In symbols: if we consider $e$ as a multiplicative equivalence ($e : R \simeq^* S$), then $(e^{-1} : S \simeq^* R) = (e : R \simeq^* S)^{-1}$.

RingEquiv.coe_toAddEquiv_symm theorem

(e : R ≃+* S) : (e.symm : S ≃+ R) = (e : R ≃+ S).symm

Full source

@[simp]
theorem coe_toAddEquiv_symm (e : R ≃+* S) : (e.symm : S ≃+ R) = (e : R ≃+ S).symm :=
  rfl

Inverse of Additive Component in Ring Equivalence

Informal description

For any ring equivalence $e : R \simeq+* S$ between (semi)rings $R$ and $S$, the additive equivalence component of the inverse $e^{-1} : S \simeq+ R$ is equal to the inverse of the additive equivalence component of $e : R \simeq+ S$.

RingEquiv.apply_symm_apply theorem

(e : R ≃+* S) : ∀ x, e (e.symm x) = x

Full source

@[simp]
theorem apply_symm_apply (e : R ≃+* S) : ∀ x, e (e.symm x) = x :=
  e.toEquiv.apply_symm_apply

Ring Isomorphism Recovery: $e(e^{-1}(x)) = x$

Informal description

For any ring isomorphism $e : R \simeq+* S$ between (semi)rings $R$ and $S$, and for any element $x \in S$, applying $e$ to the inverse image $e^{-1}(x)$ recovers the original element $x$, i.e., $e(e^{-1}(x)) = x$.

RingEquiv.symm_apply_apply theorem

(e : R ≃+* S) : ∀ x, e.symm (e x) = x

Full source

@[simp]
theorem symm_apply_apply (e : R ≃+* S) : ∀ x, e.symm (e x) = x :=
  e.toEquiv.symm_apply_apply

Inverse Ring Isomorphism Recovers Original Element

Informal description

For any ring isomorphism $e \colon R \simeq+* S$ between (semi)rings $R$ and $S$, and for any element $x \in R$, the inverse isomorphism $e^{-1}$ satisfies $e^{-1}(e(x)) = x$.

RingEquiv.image_eq_preimage theorem

(e : R ≃+* S) (s : Set R) : e '' s = e.symm ⁻¹' s

Full source

theorem image_eq_preimage (e : R ≃+* S) (s : Set R) : e '' s = e.symm ⁻¹' s :=
  e.toEquiv.image_eq_preimage s

Image-Preimage Equality for Ring Isomorphisms

Informal description

For any ring isomorphism $e \colon R \simeq^{+*} S$ between (semi)rings $R$ and $S$, and any subset $s \subseteq R$, the image of $s$ under $e$ is equal to the preimage of $s$ under the inverse isomorphism $e^{-1}$, i.e., \[ e(s) = e^{-1}^{-1}(s). \]

RingEquiv.Simps.symm_apply definition

(e : R ≃+* S) : S → R

Full source

/-- See Note [custom simps projection] -/
def Simps.symm_apply (e : R ≃+* S) : S → R :=
  e.symm

Inverse map of a ring isomorphism

Informal description

Given a ring isomorphism $e : R \simeq^{+*} S$ between two (semi)rings $R$ and $S$, the function maps an element $y \in S$ to its preimage $e^{-1}(y) \in R$ under the isomorphism $e$.

RingEquiv.trans definition

(e₁ : R ≃+* S) (e₂ : S ≃+* S') : R ≃+* S'

Full source

/-- Transitivity of `RingEquiv`. -/
@[trans]
protected def trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') : R ≃+* S' :=
  { e₁.toMulEquiv.trans e₂.toMulEquiv, e₁.toAddEquiv.trans e₂.toAddEquiv with }

Composition of ring (or semiring) equivalences

Informal description

Given two ring (or semiring) equivalences $e_1: R \simeq^{+*} S$ and $e_2: S \simeq^{+*} S'$, their composition $e_2 \circ e_1$ forms a ring equivalence $R \simeq^{+*} S'$ that preserves both the multiplicative and additive structures.

RingEquiv.coe_trans theorem

(e₁ : R ≃+* S) (e₂ : S ≃+* S') : (e₁.trans e₂ : R → S') = e₂ ∘ e₁

Full source

@[simp]
theorem coe_trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') : (e₁.trans e₂ : R → S') = e₂ ∘ e₁ :=
  rfl

Composition of Ring Equivalences as Function Composition

Informal description

For any ring equivalences $e_1: R \simeq^{+*} S$ and $e_2: S \simeq^{+*} S'$, the underlying function of their composition $e_1 \circ e_2$ is equal to the composition of their underlying functions, i.e., $(e_1 \circ e_2)(x) = e_2(e_1(x))$ for all $x \in R$.

RingEquiv.trans_apply theorem

(e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : R) : e₁.trans e₂ a = e₂ (e₁ a)

Full source

theorem trans_apply (e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : R) : e₁.trans e₂ a = e₂ (e₁ a) :=
  rfl

Application of Composition of Ring Equivalences: $(e_1 \circ e_2)(a) = e_2(e_1(a))$

Informal description

For any ring (or semiring) equivalences $e_1: R \simeq^{+*} S$ and $e_2: S \simeq^{+*} S'$, and any element $a \in R$, the application of the composed equivalence $e_1 \circ e_2$ to $a$ is equal to the application of $e_2$ to the result of applying $e_1$ to $a$, i.e., $(e_1 \circ e_2)(a) = e_2(e_1(a))$.

RingEquiv.symm_trans_apply theorem

(e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : S') : (e₁.trans e₂).symm a = e₁.symm (e₂.symm a)

Full source

@[simp]
theorem symm_trans_apply (e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : S') :
    (e₁.trans e₂).symm a = e₁.symm (e₂.symm a) :=
  rfl

Inverse of Composition of Ring Equivalences: $(e_1 \circ e_2)^{-1}(a) = e_1^{-1}(e_2^{-1}(a))$

Informal description

For any ring (or semiring) equivalences $e_1: R \simeq^{+*} S$ and $e_2: S \simeq^{+*} S'$, and any element $a \in S'$, the inverse of the composed equivalence $e_1 \circ e_2$ applied to $a$ equals the inverse of $e_1$ applied to the inverse of $e_2$ applied to $a$, i.e., $(e_1 \circ e_2)^{-1}(a) = e_1^{-1}(e_2^{-1}(a))$.

RingEquiv.symm_trans theorem

(e₁ : R ≃+* S) (e₂ : S ≃+* S') : (e₁.trans e₂).symm = e₂.symm.trans e₁.symm

Full source

theorem symm_trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') : (e₁.trans e₂).symm = e₂.symm.trans e₁.symm :=
  rfl

Inverse of Composition of Ring Equivalences is Reverse Composition of Inverses

Informal description

For any ring (or semiring) equivalences $e_1: R \simeq^{+*} S$ and $e_2: S \simeq^{+*} S'$, the inverse of their composition $(e_1 \circ e_2)^{-1}$ is equal to the composition of their inverses in reverse order, i.e., $(e_1 \circ e_2)^{-1} = e_2^{-1} \circ e_1^{-1}$.

RingEquiv.coe_mulEquiv_trans theorem

(e₁ : R ≃+* S) (e₂ : S ≃+* S') : (e₁.trans e₂ : R ≃* S') = (e₁ : R ≃* S).trans ↑e₂

Full source

@[simp]
theorem coe_mulEquiv_trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
    (e₁.trans e₂ : R ≃* S') = (e₁ : R ≃* S).trans ↑e₂ :=
  rfl

Composition of Ring Equivalences Preserves Multiplicative Structure

Informal description

For any ring equivalences $e_1: R \simeq^{+*} S$ and $e_2: S \simeq^{+*} S'$, the underlying multiplicative equivalence of their composition $(e_1 \circ e_2): R \simeq^* S'$ is equal to the composition of the underlying multiplicative equivalences $e_1: R \simeq^* S$ and $e_2: S \simeq^* S'$.

RingEquiv.coe_addEquiv_trans theorem

(e₁ : R ≃+* S) (e₂ : S ≃+* S') : (e₁.trans e₂ : R ≃+ S') = (e₁ : R ≃+ S).trans ↑e₂

Full source

@[simp]
theorem coe_addEquiv_trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
    (e₁.trans e₂ : R ≃+ S') = (e₁ : R ≃+ S).trans ↑e₂ :=
  rfl

Additive Equivalence of Composed Ring Equivalences

Informal description

For any ring equivalences $e₁: R \simeq^{+*} S$ and $e₂: S \simeq^{+*} S'$, the additive equivalence underlying their composition $(e₁ \circ e₂): R \simeq^{+} S'$ is equal to the composition of their underlying additive equivalences $e₁: R \simeq^{+} S$ and $e₂: S \simeq^{+} S'$.

RingEquiv.ofUnique definition

{M N} [Unique M] [Unique N] [Add M] [Mul M] [Add N] [Mul N] : M ≃+* N

Full source

/-- The `RingEquiv` between two semirings with a unique element. -/
def ofUnique {M N} [Unique M] [Unique N] [Add M] [Mul M] [Add N] [Mul N] : M ≃+* N :=
  { AddEquiv.ofUnique, MulEquiv.ofUnique with }

Ring equivalence between (semi)rings with unique elements

Informal description

Given two (semi)rings $ M $ and $ N $ each with a unique element, there exists a ring equivalence (i.e., a bijective homomorphism) between them that preserves both the additive and multiplicative structures. The equivalence maps the unique element of $ M $ to the unique element of $ N $.

RingEquiv.instUnique instance

{M N} [Unique M] [Unique N] [Add M] [Mul M] [Add N] [Mul N] : Unique (M ≃+* N)

Full source

instance {M N} [Unique M] [Unique N] [Add M] [Mul M] [Add N] [Mul N] :
    Unique (M ≃+* N) where
  default := .ofUnique
  uniq _ := ext fun _ => Subsingleton.elim _ _

Uniqueness of Ring Equivalence Between (Semi)rings with Unique Elements

Informal description

For any two (semi)rings $M$ and $N$ each with a unique element, there is exactly one ring equivalence between them. This equivalence preserves both the additive and multiplicative structures, mapping the unique element of $M$ to the unique element of $N$.

RingEquiv.op definition

{α β} [Add α] [Mul α] [Add β] [Mul β] : α ≃+* β ≃ (αᵐᵒᵖ ≃+* βᵐᵒᵖ)

Full source

/-- A ring iso `α ≃+* β` can equivalently be viewed as a ring iso `αᵐᵒᵖ ≃+* βᵐᵒᵖ`. -/
@[simps! symm_apply_apply symm_apply_symm_apply apply_apply apply_symm_apply]
protected def op {α β} [Add α] [Mul α] [Add β] [Mul β] :
    α ≃+* βα ≃+* β ≃ (αᵐᵒᵖ ≃+* βᵐᵒᵖ) where
  toFun f := { AddEquiv.mulOp f.toAddEquiv, MulEquiv.op f.toMulEquiv with }
  invFun f := { AddEquiv.mulOp.symm f.toAddEquiv, MulEquiv.op.symm f.toMulEquiv with }
  left_inv f := by
    ext
    rfl
  right_inv f := by
    ext
    rfl

Ring isomorphism equivalence between a ring and its multiplicative opposite

Informal description

For any (semi)rings $\alpha$ and $\beta$ equipped with addition and multiplication operations, there is a natural equivalence between the type of ring isomorphisms $\alpha \simeq^{+*} \beta$ and the type of ring isomorphisms $\alpha^\text{op} \simeq^{+*} \beta^\text{op}$, where $\text{op}$ denotes the multiplicative opposite. Specifically: 1. The forward direction maps a ring isomorphism $f : \alpha \simeq^{+*} \beta$ to the isomorphism $\alpha^\text{op} \simeq^{+*} \beta^\text{op}$ by composing with the opposite operations. 2. The inverse direction reverses this process. 3. These operations are mutual inverses, establishing a bijection between the two types of isomorphisms.

RingEquiv.unop definition

{α β} [Add α] [Mul α] [Add β] [Mul β] : αᵐᵒᵖ ≃+* βᵐᵒᵖ ≃ (α ≃+* β)

Full source

/-- The 'unopposite' of a ring iso `αᵐᵒᵖ ≃+* βᵐᵒᵖ`. Inverse to `RingEquiv.op`. -/
@[simp]
protected def unop {α β} [Add α] [Mul α] [Add β] [Mul β] : αᵐᵒᵖαᵐᵒᵖ ≃+* βᵐᵒᵖαᵐᵒᵖ ≃+* βᵐᵒᵖ ≃ (α ≃+* β) :=
  RingEquiv.op.symm

Inverse of the ring isomorphism opposite operation

Informal description

The inverse operation of `RingEquiv.op`, which converts a ring isomorphism between the multiplicative opposites $\alpha^\text{op}$ and $\beta^\text{op}$ back to a ring isomorphism between the original rings $\alpha$ and $\beta$.

RingEquiv.opOp definition

(R : Type*) [Add R] [Mul R] : R ≃+* Rᵐᵒᵖᵐᵒᵖ

Full source

/-- A ring is isomorphic to the opposite of its opposite. -/
@[simps!]
def opOp (R : Type*) [Add R] [Mul R] : R ≃+* Rᵐᵒᵖᵐᵒᵖ where
  __ := MulEquiv.opOp R
  map_add' _ _ := rfl

Ring isomorphism between a ring and its double multiplicative opposite

Informal description

For any type $ R $ equipped with addition and multiplication operations, there is a ring isomorphism between $ R $ and the double multiplicative opposite $ R^{\text{op}\text{op}} $. This isomorphism preserves both the additive and multiplicative structures, where the double opposite $ R^{\text{op}\text{op}} $ is obtained by applying the multiplicative opposite construction twice.

RingEquiv.toOpposite definition

: R ≃+* Rᵐᵒᵖ

Full source

/-- A non-unital commutative ring is isomorphic to its opposite. -/
def toOpposite : R ≃+* Rᵐᵒᵖ :=
  { MulOpposite.opEquiv with
    map_add' := fun _ _ => rfl
    map_mul' := fun x y => mul_comm (op y) (op x) }

Ring isomorphism to the multiplicative opposite

Informal description

The ring isomorphism from a non-unital commutative semiring $ R $ to its multiplicative opposite $ R^\text{op} $, defined by the canonical embedding $ \text{op} : R \to R^\text{op} $. This isomorphism preserves both addition and multiplication, where multiplication in $ R^\text{op} $ is defined by $ \text{op}(x) \cdot \text{op}(y) = \text{op}(y \cdot x) $ for all $ x, y \in R $.

RingEquiv.toOpposite_apply theorem

(r : R) : toOpposite R r = op r

Full source

@[simp]
theorem toOpposite_apply (r : R) : toOpposite R r = op r :=
  rfl

Application of Ring Isomorphism to Multiplicative Opposite: $\text{toOpposite}(r) = \text{op}(r)$

Informal description

For any element $r$ in a non-unital commutative semiring $R$, the ring isomorphism $\text{toOpposite} : R \simeq+* R^\text{op}$ maps $r$ to its multiplicative opposite $\text{op}(r) \in R^\text{op}$.

RingEquiv.toOpposite_symm_apply theorem

(r : Rᵐᵒᵖ) : (toOpposite R).symm r = unop r

Full source

@[simp]
theorem toOpposite_symm_apply (r : Rᵐᵒᵖ) : (toOpposite R).symm r = unop r :=
  rfl

Inverse of Ring Isomorphism to Opposite Ring: $(\text{toOpposite})^{-1}(r) = \text{unop}(r)$

Informal description

For any element $r$ in the multiplicative opposite $R^\text{op}$ of a non-unital commutative semiring $R$, the inverse of the ring isomorphism $\text{toOpposite} : R \simeq+* R^\text{op}$ maps $r$ back to its original element in $R$, i.e., $(\text{toOpposite})^{-1}(r) = \text{unop}(r)$.

RingEquiv.map_zero theorem

: f 0 = 0

Full source

/-- A ring isomorphism sends zero to zero. -/
protected theorem map_zero : f 0 = 0 :=
  map_zero f

Ring Equivalence Preserves Zero: $f(0) = 0$

Informal description

For any ring equivalence $f : R \simeq+* S$ between two (non-unital non-associative semi)rings $R$ and $S$, the zero element of $R$ is mapped to the zero element of $S$, i.e., $f(0) = 0$.

RingEquiv.map_eq_zero_iff theorem

: f x = 0 ↔ x = 0

Full source

protected theorem map_eq_zero_iff : f x = 0 ↔ x = 0 :=
  EmbeddingLike.map_eq_zero_iff

Ring equivalence preserves zero: $f(x) = 0 \leftrightarrow x = 0$

Informal description

For any ring equivalence $f : R \simeq+* S$ between (non-unital non-associative semi)rings $R$ and $S$, and for any element $x \in R$, we have $f(x) = 0$ if and only if $x = 0$.

RingEquiv.map_ne_zero_iff theorem

: f x ≠ 0 ↔ x ≠ 0

Full source

theorem map_ne_zero_iff : f x ≠ 0f x ≠ 0 ↔ x ≠ 0 :=
  EmbeddingLike.map_ne_zero_iff

Ring equivalence preserves non-zero elements: $f(x) \neq 0 \leftrightarrow x \neq 0$

Informal description

For any ring equivalence $f \colon R \simeq+* S$ between (non-unital non-associative semi)rings $R$ and $S$, and for any element $x \in R$, we have $f(x) \neq 0$ if and only if $x \neq 0$.

RingEquiv.ofBijective definition

[NonUnitalRingHomClass F R S] (f : F) (hf : Function.Bijective f) : R ≃+* S

Full source

/-- Produce a ring isomorphism from a bijective ring homomorphism. -/
noncomputable def ofBijective [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Bijective f) :
    R ≃+* S :=
  { Equiv.ofBijective f hf with
    map_mul' := map_mul f
    map_add' := map_add f }

Ring isomorphism from a bijective ring homomorphism

Informal description

Given a bijective ring homomorphism $f : R \to S$ between (non-unital non-associative semi)rings $R$ and $S$, the function constructs a ring isomorphism $R \simeq+* S$ by combining the bijection with the multiplicative and additive homomorphism properties of $f$.

RingEquiv.coe_ofBijective theorem

[NonUnitalRingHomClass F R S] (f : F) (hf : Function.Bijective f) : (ofBijective f hf : R → S) = f

Full source

@[simp]
theorem coe_ofBijective [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Bijective f) :
    (ofBijective f hf : R → S) = f :=
  rfl

Coercion of Bijective Ring Homomorphism to Function Equals Original Homomorphism

Informal description

Given a bijective ring homomorphism $f \colon R \to S$ between (non-unital non-associative semi)rings $R$ and $S$, the underlying function of the ring isomorphism $\text{ofBijective}\, f\, hf$ is equal to $f$. In other words, the coercion of the constructed ring equivalence to a function coincides with the original homomorphism $f$.

RingEquiv.ofBijective_apply theorem

[NonUnitalRingHomClass F R S] (f : F) (hf : Function.Bijective f) (x : R) : ofBijective f hf x = f x

Full source

theorem ofBijective_apply [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Bijective f)
    (x : R) : ofBijective f hf x = f x :=
  rfl

Application of Ring Isomorphism Constructed from Bijective Homomorphism

Informal description

Let $R$ and $S$ be (non-unital non-associative semi)rings, and let $f : R \to S$ be a bijective ring homomorphism. Then for any $x \in R$, the ring isomorphism $\text{ofBijective}\,f\,\text{hf}$ satisfies $(\text{ofBijective}\,f\,\text{hf})(x) = f(x)$.

RingEquiv.piUnique definition

{ι : Type*} (R : ι → Type*) [Unique ι] [∀ i, NonUnitalNonAssocSemiring (R i)] : (∀ i, R i) ≃+* R default

Full source

/-- Product of a singleton family of (non-unital non-associative semi)rings is isomorphic
to the only member of this family. -/
@[simps! -fullyApplied]
def piUnique {ι : Type*} (R : ι → Type*) [Unique ι] [∀ i, NonUnitalNonAssocSemiring (R i)] :
    (∀ i, R i) ≃+* R default where
  __ := Equiv.piUnique R
  map_add' _ _ := rfl
  map_mul' _ _ := rfl

Isomorphism between product of semirings over a unique index and the default semiring

Informal description

For a unique index type $\iota$ (i.e., a type with exactly one element) and a family of non-unital non-associative semirings $(R_i)_{i \in \iota}$, the product semiring $\prod_{i \in \iota} R_i$ is isomorphic to $R_{\text{default}}$ (the semiring at the unique default index), where the isomorphism preserves both the additive and multiplicative structures. The isomorphism maps a dependent function $f$ to its value at the default index, and conversely, any element of $R_{\text{default}}$ can be uniquely extended to a constant dependent function on $\iota$.

RingEquiv.piCongrRight definition

 {ι : Type*} {R S : ι → Type*} [∀ i, NonUnitalNonAssocSemiring (R i)] [∀ i, NonUnitalNonAssocSemiring (S i)]
  (e : ∀ i, R i ≃+* S i) : (∀ i, R i) ≃+* ∀ i, S i

Full source

/-- A family of ring isomorphisms `∀ j, (R j ≃+* S j)` generates a
ring isomorphisms between `∀ j, R j` and `∀ j, S j`.

This is the `RingEquiv` version of `Equiv.piCongrRight`, and the dependent version of
`RingEquiv.arrowCongr`.
-/
@[simps apply]
def piCongrRight {ι : Type*} {R S : ι → Type*} [∀ i, NonUnitalNonAssocSemiring (R i)]
    [∀ i, NonUnitalNonAssocSemiring (S i)] (e : ∀ i, R i ≃+* S i) : (∀ i, R i) ≃+* ∀ i, S i :=
  { @MulEquiv.piCongrRight ι R S _ _ fun i => (e i).toMulEquiv,
    @AddEquiv.piCongrRight ι R S _ _ fun i => (e i).toAddEquiv with
    toFun := fun x j => e j (x j)
    invFun := fun x j => (e j).symm (x j) }

Component-wise ring isomorphism of product semirings

Informal description

Given an index type $\iota$ and families of non-unital non-associative semirings $(R_i)_{i \in \iota}$ and $(S_i)_{i \in \iota}$, along with a family of ring isomorphisms $(e_i : R_i \simeq+* S_i)_{i \in \iota}$, there exists a ring isomorphism between the product semirings $\prod_{i \in \iota} R_i$ and $\prod_{i \in \iota} S_i$. This isomorphism maps a tuple $(x_i)_{i \in \iota}$ to $(e_i(x_i))_{i \in \iota}$, and its inverse maps $(y_i)_{i \in \iota}$ to $(e_i^{-1}(y_i))_{i \in \iota}$. The isomorphism preserves both the additive and multiplicative structures component-wise.

RingEquiv.piCongrRight_refl theorem

 {ι : Type*} {R : ι → Type*} [∀ i, NonUnitalNonAssocSemiring (R i)] :
  (piCongrRight fun i => RingEquiv.refl (R i)) = RingEquiv.refl _

Full source

@[simp]
theorem piCongrRight_refl {ι : Type*} {R : ι → Type*} [∀ i, NonUnitalNonAssocSemiring (R i)] :
    (piCongrRight fun i => RingEquiv.refl (R i)) = RingEquiv.refl _ :=
  rfl

Identity Component-wise Ring Isomorphism Equals Identity on Product Semiring

Informal description

For any index type $\iota$ and any family of non-unital non-associative semirings $(R_i)_{i \in \iota}$, the component-wise ring isomorphism constructed from the identity isomorphisms on each $R_i$ is equal to the identity isomorphism on the product semiring $\prod_{i \in \iota} R_i$. In other words, if we apply the identity isomorphism to each component $R_i$, the resulting product isomorphism is the identity isomorphism on the entire product space.

RingEquiv.piCongrRight_symm theorem

 {ι : Type*} {R S : ι → Type*} [∀ i, NonUnitalNonAssocSemiring (R i)] [∀ i, NonUnitalNonAssocSemiring (S i)]
  (e : ∀ i, R i ≃+* S i) : (piCongrRight e).symm = piCongrRight fun i => (e i).symm

Full source

@[simp]
theorem piCongrRight_symm {ι : Type*} {R S : ι → Type*} [∀ i, NonUnitalNonAssocSemiring (R i)]
    [∀ i, NonUnitalNonAssocSemiring (S i)] (e : ∀ i, R i ≃+* S i) :
    (piCongrRight e).symm = piCongrRight fun i => (e i).symm :=
  rfl

Inverse of Component-wise Ring Isomorphism Equals Component-wise Inverses

Informal description

Given an index type $\iota$ and families of non-unital non-associative semirings $(R_i)_{i \in \iota}$ and $(S_i)_{i \in \iota}$, along with a family of ring isomorphisms $(e_i : R_i \simeq+* S_i)_{i \in \iota}$, the inverse of the component-wise ring isomorphism $\prod_{i \in \iota} R_i \simeq+* \prod_{i \in \iota} S_i$ is equal to the component-wise ring isomorphism formed by taking the inverses of each $e_i$.

RingEquiv.piCongrRight_trans theorem

 {ι : Type*} {R S T : ι → Type*} [∀ i, NonUnitalNonAssocSemiring (R i)] [∀ i, NonUnitalNonAssocSemiring (S i)]
  [∀ i, NonUnitalNonAssocSemiring (T i)] (e : ∀ i, R i ≃+* S i) (f : ∀ i, S i ≃+* T i) :
  (piCongrRight e).trans (piCongrRight f) = piCongrRight fun i => (e i).trans (f i)

Full source

@[simp]
theorem piCongrRight_trans {ι : Type*} {R S T : ι → Type*}
    [∀ i, NonUnitalNonAssocSemiring (R i)] [∀ i, NonUnitalNonAssocSemiring (S i)]
    [∀ i, NonUnitalNonAssocSemiring (T i)] (e : ∀ i, R i ≃+* S i) (f : ∀ i, S i ≃+* T i) :
    (piCongrRight e).trans (piCongrRight f) = piCongrRight fun i => (e i).trans (f i) :=
  rfl

Composition of Component-wise Ring Isomorphisms on Product Semirings

Informal description

Let $\iota$ be an index type, and let $(R_i)_{i \in \iota}$, $(S_i)_{i \in \iota}$, and $(T_i)_{i \in \iota}$ be families of non-unital non-associative semirings. Given families of ring isomorphisms $(e_i : R_i \simeq^{+*} S_i)_{i \in \iota}$ and $(f_i : S_i \simeq^{+*} T_i)_{i \in \iota}$, the composition of the product ring isomorphisms $\text{piCongrRight}(e)$ and $\text{piCongrRight}(f)$ is equal to the product ring isomorphism $\text{piCongrRight}(\lambda i, e_i \circ f_i)$. In other words, the following diagram commutes: \[ \prod_{i \in \iota} R_i \xrightarrow{\text{piCongrRight}(e)} \prod_{i \in \iota} S_i \xrightarrow{\text{piCongrRight}(f)} \prod_{i \in \iota} T_i \] and the composition is equivalent to applying the component-wise composition of $e_i$ and $f_i$ directly via $\text{piCongrRight}$.

RingEquiv.piCongrLeft' definition

 {ι ι' : Type*} (R : ι → Type*) (e : ι ≃ ι') [∀ i, NonUnitalNonAssocSemiring (R i)] :
  ((i : ι) → R i) ≃+* ((i : ι') → R (e.symm i))

Full source

/-- Transport dependent functions through an equivalence of the base space.

This is `Equiv.piCongrLeft'` as a `RingEquiv`. -/
@[simps!]
def piCongrLeft' {ι ι' : Type*} (R : ι → Type*) (e : ι ≃ ι')
    [∀ i, NonUnitalNonAssocSemiring (R i)] :
    ((i : ι) → R i) ≃+* ((i : ι') → R (e.symm i)) where
  toEquiv := Equiv.piCongrLeft' R e
  map_mul' _ _ := rfl
  map_add' _ _ := rfl

Ring equivalence of dependent product rings under index equivalence

Informal description

Given an equivalence $e : \iota \simeq \iota'$ between index types and a family of non-unital non-associative semirings $(R_i)_{i \in \iota}$, the function `RingEquiv.piCongrLeft'` constructs a ring equivalence between the product rings $\prod_{i \in \iota} R_i$ and $\prod_{i' \in \iota'} R_{e^{-1}(i')}$. This equivalence: 1. Transports dependent functions through the base equivalence $e$ 2. Preserves both multiplication and addition pointwise

RingEquiv.piCongrLeft'_symm theorem

 {R : Type*} [NonUnitalNonAssocSemiring R] (e : α ≃ β) :
  (RingEquiv.piCongrLeft' (fun _ => R) e).symm = RingEquiv.piCongrLeft' _ e.symm

Full source

@[simp]
theorem piCongrLeft'_symm {R : Type*} [NonUnitalNonAssocSemiring R] (e : α ≃ β) :
    (RingEquiv.piCongrLeft' (fun _ => R) e).symm = RingEquiv.piCongrLeft' _ e.symm := by
  simp only [piCongrLeft', RingEquiv.symm, MulEquiv.symm, Equiv.piCongrLeft'_symm]

Inverse of Constant Family Ring Equivalence via Index Equivalence

Informal description

Let $R$ be a non-unital non-associative semiring and let $e : \alpha \simeq \beta$ be an equivalence between types $\alpha$ and $\beta$. Then the inverse of the ring equivalence $\text{piCongrLeft}'$ (applied to the constant family $\lambda \_, R$) is equal to $\text{piCongrLeft}'$ applied to $R$ and the inverse equivalence $e^{-1} : \beta \simeq \alpha$.

RingEquiv.piCongrLeft definition

 {ι ι' : Type*} (S : ι' → Type*) (e : ι ≃ ι') [∀ i, NonUnitalNonAssocSemiring (S i)] :
  ((i : ι) → S (e i)) ≃+* ((i : ι') → S i)

Full source

/-- Transport dependent functions through an equivalence of the base space.

This is `Equiv.piCongrLeft` as a `RingEquiv`. -/
@[simps!]
def piCongrLeft {ι ι' : Type*} (S : ι' → Type*) (e : ι ≃ ι')
    [∀ i, NonUnitalNonAssocSemiring (S i)] :
    ((i : ι) → S (e i)) ≃+* ((i : ι') → S i) :=
  (RingEquiv.piCongrLeft' S e.symm).symm

Ring equivalence of dependent product rings under index equivalence (forward version)

Informal description

Given an equivalence $e : \iota \simeq \iota'$ between index types and a family of non-unital non-associative semirings $(S_i)_{i \in \iota'}$, the function `RingEquiv.piCongrLeft` constructs a ring equivalence between the product rings $\prod_{i \in \iota} S_{e(i)}$ and $\prod_{i' \in \iota'} S_{i'}$. This equivalence: 1. Transports dependent functions through the base equivalence $e$ 2. Preserves both multiplication and addition pointwise

RingEquiv.piEquivPiSubtypeProd definition

 {ι : Type*} (p : ι → Prop) [DecidablePred p] (Y : ι → Type*) [∀ i, NonUnitalNonAssocSemiring (Y i)] :
  ((i : ι) → Y i) ≃+* ((i : { x : ι // p x }) → Y i) × ((i : { x : ι // ¬p x }) → Y i)

Full source

/-- Splits the indices of ring `∀ (i : ι), Y i` along the predicate `p`. This is
`Equiv.piEquivPiSubtypeProd` as a `RingEquiv`. -/
@[simps!]
def piEquivPiSubtypeProd {ι : Type*} (p : ι → Prop) [DecidablePred p] (Y : ι → Type*)
    [∀ i, NonUnitalNonAssocSemiring (Y i)] :
    ((i : ι) → Y i) ≃+* ((i : { x : ι // p x }) → Y i) × ((i : { x : ι // ¬p x }) → Y i) where
  toEquiv := Equiv.piEquivPiSubtypeProd p Y
  map_mul' _ _ := rfl
  map_add' _ _ := rfl

Ring isomorphism between product and restricted product decomposition

Informal description

Given a type $\iota$ with a decidable predicate $p : \iota \to \text{Prop}$ and a family of non-unital non-associative semirings $(Y_i)_{i \in \iota}$, there is a ring isomorphism between the product of all $Y_i$ and the product of the restricted products over the subtypes $\{x \mid p x\}$ and $\{x \mid \neg p x\}$. More precisely, the isomorphism maps a function $f$ to the pair $(f \restriction_{\{x \mid p x\}}, f \restriction_{\{x \mid \neg p x\}})$, preserving both the additive and multiplicative structures.

RingEquiv.prodCongr definition

 {R R' S S' : Type*} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S]
  [NonUnitalNonAssocSemiring S'] (f : R ≃+* R') (g : S ≃+* S') : R × S ≃+* R' × S'

Full source

/-- Product of ring equivalences. This is `Equiv.prodCongr` as a `RingEquiv`. -/
@[simps!]
def prodCongr {R R' S S' : Type*} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring R']
    [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring S']
    (f : R ≃+* R') (g : S ≃+* S') :
    R × SR × S ≃+* R' × S' where
  toEquiv := Equiv.prodCongr f g
  map_mul' _ _ := by
    simp only [Equiv.toFun_as_coe, Equiv.prodCongr_apply, EquivLike.coe_coe,
      Prod.map, Prod.fst_mul, map_mul, Prod.snd_mul, Prod.mk_mul_mk]
  map_add' _ _ := by
    simp only [Equiv.toFun_as_coe, Equiv.prodCongr_apply, EquivLike.coe_coe,
      Prod.map, Prod.fst_add, map_add, Prod.snd_add, Prod.mk_add_mk]

Product of ring equivalences

Informal description

Given two ring equivalences (isomorphisms) $f : R \simeq+* R'$ and $g : S \simeq+* S'$ between non-unital non-associative semirings, the function `RingEquiv.prodCongr` constructs a ring equivalence between the product rings $R \times S$ and $R' \times S'$ by applying $f$ to the first component and $g$ to the second component of each pair. The equivalence preserves both the multiplicative and additive structures componentwise.

RingEquiv.coe_prodCongr theorem

 {R R' S S' : Type*} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S]
  [NonUnitalNonAssocSemiring S'] (f : R ≃+* R') (g : S ≃+* S') : ⇑(RingEquiv.prodCongr f g) = Prod.map f g

Full source

@[simp]
theorem coe_prodCongr {R R' S S' : Type*} [NonUnitalNonAssocSemiring R]
    [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring S']
    (f : R ≃+* R') (g : S ≃+* S') :
    ⇑(RingEquiv.prodCongr f g) = Prod.map f g :=
  rfl

Componentwise Action of Product Ring Isomorphism

Informal description

Given two ring isomorphisms $f \colon R \simeq+* R'$ and $g \colon S \simeq+* S'$ between non-unital non-associative semirings, the underlying function of the product isomorphism $\text{RingEquiv.prodCongr}\, f\, g$ is equal to the componentwise application $\text{Prod.map}\, f\, g$. In other words, for any $(r,s) \in R \times S$, we have $(\text{RingEquiv.prodCongr}\, f\, g)(r,s) = (f(r), g(s))$.

RingEquiv.piOptionEquivProd definition

 {ι : Type*} {R : Option ι → Type*} [Π i, NonUnitalNonAssocSemiring (R i)] : (Π i, R i) ≃+* R none × (Π i, R (some i))

Full source

/-- This is `Equiv.piOptionEquivProd` as a `RingEquiv`. -/
@[simps!]
def piOptionEquivProd {ι : Type*} {R : Option ι → Type*} [Π i, NonUnitalNonAssocSemiring (R i)] :
    (Π i, R i) ≃+* R none × (Π i, R (some i)) where
  toEquiv := Equiv.piOptionEquivProd
  map_add' _ _ := rfl
  map_mul' _ _ := rfl

Ring equivalence between product over options and binary product

Informal description

For any type $\iota$ and any family of non-unital non-associative semirings $(R_i)_{i \in \text{Option } \iota}$, there is a ring equivalence between the product of $R_i$ over all $i \in \text{Option } \iota$ and the direct product of $R_{\text{none}}$ with the product of $R_{\text{some } i}$ over all $i \in \iota$. This equivalence maps a function $f : \prod_{i \in \text{Option } \iota} R_i$ to the pair $(f(\text{none}), \lambda i, f(\text{some } i))$, and preserves both the additive and multiplicative structures.

RingEquiv.map_one theorem

: f 1 = 1

Full source

/-- A ring isomorphism sends one to one. -/
protected theorem map_one : f 1 = 1 :=
  map_one f

Ring Equivalence Preserves Multiplicative Identity

Informal description

For any ring equivalence $f \colon R \simeq+* S$ between (semi)rings $R$ and $S$, the image of the multiplicative identity $1_R$ under $f$ is the multiplicative identity $1_S$, i.e., $f(1_R) = 1_S$.

RingEquiv.map_eq_one_iff theorem

: f x = 1 ↔ x = 1

Full source

protected theorem map_eq_one_iff : f x = 1 ↔ x = 1 :=
  EmbeddingLike.map_eq_one_iff

Ring Equivalence Preserves Identity: $f(x) = 1 \leftrightarrow x = 1$

Informal description

For any ring equivalence $f : R \simeq+* S$ between (non-unital non-associative semi)rings $R$ and $S$, and for any element $x \in R$, we have $f(x) = 1$ if and only if $x = 1$.

RingEquiv.map_ne_one_iff theorem

: f x ≠ 1 ↔ x ≠ 1

Full source

theorem map_ne_one_iff : f x ≠ 1f x ≠ 1 ↔ x ≠ 1 :=
  EmbeddingLike.map_ne_one_iff

Non-Identity Preservation under Ring Equivalences: $f(x) \neq 1 \leftrightarrow x \neq 1$

Informal description

For any ring equivalence $f \colon R \simeq+* S$ between non-associative semirings $R$ and $S$, and for any element $x \in R$, we have $f(x) \neq 1$ if and only if $x \neq 1$.

RingEquiv.coe_monoidHom_refl theorem

: (RingEquiv.refl R : R →* R) = MonoidHom.id R

Full source

theorem coe_monoidHom_refl : (RingEquiv.refl R : R →* R) = MonoidHom.id R :=
  rfl

Identity Ring Isomorphism Yields Identity Monoid Homomorphism

Informal description

The monoid homomorphism obtained by coercing the identity ring isomorphism $\text{RingEquiv.refl} \colon R \simeq+* R$ is equal to the identity monoid homomorphism $\text{MonoidHom.id} \colon R \to* R$.

RingEquiv.coe_addMonoidHom_refl theorem

: (RingEquiv.refl R : R →+ R) = AddMonoidHom.id R

Full source

@[simp]
theorem coe_addMonoidHom_refl : (RingEquiv.refl R : R →+ R) = AddMonoidHom.id R :=
  rfl

Identity Ring Isomorphism Yields Identity Additive Homomorphism

Informal description

For any (semi)ring $R$, the additive monoid homomorphism associated with the identity ring isomorphism $\text{refl}_R : R \simeq+* R$ is equal to the identity additive monoid homomorphism on $R$.

RingEquiv.coe_ringHom_refl theorem

: (RingEquiv.refl R : R →+* R) = RingHom.id R

Full source

@[simp]
theorem coe_ringHom_refl : (RingEquiv.refl R : R →+* R) = RingHom.id R :=
  rfl

Identity Ring Isomorphism Coerces to Identity Ring Homomorphism

Informal description

The coercion of the identity ring isomorphism $\text{RingEquiv.refl} : R \simeq+* R$ to a ring homomorphism is equal to the identity ring homomorphism $\text{RingHom.id} : R \to+* R$.

RingEquiv.coe_monoidHom_trans theorem

 [NonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') : (e₁.trans e₂ : R →* S') = (e₂ : S →* S').comp ↑e₁

Full source

@[simp]
theorem coe_monoidHom_trans [NonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
    (e₁.trans e₂ : R →* S') = (e₂ : S →* S').comp ↑e₁ :=
  rfl

Composition of Ring Equivalences as Monoid Homomorphisms

Informal description

Let $R$, $S$, and $S'$ be non-associative semirings, and let $e_1: R \simeq^{+*} S$ and $e_2: S \simeq^{+*} S'$ be ring equivalences. Then the monoid homomorphism obtained from the composition $e_2 \circ e_1$ is equal to the composition of the monoid homomorphisms obtained from $e_2$ and $e_1$, i.e., $$(e_2 \circ e_1)_{\text{monoid}} = (e_2)_{\text{monoid}} \circ (e_1)_{\text{monoid}}.$$

RingEquiv.coe_addMonoidHom_trans theorem

 [NonUnitalNonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') : (e₁.trans e₂ : R →+ S') = (e₂ : S →+ S').comp ↑e₁

Full source

@[simp]
theorem coe_addMonoidHom_trans [NonUnitalNonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
    (e₁.trans e₂ : R →+ S') = (e₂ : S →+ S').comp ↑e₁ :=
  rfl

Composition of Ring Equivalences as Additive Monoid Homomorphisms

Informal description

Let $R$, $S$, and $S'$ be non-unital non-associative semirings, and let $e_1: R \simeq^{+*} S$ and $e_2: S \simeq^{+*} S'$ be ring equivalences. Then the additive monoid homomorphism corresponding to the composition $e_2 \circ e_1$ is equal to the composition of the additive monoid homomorphisms corresponding to $e_2$ and $e_1$. In other words, $(e_2 \circ e_1 : R \to^+ S') = (e_2 : S \to^+ S') \circ (e_1 : R \to^+ S)$.

RingEquiv.coe_ringHom_trans theorem

 [NonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') : (e₁.trans e₂ : R →+* S') = (e₂ : S →+* S').comp ↑e₁

Full source

@[simp]
theorem coe_ringHom_trans [NonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
    (e₁.trans e₂ : R →+* S') = (e₂ : S →+* S').comp ↑e₁ :=
  rfl

Composition of Ring Equivalences as Ring Homomorphisms

Informal description

Let $R$, $S$, and $S'$ be non-associative semirings, and let $e_1: R \simeq^{+*} S$ and $e_2: S \simeq^{+*} S'$ be ring equivalences. Then the ring homomorphism obtained from the composition $e_2 \circ e_1$ is equal to the composition of the ring homomorphisms obtained from $e_2$ and $e_1$, i.e., $$(e_1 \circ e_2)_{\text{ring}} = (e_2)_{\text{ring}} \circ (e_1)_{\text{ring}}.$$

RingEquiv.comp_symm theorem

(e : R ≃+* S) : (e : R →+* S).comp (e.symm : S →+* R) = RingHom.id S

Full source

@[simp]
theorem comp_symm (e : R ≃+* S) : (e : R →+* S).comp (e.symm : S →+* R) = RingHom.id S :=
  RingHom.ext e.apply_symm_apply

Composition of Ring Isomorphism with Its Inverse Yields Identity on Codomain

Informal description

For any ring isomorphism $e : R \simeq^{+*} S$ between (non-associative) semirings $R$ and $S$, the composition of the ring homomorphism $e : R \to^{+*} S$ with its inverse $e^{-1} : S \to^{+*} R$ equals the identity ring homomorphism on $S$, i.e., $$e \circ e^{-1} = \text{id}_S.$$

RingEquiv.symm_comp theorem

(e : R ≃+* S) : (e.symm : S →+* R).comp (e : R →+* S) = RingHom.id R

Full source

@[simp]
theorem symm_comp (e : R ≃+* S) : (e.symm : S →+* R).comp (e : R →+* S) = RingHom.id R :=
  RingHom.ext e.symm_apply_apply

Inverse Ring Isomorphism Composes to Identity on $R$

Informal description

For any ring isomorphism $e \colon R \simeq^{+*} S$ between (semi)rings $R$ and $S$, the composition of the ring homomorphism associated to $e$ with the ring homomorphism associated to its inverse $e^{-1}$ is equal to the identity ring homomorphism on $R$, i.e., $$(e^{-1})_{\text{ring}} \circ e_{\text{ring}} = \text{id}_R.$$

RingEquiv.map_neg theorem

: f (-x) = -f x

Full source

protected theorem map_neg : f (-x) = -f x :=
  map_neg f x

Ring Equivalence Preserves Negation: $f(-x) = -f(x)$

Informal description

For any ring equivalence $f : R \simeq+* S$ between two (non-unital non-associative) rings $R$ and $S$, and for any element $x \in R$, the equivalence preserves negation: $f(-x) = -f(x)$.

RingEquiv.map_sub theorem

: f (x - y) = f x - f y

Full source

protected theorem map_sub : f (x - y) = f x - f y :=
  map_sub f x y

Ring Equivalence Preserves Subtraction: $f(x - y) = f(x) - f(y)$

Informal description

For any ring equivalence $f : R \simeq+* S$ between two (non-unital non-associative) rings $R$ and $S$, and for any elements $x, y \in R$, the equivalence preserves subtraction: $f(x - y) = f(x) - f(y)$.

RingEquiv.map_neg_one theorem

: f (-1) = -1

Full source

@[simp]
theorem map_neg_one : f (-1) = -1 :=
  f.map_one ▸ f.map_neg 1

Ring Equivalence Preserves Negative One: $f(-1) = -1$

Informal description

For any ring equivalence $f \colon R \simeq+* S$ between (semi)rings $R$ and $S$, the image of the additive inverse of the multiplicative identity $-1_R$ under $f$ is the additive inverse of the multiplicative identity $-1_S$, i.e., $f(-1_R) = -1_S$.

RingEquiv.map_eq_neg_one_iff theorem

{x : R} : f x = -1 ↔ x = -1

Full source

theorem map_eq_neg_one_iff {x : R} : f x = -1 ↔ x = -1 := by
  rw [← neg_eq_iff_eq_neg, ← neg_eq_iff_eq_neg, ← map_neg, RingEquiv.map_eq_one_iff]

Ring Equivalence Preserves Negative Identity: $f(x) = -1 \leftrightarrow x = -1$

Informal description

For any ring equivalence $f : R \simeq+* S$ between (non-unital non-associative semi)rings $R$ and $S$, and for any element $x \in R$, we have $f(x) = -1$ if and only if $x = -1$.

RingEquiv.toNonUnitalRingHom definition

(e : R ≃+* S) : R →ₙ+* S

Full source

/-- Reinterpret a ring equivalence as a non-unital ring homomorphism. -/
def toNonUnitalRingHom (e : R ≃+* S) : R →ₙ+* S :=
  { e.toMulEquiv.toMulHom, e.toAddEquiv.toAddMonoidHom with }

Non-unital ring homomorphism induced by a ring equivalence

Informal description

Given a ring equivalence (isomorphism) $e : R \simeq+* S$ between two (non-unital non-associative semi)rings, this function returns the corresponding non-unital ring homomorphism $R \to_{n+*} S$ by extracting the multiplicative and additive homomorphism components from $e$.

RingEquiv.toNonUnitalRingHom_injective theorem

: Function.Injective (toNonUnitalRingHom : R ≃+* S → R →ₙ+* S)

Full source

theorem toNonUnitalRingHom_injective :
    Function.Injective (toNonUnitalRingHom : R ≃+* S → R →ₙ+* S) := fun _ _ h =>
  RingEquiv.ext (NonUnitalRingHom.ext_iff.1 h)

Injectivity of the Ring Isomorphism to Non-Unital Ring Homomorphism Map

Informal description

The map from ring isomorphisms $R \simeq+* S$ to non-unital ring homomorphisms $R \to_{n+*} S$ is injective. In other words, if two ring isomorphisms induce the same non-unital ring homomorphism, then they must be equal.

RingEquiv.toNonUnitalRingHom_eq_coe theorem

(f : R ≃+* S) : f.toNonUnitalRingHom = ↑f

Full source

theorem toNonUnitalRingHom_eq_coe (f : R ≃+* S) : f.toNonUnitalRingHom = ↑f :=
  rfl

Equality of Induced Homomorphism and Underlying Function in Ring Isomorphism

Informal description

For any ring isomorphism $f : R \simeq+* S$ between non-unital non-associative semirings $R$ and $S$, the induced non-unital ring homomorphism $f.toNonUnitalRingHom$ is equal to the underlying function of $f$ (denoted by $\uparrow f$).

RingEquiv.coe_toNonUnitalRingHom theorem

(f : R ≃+* S) : ⇑(f : R →ₙ+* S) = f

Full source

@[simp, norm_cast]
theorem coe_toNonUnitalRingHom (f : R ≃+* S) : ⇑(f : R →ₙ+* S) = f :=
  rfl

Equality of Ring Equivalence and its Induced Non-Unital Ring Homomorphism

Informal description

For any ring equivalence $f : R \simeq+* S$ between non-unital non-associative semirings $R$ and $S$, the underlying function of the induced non-unital ring homomorphism $f : R \to_{ₙ+*} S$ is equal to $f$ itself as a function.

RingEquiv.coe_nonUnitalRingHom_inj_iff theorem

 {R S : Type*} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f g : R ≃+* S) : f = g ↔ (f : R →ₙ+* S) = g

Full source

theorem coe_nonUnitalRingHom_inj_iff {R S : Type*} [NonUnitalNonAssocSemiring R]
    [NonUnitalNonAssocSemiring S] (f g : R ≃+* S) : f = g ↔ (f : R →ₙ+* S) = g :=
  ⟨fun h => by rw [h], fun h => ext <| NonUnitalRingHom.ext_iff.mp h⟩

Equality of Ring Isomorphisms via Underlying Non-Unital Ring Homomorphisms

Informal description

For any two non-unital non-associative semirings $R$ and $S$, and any two ring isomorphisms $f, g: R \simeq+* S$, the following are equivalent: 1. The ring isomorphisms $f$ and $g$ are equal. 2. The underlying non-unital ring homomorphisms of $f$ and $g$ are equal.

RingEquiv.toNonUnitalRingHom_refl theorem

: (RingEquiv.refl R).toNonUnitalRingHom = NonUnitalRingHom.id R

Full source

@[simp]
theorem toNonUnitalRingHom_refl :
    (RingEquiv.refl R).toNonUnitalRingHom = NonUnitalRingHom.id R :=
  rfl

Identity Ring Isomorphism Induces Identity Non-Unital Ring Homomorphism

Informal description

For any non-unital non-associative semiring $R$, the non-unital ring homomorphism induced by the identity ring isomorphism $\text{refl}_R : R \simeq+* R$ is equal to the identity non-unital ring homomorphism on $R$.

RingEquiv.toNonUnitalRingHom_apply_symm_toNonUnitalRingHom_apply theorem

(e : R ≃+* S) : ∀ y : S, e.toNonUnitalRingHom (e.symm.toNonUnitalRingHom y) = y

Full source

@[simp]
theorem toNonUnitalRingHom_apply_symm_toNonUnitalRingHom_apply (e : R ≃+* S) :
    ∀ y : S, e.toNonUnitalRingHom (e.symm.toNonUnitalRingHom y) = y :=
  e.toEquiv.apply_symm_apply

Recovery of Element via Ring Isomorphism and its Inverse

Informal description

For any ring isomorphism $e : R \simeq+* S$ between non-unital non-associative semirings $R$ and $S$, and for any element $y \in S$, applying the non-unital ring homomorphism associated to $e$ to the image of $y$ under the non-unital ring homomorphism associated to $e^{-1}$ recovers $y$. In other words, $e(e^{-1}(y)) = y$ holds for the homomorphism components.

RingEquiv.symm_toNonUnitalRingHom_apply_toNonUnitalRingHom_apply theorem

(e : R ≃+* S) : ∀ x : R, e.symm.toNonUnitalRingHom (e.toNonUnitalRingHom x) = x

Full source

@[simp]
theorem symm_toNonUnitalRingHom_apply_toNonUnitalRingHom_apply (e : R ≃+* S) :
    ∀ x : R, e.symm.toNonUnitalRingHom (e.toNonUnitalRingHom x) = x :=
  Equiv.symm_apply_apply e.toEquiv

Inverse Ring Homomorphism Recovers Original Element

Informal description

For any ring isomorphism $e : R \simeq+* S$ between (non-unital non-associative semi)rings $R$ and $S$, and for any element $x \in R$, applying the inverse homomorphism $e^{-1}$ to the image of $x$ under $e$ recovers $x$, i.e., $e^{-1}(e(x)) = x$.

RingEquiv.toNonUnitalRingHom_trans theorem

 (e₁ : R ≃+* S) (e₂ : S ≃+* S') : (e₁.trans e₂).toNonUnitalRingHom = e₂.toNonUnitalRingHom.comp e₁.toNonUnitalRingHom

Full source

@[simp]
theorem toNonUnitalRingHom_trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
    (e₁.trans e₂).toNonUnitalRingHom = e₂.toNonUnitalRingHom.comp e₁.toNonUnitalRingHom :=
  rfl

Compatibility of Ring Equivalence Composition with Non-Unital Ring Homomorphism Construction

Informal description

For any ring equivalences (isomorphisms) $e_1: R \simeq^{+*} S$ and $e_2: S \simeq^{+*} S'$, the non-unital ring homomorphism induced by their composition $e_1 \circ e_2$ equals the composition of the induced non-unital ring homomorphisms, i.e., $(e_1 \circ e_2).\text{toNonUnitalRingHom} = e_2.\text{toNonUnitalRingHom} \circ e_1.\text{toNonUnitalRingHom}$.

RingEquiv.toNonUnitalRingHomm_comp_symm_toNonUnitalRingHom theorem

(e : R ≃+* S) : e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom = NonUnitalRingHom.id _

Full source

@[simp]
theorem toNonUnitalRingHomm_comp_symm_toNonUnitalRingHom (e : R ≃+* S) :
    e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom = NonUnitalRingHom.id _ := by
  ext
  simp

Composition of Ring Isomorphism with its Inverse Yields Identity

Informal description

For any ring isomorphism $e \colon R \simeq^{+*} S$ between non-unital non-associative semirings $R$ and $S$, the composition of the induced non-unital ring homomorphism $e$ with its inverse homomorphism $e^{-1}$ equals the identity homomorphism on $S$, i.e., $e \circ e^{-1} = \text{id}_S$.

RingEquiv.symm_toNonUnitalRingHom_comp_toNonUnitalRingHom theorem

(e : R ≃+* S) : e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom = NonUnitalRingHom.id _

Full source

@[simp]
theorem symm_toNonUnitalRingHom_comp_toNonUnitalRingHom (e : R ≃+* S) :
    e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom = NonUnitalRingHom.id _ := by
  ext
  simp

Inverse Composition Yields Identity Homomorphism for Ring Isomorphisms

Informal description

For any ring isomorphism $e \colon R \simeq^{+*} S$ between (non-unital non-associative semi)rings $R$ and $S$, the composition of the induced non-unital ring homomorphism $e \colon R \to_{n+*} S$ with its inverse $e^{-1} \colon S \to_{n+*} R$ equals the identity homomorphism on $R$, i.e., $e^{-1} \circ e = \text{id}_R$.

RingEquiv.toRingHom definition

(e : R ≃+* S) : R →+* S

Full source

/-- Reinterpret a ring equivalence as a ring homomorphism. -/
def toRingHom (e : R ≃+* S) : R →+* S :=
  { e.toMulEquiv.toMonoidHom, e.toAddEquiv.toAddMonoidHom with }

Conversion of ring equivalence to ring homomorphism

Informal description

Given a ring equivalence (isomorphism) $e \colon R \simeq^{+*} S$ between (semi)rings $R$ and $S$, the function `RingEquiv.toRingHom` converts $e$ into a ring homomorphism $R \to^{+*} S$ that preserves both the multiplicative and additive structures. Specifically, for any $x, y \in R$, the homomorphism satisfies: - $e(x + y) = e(x) + e(y)$ (additive structure preservation) - $e(x \cdot y) = e(x) \cdot e(y)$ (multiplicative structure preservation) - $e(1) = 1$ (multiplicative identity preservation) - $e(0) = 0$ (additive identity preservation)

RingEquiv.toRingHom_injective theorem

: Function.Injective (toRingHom : R ≃+* S → R →+* S)

Full source

theorem toRingHom_injective : Function.Injective (toRingHom : R ≃+* S → R →+* S) := fun _ _ h =>
  RingEquiv.ext (RingHom.ext_iff.1 h)

Injectivity of the Ring Equivalence to Ring Homomorphism Conversion

Informal description

The function that converts a ring equivalence (isomorphism) $f \colon R \simeq^{+*} S$ between non-associative semirings $R$ and $S$ into a ring homomorphism $R \to^{+*} S$ is injective. In other words, if two ring equivalences induce the same ring homomorphism, then they must be equal.

RingEquiv.toRingHom_eq_coe theorem

(f : R ≃+* S) : f.toRingHom = ↑f

Full source

@[simp] theorem toRingHom_eq_coe (f : R ≃+* S) : f.toRingHom = ↑f :=
  rfl

Ring isomorphism's homomorphism equals its coercion

Informal description

For any ring isomorphism $f \colon R \simeq^{+*} S$ between non-associative semirings $R$ and $S$, the associated ring homomorphism $f.toRingHom$ is equal to the coercion of $f$ to a ring homomorphism (denoted $\uparrow f$).

RingEquiv.coe_toRingHom theorem

(f : R ≃+* S) : ⇑(f : R →+* S) = f

Full source

@[simp, norm_cast]
theorem coe_toRingHom (f : R ≃+* S) : ⇑(f : R →+* S) = f :=
  rfl

Ring equivalence and ring homomorphism functions coincide

Informal description

For any ring equivalence $f : R \simeq+* S$ between two non-associative semirings $R$ and $S$, the underlying function of the associated ring homomorphism $f : R \to+* S$ is equal to the underlying function of $f$ itself.

RingEquiv.coe_ringHom_inj_iff theorem

{R S : Type*} [NonAssocSemiring R] [NonAssocSemiring S] (f g : R ≃+* S) : f = g ↔ (f : R →+* S) = g

Full source

theorem coe_ringHom_inj_iff {R S : Type*} [NonAssocSemiring R] [NonAssocSemiring S]
    (f g : R ≃+* S) : f = g ↔ (f : R →+* S) = g :=
  ⟨fun h => by rw [h], fun h => ext <| RingHom.ext_iff.mp h⟩

Equality of Ring Isomorphisms via Underlying Homomorphisms

Informal description

For any two non-associative semirings $R$ and $S$, and any two ring isomorphisms $f, g : R \simeq+* S$, the following are equivalent: 1. The ring isomorphisms $f$ and $g$ are equal. 2. The underlying ring homomorphisms of $f$ and $g$ are equal. In other words, $f = g$ if and only if their corresponding ring homomorphisms are equal.

RingEquiv.toNonUnitalRingHom_commutes theorem

(f : R ≃+* S) : ((f : R →+* S) : R →ₙ+* S) = (f : R →ₙ+* S)

Full source

/-- The two paths coercion can take to a `NonUnitalRingEquiv` are equivalent -/
@[simp, norm_cast]
theorem toNonUnitalRingHom_commutes (f : R ≃+* S) :
    ((f : R →+* S) : R →ₙ+* S) = (f : R →ₙ+* S) :=
  rfl

Commutativity of Coercion Paths to Non-Unital Ring Homomorphism for Ring Equivalences

Informal description

For any ring equivalence $f : R \simeq+* S$ between non-associative semirings $R$ and $S$, the coercion of $f$ to a non-unital ring homomorphism via the ring homomorphism path $((f : R \to+* S) : R \to_{n}+* S)$ is equal to the direct coercion of $f$ to a non-unital ring homomorphism $(f : R \to_{n}+* S)$.

RingEquiv.toMonoidHom abbrev

(e : R ≃+* S) : R →* S

Full source

/-- Reinterpret a ring equivalence as a monoid homomorphism. -/
abbrev toMonoidHom (e : R ≃+* S) : R →* S :=
  e.toRingHom.toMonoidHom

Conversion of Ring Isomorphism to Monoid Homomorphism

Informal description

Given a ring equivalence (isomorphism) $e \colon R \simeq^{+*} S$ between (semi)rings $R$ and $S$, the function `RingEquiv.toMonoidHom` converts $e$ into a monoid homomorphism $R \to^{*} S$ that preserves the multiplicative structure. Specifically, for any $x, y \in R$, the homomorphism satisfies: - $e(x \cdot y) = e(x) \cdot e(y)$ (multiplicative structure preservation) - $e(1) = 1$ (multiplicative identity preservation)

RingEquiv.toAddMonoidHom abbrev

(e : R ≃+* S) : R →+ S

Full source

/-- Reinterpret a ring equivalence as an `AddMonoid` homomorphism. -/
abbrev toAddMonoidHom (e : R ≃+* S) : R →+ S :=
  e.toRingHom.toAddMonoidHom

Conversion of Ring Equivalence to Additive Monoid Homomorphism

Informal description

Given a ring equivalence (isomorphism) $e \colon R \simeq^{+*} S$ between (semi)rings $R$ and $S$, the function `RingEquiv.toAddMonoidHom` converts $e$ into an additive monoid homomorphism $R \to^{+} S$ that preserves the additive structure. Specifically, for any $x, y \in R$, the homomorphism satisfies: - $e(0) = 0$ (preservation of zero) - $e(x + y) = e(x) + e(y)$ (preservation of addition)

RingEquiv.toAddMonoidMom_commutes theorem

(f : R ≃+* S) : (f : R →+* S).toAddMonoidHom = (f : R ≃+ S).toAddMonoidHom

Full source

/-- The two paths coercion can take to an `AddMonoidHom` are equivalent -/
theorem toAddMonoidMom_commutes (f : R ≃+* S) :
    (f : R →+* S).toAddMonoidHom = (f : R ≃+ S).toAddMonoidHom :=
  rfl

Compatibility of Additive Monoid Homomorphism Paths in Ring Equivalence

Informal description

For any ring equivalence $f : R \simeq+* S$ between (semi)rings $R$ and $S$, the additive monoid homomorphism obtained by viewing $f$ as a ring homomorphism ($R \to+* S$) is equal to the additive monoid homomorphism obtained by viewing $f$ as an additive equivalence ($R \simeq+ S$).

RingEquiv.toMonoidHom_commutes theorem

(f : R ≃+* S) : (f : R →+* S).toMonoidHom = (f : R ≃* S).toMonoidHom

Full source

/-- The two paths coercion can take to a `MonoidHom` are equivalent -/
theorem toMonoidHom_commutes (f : R ≃+* S) :
    (f : R →+* S).toMonoidHom = (f : R ≃* S).toMonoidHom :=
  rfl

Equality of Monoid Homomorphisms Induced by Ring Equivalence

Informal description

For any ring equivalence $f \colon R \simeq+* S$ between (semi)rings $R$ and $S$, the monoid homomorphism obtained by viewing $f$ as a ring homomorphism ($f \colon R \to+* S$) is equal to the monoid homomorphism obtained by viewing $f$ as a multiplicative equivalence ($f \colon R \simeq* S$).

RingEquiv.toEquiv_commutes theorem

(f : R ≃+* S) : (f : R ≃+ S).toEquiv = (f : R ≃* S).toEquiv

Full source

/-- The two paths coercion can take to an `Equiv` are equivalent -/
theorem toEquiv_commutes (f : R ≃+* S) : (f : R ≃+ S).toEquiv = (f : R ≃* S).toEquiv :=
  rfl

Equality of Underlying Bijections in Ring Equivalence

Informal description

For any ring equivalence $f : R \simeq+* S$ between (semi)rings $R$ and $S$, the underlying bijection obtained by viewing $f$ as an additive equivalence ($R \simeq+ S$) is equal to the underlying bijection obtained by viewing $f$ as a multiplicative equivalence ($R \simeq* S$).

RingEquiv.toRingHom_refl theorem

: (RingEquiv.refl R).toRingHom = RingHom.id R

Full source

@[simp]
theorem toRingHom_refl : (RingEquiv.refl R).toRingHom = RingHom.id R :=
  rfl

Identity Ring Isomorphism Yields Identity Ring Homomorphism

Informal description

For any (semi)ring $R$, the ring homomorphism obtained from the identity ring isomorphism $\text{refl} \colon R \simeq^{+*} R$ is equal to the identity ring homomorphism $\text{id} \colon R \to^{+*} R$.

RingEquiv.toMonoidHom_refl theorem

: (RingEquiv.refl R).toMonoidHom = MonoidHom.id R

Full source

@[simp]
theorem toMonoidHom_refl : (RingEquiv.refl R).toMonoidHom = MonoidHom.id R :=
  rfl

Identity Ring Isomorphism Yields Identity Monoid Homomorphism

Informal description

The monoid homomorphism associated with the identity ring isomorphism $\text{refl} \colon R \simeq^{+*} R$ is equal to the identity monoid homomorphism $\text{id} \colon R \to^{*} R$.

RingEquiv.toAddMonoidHom_refl theorem

: (RingEquiv.refl R).toAddMonoidHom = AddMonoidHom.id R

Full source

@[simp]
theorem toAddMonoidHom_refl : (RingEquiv.refl R).toAddMonoidHom = AddMonoidHom.id R :=
  rfl

Identity Ring Isomorphism Yields Identity Additive Monoid Homomorphism

Informal description

For any (semi)ring $R$, the additive monoid homomorphism obtained from the identity ring isomorphism $\text{refl} \colon R \simeq^{+*} R$ is equal to the identity additive monoid homomorphism $\text{id} \colon R \to^{+} R$.

RingEquiv.toRingHom_apply_symm_toRingHom_apply theorem

(e : R ≃+* S) : ∀ y : S, e.toRingHom (e.symm.toRingHom y) = y

Full source

theorem toRingHom_apply_symm_toRingHom_apply (e : R ≃+* S) :
    ∀ y : S, e.toRingHom (e.symm.toRingHom y) = y :=
  e.toEquiv.apply_symm_apply

Recovery of Element via Ring Isomorphism and its Inverse

Informal description

For any ring isomorphism $e \colon R \simeq^{+*} S$ between (semi)rings $R$ and $S$, and for any element $y \in S$, applying the ring homomorphism associated with $e$ to the image of $y$ under the ring homomorphism associated with the inverse isomorphism $e^{-1}$ recovers $y$. In other words, $e(e^{-1}(y)) = y$ where $e$ and $e^{-1}$ are viewed as ring homomorphisms.

RingEquiv.symm_toRingHom_apply_toRingHom_apply theorem

(e : R ≃+* S) : ∀ x : R, e.symm.toRingHom (e.toRingHom x) = x

Full source

theorem symm_toRingHom_apply_toRingHom_apply (e : R ≃+* S) :
    ∀ x : R, e.symm.toRingHom (e.toRingHom x) = x :=
  Equiv.symm_apply_apply e.toEquiv

Inverse Ring Homomorphism Recovers Original Element

Informal description

For any ring isomorphism $e \colon R \simeq^{+*} S$ between (semi)rings $R$ and $S$, and for any element $x \in R$, applying the inverse ring homomorphism $e^{-1}$ to the image $e(x)$ recovers the original element $x$, i.e., $e^{-1}(e(x)) = x$.

RingEquiv.toRingHom_trans theorem

(e₁ : R ≃+* S) (e₂ : S ≃+* S') : (e₁.trans e₂).toRingHom = e₂.toRingHom.comp e₁.toRingHom

Full source

@[simp]
theorem toRingHom_trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
    (e₁.trans e₂).toRingHom = e₂.toRingHom.comp e₁.toRingHom :=
  rfl

Composition of Ring Homomorphisms via Ring Equivalences

Informal description

Let $R$, $S$, and $S'$ be (non-unital non-associative semi)rings, and let $e_1: R \simeq^{+*} S$ and $e_2: S \simeq^{+*} S'$ be ring equivalences. Then the ring homomorphism associated with the composition $e_2 \circ e_1$ equals the composition of the ring homomorphisms associated with $e_2$ and $e_1$, i.e., $$(e_1 \circ e_2).\text{toRingHom} = e_2.\text{toRingHom} \circ e_1.\text{toRingHom}.$$

RingEquiv.toRingHom_comp_symm_toRingHom theorem

(e : R ≃+* S) : e.toRingHom.comp e.symm.toRingHom = RingHom.id _

Full source

theorem toRingHom_comp_symm_toRingHom (e : R ≃+* S) :
    e.toRingHom.comp e.symm.toRingHom = RingHom.id _ := by
  ext
  simp

Composition of Ring Isomorphism with Its Inverse Yields Identity on Codomain

Informal description

For any ring isomorphism $e \colon R \simeq^{+*} S$ between (non-associative) semirings $R$ and $S$, the composition of the ring homomorphism $e \colon R \to^{+*} S$ with its inverse $e^{-1} \colon S \to^{+*} R$ equals the identity ring homomorphism on $S$, i.e., $$e \circ e^{-1} = \text{id}_S.$$

RingEquiv.symm_toRingHom_comp_toRingHom theorem

(e : R ≃+* S) : e.symm.toRingHom.comp e.toRingHom = RingHom.id _

Full source

theorem symm_toRingHom_comp_toRingHom (e : R ≃+* S) :
    e.symm.toRingHom.comp e.toRingHom = RingHom.id _ := by
  ext
  simp

Inverse Ring Isomorphism Composes to Identity on $S$

Informal description

For any ring isomorphism $e \colon R \simeq^{+*} S$ between (semi)rings $R$ and $S$, the composition of the ring homomorphism associated to $e$ with the ring homomorphism associated to its inverse $e^{-1}$ is equal to the identity ring homomorphism on $S$, i.e., $$(e^{-1})_{\text{ring}} \circ e_{\text{ring}} = \text{id}_S.$$

RingEquiv.ofHomInv' definition

 {R S F G : Type*} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [FunLike F R S] [FunLike G S R]
  [NonUnitalRingHomClass F R S] [NonUnitalRingHomClass G S R] (hom : F) (inv : G)
  (hom_inv_id : (inv : S →ₙ+* R).comp (hom : R →ₙ+* S) = NonUnitalRingHom.id R)
  (inv_hom_id : (hom : R →ₙ+* S).comp (inv : S →ₙ+* R) = NonUnitalRingHom.id S) : R ≃+* S

Full source

/-- Construct an equivalence of rings from homomorphisms in both directions, which are inverses.
-/
@[simps]
def ofHomInv' {R S F G : Type*} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S]
    [FunLike F R S] [FunLike G S R]
    [NonUnitalRingHomClass F R S] [NonUnitalRingHomClass G S R] (hom : F) (inv : G)
    (hom_inv_id : (inv : S →ₙ+* R).comp (hom : R →ₙ+* S) = NonUnitalRingHom.id R)
    (inv_hom_id : (hom : R →ₙ+* S).comp (inv : S →ₙ+* R) = NonUnitalRingHom.id S) :
    R ≃+* S where
  toFun := hom
  invFun := inv
  left_inv := DFunLike.congr_fun hom_inv_id
  right_inv := DFunLike.congr_fun inv_hom_id
  map_mul' := map_mul hom
  map_add' := map_add hom

Ring equivalence from inverse non-unital ring homomorphisms

Informal description

Given non-unital non-associative semirings $ R $ and $ S $, and types $ F $ and $ G $ of non-unital ring homomorphisms between them, if $ \text{hom} : F $ and $ \text{inv} : G $ are homomorphisms that are inverses of each other (i.e., their compositions in both directions yield the identity homomorphism), then they induce a ring equivalence $ R \simeq+* S $. More precisely, if: 1. $ \text{inv} \circ \text{hom} = \text{id}_R $ (as non-unital ring homomorphisms) 2. $ \text{hom} \circ \text{inv} = \text{id}_S $ (as non-unital ring homomorphisms) then there exists a ring equivalence $ e : R \simeq+* S $ where: - The forward map $ e $ is $ \text{hom} $ - The inverse map $ e^{-1} $ is $ \text{inv} $ - Both maps preserve addition and multiplication

RingEquiv.ofHomInv definition

 {R S F G : Type*} [NonAssocSemiring R] [NonAssocSemiring S] [FunLike F R S] [FunLike G S R] [RingHomClass F R S]
  [RingHomClass G S R] (hom : F) (inv : G) (hom_inv_id : (inv : S →+* R).comp (hom : R →+* S) = RingHom.id R)
  (inv_hom_id : (hom : R →+* S).comp (inv : S →+* R) = RingHom.id S) : R ≃+* S

Full source

/--
Construct an equivalence of rings from unital homomorphisms in both directions, which are inverses.
-/
@[simps]
def ofHomInv {R S F G : Type*} [NonAssocSemiring R] [NonAssocSemiring S]
    [FunLike F R S] [FunLike G S R] [RingHomClass F R S]
    [RingHomClass G S R] (hom : F) (inv : G)
    (hom_inv_id : (inv : S →+* R).comp (hom : R →+* S) = RingHom.id R)
    (inv_hom_id : (hom : R →+* S).comp (inv : S →+* R) = RingHom.id S) :
    R ≃+* S where
  toFun := hom
  invFun := inv
  left_inv := DFunLike.congr_fun hom_inv_id
  right_inv := DFunLike.congr_fun inv_hom_id
  map_mul' := map_mul hom
  map_add' := map_add hom

Ring equivalence from inverse ring homomorphisms

Informal description

Given two non-associative semirings $ R $ and $ S $, and two types $ F $ and $ G $ of ring homomorphisms between them, if $ \text{hom} : F $ and $ \text{inv} : G $ are ring homomorphisms that are inverses of each other (i.e., their compositions in both directions yield the identity homomorphism), then they induce a ring equivalence $ R \simeq+* S $. More precisely, if: 1. $ \text{inv} \circ \text{hom} = \text{id}_R $ (as ring homomorphisms) 2. $ \text{hom} \circ \text{inv} = \text{id}_S $ (as ring homomorphisms) then there exists a ring equivalence $ e : R \simeq+* S $ where: - The forward map $ e $ is $ \text{hom} $ - The inverse map $ e^{-1} $ is $ \text{inv} $ - Both maps preserve addition and multiplication

RingEquiv.map_pow theorem

(f : R ≃+* S) (a) : ∀ n : ℕ, f (a ^ n) = f a ^ n

Full source

protected theorem map_pow (f : R ≃+* S) (a) : ∀ n : ℕ, f (a ^ n) = f a ^ n :=
  map_pow f a

Power Preservation under Ring Equivalences: $f(a^n) = f(a)^n$

Informal description

For any ring equivalence $f : R \simeq+* S$ between two (semi)rings $R$ and $S$, and for any element $a \in R$ and natural number $n$, the image of $a^n$ under $f$ equals the $n$-th power of $f(a)$, i.e., $f(a^n) = (f(a))^n$.

MulEquiv.toRingEquiv definition

 {R S F : Type*} [Add R] [Add S] [Mul R] [Mul S] [EquivLike F R S] [MulEquivClass F R S] (f : F)
  (H : ∀ x y : R, f (x + y) = f x + f y) : R ≃+* S

Full source

/-- Gives a `RingEquiv` from an element of a `MulEquivClass` preserving addition. -/
def toRingEquiv {R S F : Type*} [Add R] [Add S] [Mul R] [Mul S] [EquivLike F R S]
    [MulEquivClass F R S] (f : F)
    (H : ∀ x y : R, f (x + y) = f x + f y) : R ≃+* S :=
  { (f : R ≃* S).toEquiv, (f : R ≃* S), AddEquiv.mk' (f : R ≃* S).toEquiv H with }

Ring equivalence from multiplicative equivalence preserving addition

Informal description

Given types $ R $ and $ S $ equipped with addition and multiplication operations, and a type $ F $ satisfying `MulEquivClass F R S`, the function converts a multiplicative equivalence $ f : F $ into a ring equivalence $ R \simeq+* S $, provided that $ f $ also preserves addition. Specifically, for all $ x, y \in R $, the condition $ f(x + y) = f(x) + f(y) $ must hold. The resulting ring equivalence consists of: 1. A bijection between $ R $ and $ S $ (as an $ R \simeq S $), 2. A multiplicative homomorphism preserving multiplication (as an $ R \simeq^* S $), 3. An additive homomorphism preserving addition (as an $ R \simeq^+ S $).

AddEquiv.toRingEquiv definition

 {R S F : Type*} [Add R] [Add S] [Mul R] [Mul S] [EquivLike F R S] [AddEquivClass F R S] (f : F)
  (H : ∀ x y : R, f (x * y) = f x * f y) : R ≃+* S

Full source

/-- Gives a `RingEquiv` from an element of an `AddEquivClass` preserving addition. -/
def toRingEquiv {R S F : Type*} [Add R] [Add S] [Mul R] [Mul S] [EquivLike F R S]
    [AddEquivClass F R S] (f : F)
    (H : ∀ x y : R, f (x * y) = f x * f y) : R ≃+* S :=
  { (f : R ≃+ S).toEquiv, (f : R ≃+ S), MulEquiv.mk' (f : R ≃+ S).toEquiv H with }

Additive equivalence preserving multiplication yields ring equivalence

Informal description

Given an additive equivalence $f : R \to S$ between two (non-unital non-associative semi)rings $R$ and $S$, if $f$ also preserves multiplication (i.e., $f(x * y) = f(x) * f(y)$ for all $x, y \in R$), then $f$ can be extended to a ring equivalence between $R$ and $S$.

RingEquiv.self_trans_symm theorem

(e : R ≃+* S) : e.trans e.symm = RingEquiv.refl R

Full source

@[simp]
theorem self_trans_symm (e : R ≃+* S) : e.trans e.symm = RingEquiv.refl R :=
  ext e.left_inv

Composition of Ring Isomorphism with its Inverse Yields Identity

Informal description

For any ring isomorphism $e : R \simeq^{+*} S$ between (semi)rings $R$ and $S$, the composition of $e$ with its inverse $e^{-1}$ is equal to the identity isomorphism on $R$, i.e., $e \circ e^{-1} = \text{id}_R$.

RingEquiv.symm_trans_self theorem

(e : R ≃+* S) : e.symm.trans e = RingEquiv.refl S

Full source

@[simp]
theorem symm_trans_self (e : R ≃+* S) : e.symm.trans e = RingEquiv.refl S :=
  ext e.right_inv

Inverse-Then-Forward Composition Yields Identity on Target Ring

Informal description

For any ring isomorphism $e : R \simeq^{+*} S$ between (semi)rings $R$ and $S$, the composition of its inverse $e^{-1}$ with $e$ equals the identity isomorphism on $S$, i.e., $e^{-1} \circ e = \text{id}_S$.

RingEquiv.ofRingHom definition

(f : R →+* S) (g : S →+* R) (h₁ : f.comp g = RingHom.id S) (h₂ : g.comp f = RingHom.id R) : R ≃+* S

Full source

/-- If a ring homomorphism has an inverse, it is a ring isomorphism. -/
@[simps]
def ofRingHom (f : R →+* S) (g : S →+* R) (h₁ : f.comp g = RingHom.id S)
    (h₂ : g.comp f = RingHom.id R) : R ≃+* S :=
  { f with
    toFun := f
    invFun := g
    left_inv := RingHom.ext_iff.1 h₂
    right_inv := RingHom.ext_iff.1 h₁ }

Ring isomorphism from inverse ring homomorphisms

Informal description

Given two (semi)ring homomorphisms $f: R \to S$ and $g: S \to R$ such that $f \circ g$ is the identity on $S$ and $g \circ f$ is the identity on $R$, this constructs a (semi)ring isomorphism between $R$ and $S$ where $f$ is the forward map and $g$ is the inverse map.

RingEquiv.coe_ringHom_ofRingHom theorem

(f : R →+* S) (g : S →+* R) (h₁ h₂) : ofRingHom f g h₁ h₂ = f

Full source

theorem coe_ringHom_ofRingHom (f : R →+* S) (g : S →+* R) (h₁ h₂) : ofRingHom f g h₁ h₂ = f :=
  rfl

Ring equivalence from inverse homomorphisms equals forward homomorphism

Informal description

Given two (semi)ring homomorphisms $f: R \to S$ and $g: S \to R$ such that $f \circ g$ is the identity on $S$ and $g \circ f$ is the identity on $R$, the ring equivalence $\text{ofRingHom}\, f\, g\, h_1\, h_2$ is equal to $f$ when viewed as a ring homomorphism.

RingEquiv.ofRingHom_coe_ringHom theorem

(f : R ≃+* S) (g : S →+* R) (h₁ h₂) : ofRingHom (↑f) g h₁ h₂ = f

Full source

@[simp]
theorem ofRingHom_coe_ringHom (f : R ≃+* S) (g : S →+* R) (h₁ h₂) : ofRingHom (↑f) g h₁ h₂ = f :=
  ext fun _ ↦ rfl

Construction of Ring Isomorphism from Homomorphisms Recovers Original Isomorphism

Informal description

Let $R$ and $S$ be (semi)rings, and let $f : R \simeq+* S$ be a ring isomorphism. For any ring homomorphism $g : S \to R$ satisfying the conditions that $f \circ g$ is the identity on $S$ and $g \circ f$ is the identity on $R$, the ring isomorphism constructed via `ofRingHom` from the underlying ring homomorphism of $f$ and $g$ is equal to $f$ itself.

RingEquiv.ofRingHom_symm theorem

(f : R →+* S) (g : S →+* R) (h₁ h₂) : (ofRingHom f g h₁ h₂).symm = ofRingHom g f h₂ h₁

Full source

theorem ofRingHom_symm (f : R →+* S) (g : S →+* R) (h₁ h₂) :
    (ofRingHom f g h₁ h₂).symm = ofRingHom g f h₂ h₁ :=
  rfl

Inverse of Ring Isomorphism Constructed from Inverse Homomorphisms

Informal description

Given ring homomorphisms $f: R \to S$ and $g: S \to R$ such that $f \circ g = \text{id}_S$ and $g \circ f = \text{id}_R$, the inverse of the ring isomorphism $\text{ofRingHom}\,f\,g\,h_1\,h_2$ is equal to $\text{ofRingHom}\,g\,f\,h_2\,h_1$.

MulEquiv.noZeroDivisors theorem

{A : Type*} (B : Type*) [MulZeroClass A] [MulZeroClass B] [NoZeroDivisors B] (e : A ≃* B) : NoZeroDivisors A

Full source

/-- If two rings are isomorphic, and the second doesn't have zero divisors,
then so does the first. -/
protected theorem noZeroDivisors {A : Type*} (B : Type*) [MulZeroClass A] [MulZeroClass B]
    [NoZeroDivisors B] (e : A ≃* B) : NoZeroDivisors A :=
  e.injective.noZeroDivisors e (map_zero e) (map_mul e)

Multiplicative Isomorphism Preserves No-Zero-Divisors Property

Informal description

Let $A$ and $B$ be types equipped with multiplication and zero operations forming `MulZeroClass` structures. If there exists a multiplicative isomorphism $e : A \simeq^* B$ and $B$ has no zero divisors, then $A$ also has no zero divisors. That is, for any $x, y \in A$, if $x * y = 0$ then either $x = 0$ or $y = 0$.

MulEquiv.isDomain theorem

{A : Type*} (B : Type*) [Semiring A] [Semiring B] [IsDomain B] (e : A ≃* B) : IsDomain A

Full source

/-- If two rings are isomorphic, and the second is a domain, then so is the first. -/
protected theorem isDomain {A : Type*} (B : Type*) [Semiring A] [Semiring B] [IsDomain B]
    (e : A ≃* B) : IsDomain A :=
  { e.injective.isLeftCancelMulZero e (map_zero e) (map_mul e),
    e.injective.isRightCancelMulZero e (map_zero e) (map_mul e) with
    exists_pair_ne := ⟨e.symm 0, e.symm 1, e.symm.injective.ne zero_ne_one⟩ }

Multiplicative Isomorphism Preserves Domain Property

Informal description

Let $A$ and $B$ be semirings, and let $e : A \simeq^* B$ be a multiplicative isomorphism between them. If $B$ is a domain (i.e., a nontrivial semiring where multiplication by any nonzero element is cancellative on both sides), then $A$ is also a domain.

Mathlib.Algebra.Ring.Equiv

Notations

Implementation notes

Tags