Mathlib.Algebra.Algebra.Equiv

AlgEquiv structure

(R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [Semiring A] [Semiring B]
  [Algebra R A] [Algebra R B] extends A ≃ B, A ≃* B, A ≃+ B, A ≃+* B

Full source

/-- An equivalence of algebras (denoted as `A ≃ₐ[R] B`)
is an equivalence of rings commuting with the actions of scalars. -/
structure AlgEquiv (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [Semiring A] [Semiring B]
  [Algebra R A] [Algebra R B] extends A ≃ B, A ≃* B, A ≃+ B, A ≃+* B where
  /-- An equivalence of algebras commutes with the action of scalars. -/
  protected commutes' : ∀ r : R, toFun (algebraMap R A r) = algebraMap R B r

$R$-algebra isomorphism

Informal description

An $R$-algebra isomorphism between two $R$-algebras $A$ and $B$ is a bijective map that preserves both the ring structure (addition and multiplication) and the scalar multiplication by elements of $R$. More precisely, an $R$-algebra isomorphism is a bijection $f: A \to B$ such that: - $f$ is a ring homomorphism (i.e., $f(x + y) = f(x) + f(y)$ and $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in A$) - $f$ preserves the scalar multiplication (i.e., $f(r \cdot x) = r \cdot f(x)$ for all $r \in R$ and $x \in A$) This structure extends the notions of bijective maps, multiplicative homomorphisms, additive homomorphisms, and ring homomorphisms between $A$ and $B$.

term_≃ₐ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:50 A " ≃ₐ[" R "] " A' => AlgEquiv R A A'

$ R $-algebra isomorphism notation

Informal description

The notation $ A \simeqₐ[R] A' $ denotes the type of $ R $-algebra isomorphisms between $ A $ and $ A' $, i.e., bijective $ R $-algebra homomorphisms that preserve both the ring and module structures over $ R $.

AlgEquivClass structure

(F : Type*) (R A B : outParam Type*) [CommSemiring R] [Semiring A]
    [Semiring B] [Algebra R A] [Algebra R B] [EquivLike F A B] : Prop
    extends RingEquivClass F A B

Full source

/-- `AlgEquivClass F R A B` states that `F` is a type of algebra structure preserving
  equivalences. You should extend this class when you extend `AlgEquiv`. -/
class AlgEquivClass (F : Type*) (R A B : outParam Type*) [CommSemiring R] [Semiring A]
    [Semiring B] [Algebra R A] [Algebra R B] [EquivLike F A B] : Prop
    extends RingEquivClass F A B where
  /-- An equivalence of algebras commutes with the action of scalars. -/
  commutes : ∀ (f : F) (r : R), f (algebraMap R A r) = algebraMap R B r

Algebra Equivalence Class

Informal description

The class `AlgEquivClass F R A B` states that `F` is a type of algebra structure preserving equivalences between `A` and `B`, where `R` is a commutative semiring and both `A` and `B` are semirings equipped with an `R`-algebra structure. This class extends `RingEquivClass` to include compatibility with the `R`-algebra structure, ensuring that the equivalence preserves scalar multiplication by elements of `R` in addition to the ring operations.

AlgEquivClass.toAlgHomClass instance

 (F R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [EquivLike F A B]
  [h : AlgEquivClass F R A B] : AlgHomClass F R A B

Full source

instance (priority := 100) toAlgHomClass (F R A B : Type*) [CommSemiring R] [Semiring A]
    [Semiring B] [Algebra R A] [Algebra R B] [EquivLike F A B] [h : AlgEquivClass F R A B] :
    AlgHomClass F R A B :=
  { h with }

$R$-Algebra Equivalences as $R$-Algebra Homomorphisms

Informal description

For any commutative semiring $R$ and semirings $A$ and $B$ equipped with $R$-algebra structures, if $F$ is a type of $R$-algebra equivalences between $A$ and $B$ (i.e., $F$ satisfies `AlgEquivClass F R A B`), then $F$ is also a type of $R$-algebra homomorphisms between $A$ and $B$ (i.e., $F$ satisfies `AlgHomClass F R A B`). This means that every $R$-algebra equivalence in $F$ preserves both the ring operations and the scalar multiplication by elements of $R$.

AlgEquivClass.toLinearEquivClass instance

 (F R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [EquivLike F A B]
  [h : AlgEquivClass F R A B] : LinearEquivClass F R A B

Full source

instance (priority := 100) toLinearEquivClass (F R A B : Type*) [CommSemiring R]
    [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
    [EquivLike F A B] [h : AlgEquivClass F R A B] : LinearEquivClass F R A B :=
  { h with map_smulₛₗ := fun f => map_smulₛₗ f }

$R$-Algebra Equivalences as $R$-Linear Equivalences

Informal description

For any commutative semiring $R$ and semirings $A$ and $B$ equipped with $R$-algebra structures, if $F$ is a type of $R$-algebra equivalences between $A$ and $B$ (i.e., $F$ satisfies `AlgEquivClass F R A B`), then $F$ is also a type of $R$-linear equivalences between $A$ and $B$ (i.e., $F$ satisfies `LinearEquivClass F R A B`). This means that every $R$-algebra equivalence in $F$ preserves both the additive structure and the scalar multiplication by elements of $R$.

AlgEquivClass.toAlgEquiv definition

 {F R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [EquivLike F A B]
  [AlgEquivClass F R A B] (f : F) : A ≃ₐ[R] B

Full source

/-- Turn an element of a type `F` satisfying `AlgEquivClass F R A B` into an actual `AlgEquiv`.
This is declared as the default coercion from `F` to `A ≃ₐ[R] B`. -/
@[coe]
def toAlgEquiv {F R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A]
    [Algebra R B] [EquivLike F A B] [AlgEquivClass F R A B] (f : F) : A ≃ₐ[R] B :=
  { (f : A ≃ B), (f : A ≃+* B) with commutes' := commutes f }

Conversion from algebra equivalence class to explicit algebra isomorphism

Informal description

Given a commutative semiring $R$ and semirings $A$, $B$ equipped with $R$-algebra structures, and a type $F$ satisfying `AlgEquivClass F R A B`, the function converts an element $f : F$ into an explicit $R$-algebra isomorphism $A \simeq_{alg[R]} B$. This isomorphism consists of: 1. A bijection between $A$ and $B$ (as an $A \simeq B$), 2. A ring isomorphism preserving both addition and multiplication (as an $A \simeq+* B$), 3. Compatibility with the $R$-algebra structure: $f(r \cdot x) = r \cdot f(x)$ for all $r \in R$ and $x \in A$.

AlgEquivClass.instCoeTCAlgEquiv instance

 (F R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [EquivLike F A B]
  [AlgEquivClass F R A B] : CoeTC F (A ≃ₐ[R] B)

Full source

instance (F R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
    [EquivLike F A B] [AlgEquivClass F R A B] : CoeTC F (A ≃ₐ[R] B) :=
  ⟨toAlgEquiv⟩

Canonical Coercion from Algebra Equivalence Class to Algebra Isomorphism

Informal description

For any commutative semiring $R$, semirings $A$ and $B$ equipped with $R$-algebra structures, and any type $F$ that satisfies `AlgEquivClass F R A B`, there is a canonical way to treat elements of $F$ as $R$-algebra isomorphisms from $A$ to $B$. This means any $f \in F$ can be coerced into an $R$-algebra isomorphism $A \simeq_{alg[R]} B$ that preserves the ring structure and scalar multiplication by elements of $R$.

AlgEquiv.instEquivLike instance

: EquivLike (A₁ ≃ₐ[R] A₂) A₁ A₂

Full source

instance : EquivLike (A₁ ≃ₐ[R] A₂) A₁ A₂ where
  coe f := f.toFun
  inv f := f.invFun
  left_inv f := f.left_inv
  right_inv f := f.right_inv
  coe_injective' f g h₁ h₂ := by
    obtain ⟨⟨f,_⟩,_⟩ := f
    obtain ⟨⟨g,_⟩,_⟩ := g
    congr

Equivalence-like Structure of R-Algebra Isomorphisms

Informal description

For any commutative semiring $R$ and semirings $A_1$, $A_2$ equipped with $R$-algebra structures, the type $A_1 \simeq_{alg[R]} A_2$ of $R$-algebra isomorphisms between $A_1$ and $A_2$ forms an equivalence-like class, meaning its elements can be injectively coerced to bijections between $A_1$ and $A_2$.

AlgEquiv.instFunLike instance

: FunLike (A₁ ≃ₐ[R] A₂) A₁ A₂

Full source

/-- Helper instance since the coercion is not always found. -/
instance : FunLike (A₁ ≃ₐ[R] A₂) A₁ A₂ where
  coe := DFunLike.coe
  coe_injective' := DFunLike.coe_injective'

Function-like Structure of R-Algebra Isomorphisms

Informal description

For any commutative semiring $R$ and semirings $A_1$, $A_2$ equipped with $R$-algebra structures, the type $A_1 \simeq_{alg[R]} A_2$ of $R$-algebra isomorphisms between $A_1$ and $A_2$ can be treated as a function-like type, meaning its elements can be coerced to functions from $A_1$ to $A_2$.

AlgEquiv.instAlgEquivClass instance

: AlgEquivClass (A₁ ≃ₐ[R] A₂) R A₁ A₂

Full source

instance : AlgEquivClass (A₁ ≃ₐ[R] A₂) R A₁ A₂ where
  map_add f := f.map_add'
  map_mul f := f.map_mul'
  commutes f := f.commutes'

$R$-Algebra Isomorphisms Form an Algebra Equivalence Class

Informal description

For any commutative semiring $R$ and semirings $A_1$, $A_2$ equipped with $R$-algebra structures, the type $A_1 \simeq_{alg[R]} A_2$ of $R$-algebra isomorphisms between $A_1$ and $A_2$ forms an algebra equivalence class. This means that any $R$-algebra isomorphism preserves both the ring structure and the scalar multiplication by elements of $R$.

AlgEquiv.ext theorem

{f g : A₁ ≃ₐ[R] A₂} (h : ∀ a, f a = g a) : f = g

Full source

@[ext]
theorem ext {f g : A₁ ≃ₐ[R] A₂} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

Extensionality of $R$-algebra isomorphisms

Informal description

For any two $R$-algebra isomorphisms $f, g: A_1 \simeq_{alg[R]} A_2$, if $f(a) = g(a)$ for all $a \in A_1$, then $f = g$.

AlgEquiv.congr_arg theorem

{f : A₁ ≃ₐ[R] A₂} {x x' : A₁} : x = x' → f x = f x'

Full source

protected theorem congr_arg {f : A₁ ≃ₐ[R] A₂} {x x' : A₁} : x = x' → f x = f x' :=
  DFunLike.congr_arg f

$R$-algebra isomorphism preserves equality: $x = x' \implies f(x) = f(x')$

Informal description

For any $R$-algebra isomorphism $f: A_1 \simeq_{alg[R]} A_2$ and elements $x, x' \in A_1$, if $x = x'$, then $f(x) = f(x')$.

AlgEquiv.congr_fun theorem

{f g : A₁ ≃ₐ[R] A₂} (h : f = g) (x : A₁) : f x = g x

Full source

protected theorem congr_fun {f g : A₁ ≃ₐ[R] A₂} (h : f = g) (x : A₁) : f x = g x :=
  DFunLike.congr_fun h x

Pointwise Equality of $R$-Algebra Isomorphisms

Informal description

For any two $R$-algebra isomorphisms $f, g: A_1 \simeq_{alg[R]} A_2$, if $f = g$, then for all $x \in A_1$, we have $f(x) = g(x)$.

AlgEquiv.coe_mk theorem

{toEquiv map_mul map_add commutes} : ⇑(⟨toEquiv, map_mul, map_add, commutes⟩ : A₁ ≃ₐ[R] A₂) = toEquiv

Full source

@[simp]
theorem coe_mk {toEquiv map_mul map_add commutes} :
    ⇑(⟨toEquiv, map_mul, map_add, commutes⟩ : A₁ ≃ₐ[R] A₂) = toEquiv :=
  rfl

Underlying Function of Constructed $R$-Algebra Isomorphism Equals Given Equivalence

Informal description

Let $R$ be a commutative semiring, and let $A_1$ and $A_2$ be semirings equipped with $R$-algebra structures. Given an equivalence $toEquiv : A_1 \simeq A_2$, a multiplicative homomorphism $map\_mul$, an additive homomorphism $map\_add$, and a scalar multiplication compatibility condition $commutes$, the underlying function of the constructed $R$-algebra isomorphism $\langle toEquiv, map\_mul, map\_add, commutes \rangle : A_1 \simeq_{alg[R]} A_2$ is equal to $toEquiv$.

AlgEquiv.mk_coe theorem

 (e : A₁ ≃ₐ[R] A₂) (e' h₁ h₂ h₃ h₄ h₅) : (⟨⟨e, e', h₁, h₂⟩, h₃, h₄, h₅⟩ : A₁ ≃ₐ[R] A₂) = e

Full source

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

Reconstruction of $R$-Algebra Isomorphism from Components Yields Original Isomorphism

Informal description

Given an $R$-algebra isomorphism $e: A_1 \simeq_{alg[R]} A_2$ and components $e'$, $h_1$, $h_2$, $h_3$, $h_4$, $h_5$ that reconstruct $e$, the constructed isomorphism $\langle \langle e, e', h_1, h_2 \rangle, h_3, h_4, h_5 \rangle$ is equal to $e$ itself.

AlgEquiv.toEquiv_eq_coe theorem

: e.toEquiv = e

Full source

@[simp]
theorem toEquiv_eq_coe : e.toEquiv = e :=
  rfl

Equality of Underlying Equivalence and $R$-Algebra Isomorphism

Informal description

For any $R$-algebra isomorphism $e : A \simeq_{alg[R]} B$, the underlying equivalence $e.\text{toEquiv}$ is equal to $e$ itself when viewed as a function.

AlgEquiv.coe_coe theorem

{F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) : ⇑(f : A₁ ≃ₐ[R] A₂) = f

Full source

@[simp]
protected theorem coe_coe {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) :
    ⇑(f : A₁ ≃ₐ[R] A₂) = f :=
  rfl

Equality of Coerced Algebra Isomorphism and Original Function

Informal description

For any type $F$ that is an instance of `EquivLike` and `AlgEquivClass` with commutative semiring $R$ and semirings $A₁$, $A₂$ equipped with $R$-algebra structures, the canonical map from $F$ to $A₁ ≃ₐ[R] A₂$ (when coerced to a function) equals the original element $f \in F$.

AlgEquiv.coe_fun_injective theorem

: @Function.Injective (A₁ ≃ₐ[R] A₂) (A₁ → A₂) fun e => (e : A₁ → A₂)

Full source

theorem coe_fun_injective : @Function.Injective (A₁ ≃ₐ[R] A₂) (A₁ → A₂) fun e => (e : A₁ → A₂) :=
  DFunLike.coe_injective

Injectivity of the Canonical Map from $R$-Algebra Isomorphisms to Functions

Informal description

The canonical map from the type of $R$-algebra isomorphisms $A_1 \simeq_{alg[R]} A_2$ to the type of functions $A_1 \to A_2$ is injective. That is, if two $R$-algebra isomorphisms $e_1, e_2 : A_1 \simeq_{alg[R]} A_2$ satisfy $(e_1 : A_1 \to A_2) = (e_2 : A_1 \to A_2)$, then $e_1 = e_2$.

AlgEquiv.hasCoeToRingEquiv instance

: CoeOut (A₁ ≃ₐ[R] A₂) (A₁ ≃+* A₂)

Full source

instance hasCoeToRingEquiv : CoeOut (A₁ ≃ₐ[R] A₂) (A₁ ≃+* A₂) :=
  ⟨AlgEquiv.toRingEquiv⟩

Coercion from $R$-algebra isomorphisms to ring isomorphisms

Informal description

Every $R$-algebra isomorphism $A_1 \simeq_{alg[R]} A_2$ can be coerced into a ring isomorphism $A_1 \simeq+* A_2$.

AlgEquiv.coe_toEquiv theorem

: ((e : A₁ ≃ A₂) : A₁ → A₂) = e

Full source

@[simp]
theorem coe_toEquiv : ((e : A₁ ≃ A₂) : A₁ → A₂) = e :=
  rfl

Coercion of $R$-algebra isomorphism to function via equivalence

Informal description

For any $R$-algebra isomorphism $e : A_1 \simeq_{alg[R]} A_2$, the underlying function $e : A_1 \to A_2$ coincides with the function obtained by coercing $e$ to an equivalence $A_1 \simeq A_2$ and then to a function $A_1 \to A_2$.

AlgEquiv.toRingEquiv_eq_coe theorem

: e.toRingEquiv = e

Full source

@[simp]
theorem toRingEquiv_eq_coe : e.toRingEquiv = e :=
  rfl

Equality of Underlying Ring Isomorphism and Coercion in $R$-Algebra Isomorphism

Informal description

For any $R$-algebra isomorphism $e : A_1 \simeq_{alg[R]} A_2$, the underlying ring isomorphism $e.toRingEquiv$ is equal to the coercion of $e$ to a ring isomorphism.

AlgEquiv.toRingEquiv_toRingHom theorem

: ((e : A₁ ≃+* A₂) : A₁ →+* A₂) = e

Full source

@[simp, norm_cast]
lemma toRingEquiv_toRingHom : ((e : A₁ ≃+* A₂) : A₁ →+* A₂) = e :=
  rfl

Equality of Ring Homomorphism from $R$-Algebra Isomorphism and Its Underlying Ring Equivalence

Informal description

For any $R$-algebra isomorphism $e : A_1 \simeq_{alg[R]} A_2$, the ring homomorphism obtained from the underlying ring equivalence of $e$ is equal to $e$ itself when viewed as a ring homomorphism.

AlgEquiv.coe_ringEquiv theorem

: ((e : A₁ ≃+* A₂) : A₁ → A₂) = e

Full source

@[simp, norm_cast]
theorem coe_ringEquiv : ((e : A₁ ≃+* A₂) : A₁ → A₂) = e :=
  rfl

Underlying Function Equality in $R$-Algebra Isomorphism and Ring Equivalence

Informal description

For any $R$-algebra isomorphism $e : A_1 \simeq_{alg[R]} A_2$, the underlying function of its associated ring equivalence $e : A_1 \simeq+* A_2$ is equal to $e$ itself as a function from $A_1$ to $A_2$.

AlgEquiv.coe_ringEquiv' theorem

: (e.toRingEquiv : A₁ → A₂) = e

Full source

theorem coe_ringEquiv' : (e.toRingEquiv : A₁ → A₂) = e :=
  rfl

Underlying Function of Ring Equivalence in $R$-Algebra Isomorphism

Informal description

For any $R$-algebra isomorphism $e : A_1 \simeq_{alg[R]} A_2$, the underlying function of its associated ring equivalence $e.toRingEquiv$ is equal to $e$ itself as a function from $A_1$ to $A_2$.

AlgEquiv.coe_ringEquiv_injective theorem

: Function.Injective ((↑) : (A₁ ≃ₐ[R] A₂) → A₁ ≃+* A₂)

Full source

theorem coe_ringEquiv_injective : Function.Injective ((↑) : (A₁ ≃ₐ[R] A₂) → A₁ ≃+* A₂) :=
  fun _ _ h => ext <| RingEquiv.congr_fun h

Injectivity of the Canonical Map from $R$-Algebra Isomorphisms to Ring Isomorphisms

Informal description

The canonical map from $R$-algebra isomorphisms $A_1 \simeq_{alg[R]} A_2$ to ring isomorphisms $A_1 \simeq+* A_2$ is injective. In other words, if two $R$-algebra isomorphisms induce the same ring isomorphism, then they must be equal as $R$-algebra isomorphisms.

AlgEquiv.toAlgHom definition

: A₁ →ₐ[R] A₂

Full source

/-- Interpret an algebra equivalence as an algebra homomorphism.

This definition is included for symmetry with the other `to*Hom` projections.
The `simp` normal form is to use the coercion of the `AlgHomClass.coeTC` instance. -/
@[coe]
def toAlgHom : A₁ →ₐ[R] A₂ :=
  { e with
    map_one' := map_one e
    map_zero' := map_zero e }

Underlying algebra homomorphism of an $R$-algebra isomorphism

Informal description

The function maps an $R$-algebra isomorphism $e: A_1 \simeq_{alg[R]} A_2$ to its underlying $R$-algebra homomorphism $e: A_1 \to_{alg[R]} A_2$, which preserves the multiplicative and additive structures as well as the scalar multiplication by elements of $R$.

AlgEquiv.toAlgHom_eq_coe theorem

: e.toAlgHom = e

Full source

@[simp]
theorem toAlgHom_eq_coe : e.toAlgHom = e :=
  rfl

Equality of Underlying Algebra Homomorphism and Isomorphism

Informal description

For any $R$-algebra isomorphism $e : A_1 \simeq_{alg[R]} A_2$, the underlying algebra homomorphism $e.toAlgHom$ is equal to $e$ itself when viewed as a function.

AlgEquiv.coe_algHom theorem

: DFunLike.coe (e.toAlgHom) = DFunLike.coe e

Full source

@[simp, norm_cast]
theorem coe_algHom : DFunLike.coe (e.toAlgHom) = DFunLike.coe e :=
  rfl

Equality of Underlying Functions in $R$-Algebra Isomorphism and its Homomorphism

Informal description

For any $R$-algebra isomorphism $e : A_1 \simeq_{alg[R]} A_2$, the underlying function of its associated algebra homomorphism $e.toAlgHom$ is equal to the underlying function of $e$ itself.

AlgEquiv.coe_algHom_injective theorem

: Function.Injective ((↑) : (A₁ ≃ₐ[R] A₂) → A₁ →ₐ[R] A₂)

Full source

theorem coe_algHom_injective : Function.Injective ((↑) : (A₁ ≃ₐ[R] A₂) → A₁ →ₐ[R] A₂) :=
  fun _ _ h => ext <| AlgHom.congr_fun h

Injectivity of the Canonical Map from $R$-Algebra Isomorphisms to $R$-Algebra Homomorphisms

Informal description

The canonical map from $R$-algebra isomorphisms between $A_1$ and $A_2$ to $R$-algebra homomorphisms is injective. In other words, if two $R$-algebra isomorphisms $f, g: A_1 \simeq_{alg[R]} A_2$ induce the same $R$-algebra homomorphism, then $f = g$.

AlgEquiv.toAlgHom_toRingHom theorem

: ((e : A₁ →ₐ[R] A₂) : A₁ →+* A₂) = e

Full source

@[simp, norm_cast]
lemma toAlgHom_toRingHom : ((e : A₁ →ₐ[R] A₂) : A₁ →+* A₂) = e :=
  rfl

Underlying Ring Homomorphism of Algebra Homomorphism from Algebra Isomorphism

Informal description

For any $R$-algebra isomorphism $e \colon A_1 \simeq_{alg[R]} A_2$, the underlying ring homomorphism of its associated algebra homomorphism is equal to $e$ itself when viewed as a ring homomorphism.

AlgEquiv.coe_ringHom_commutes theorem

: ((e : A₁ →ₐ[R] A₂) : A₁ →+* A₂) = ((e : A₁ ≃+* A₂) : A₁ →+* A₂)

Full source

/-- The two paths coercion can take to a `RingHom` are equivalent -/
theorem coe_ringHom_commutes : ((e : A₁ →ₐ[R] A₂) : A₁ →+* A₂) = ((e : A₁ ≃+* A₂) : A₁ →+* A₂) :=
  rfl

Equality of Ring Homomorphism Paths in $R$-Algebra Isomorphism Coercion

Informal description

For any $R$-algebra isomorphism $e \colon A_1 \simeq_{alg[R]} A_2$, the underlying ring homomorphism obtained by coercing $e$ as an $R$-algebra homomorphism is equal to the underlying ring homomorphism obtained by coercing $e$ as a ring isomorphism.

AlgEquiv.commutes theorem

: ∀ r : R, e (algebraMap R A₁ r) = algebraMap R A₂ r

Full source

@[simp]
theorem commutes : ∀ r : R, e (algebraMap R A₁ r) = algebraMap R A₂ r :=
  e.commutes'

$R$-algebra isomorphism commutes with scalar multiplication

Informal description

For any $R$-algebra isomorphism $e \colon A_1 \simeq_{alg[R]} A_2$ and any element $r \in R$, the isomorphism commutes with the algebra maps, i.e., $e(\iota_1(r)) = \iota_2(r)$, where $\iota_1 \colon R \to A_1$ and $\iota_2 \colon R \to A_2$ are the respective algebra structure maps.

AlgEquiv.bijective theorem

: Function.Bijective e

Full source

protected theorem bijective : Function.Bijective e :=
  EquivLike.bijective e

Bijectivity of $R$-algebra isomorphisms

Informal description

For any $R$-algebra isomorphism $e \colon A \simeq_{alg[R]} B$, the underlying function $e \colon A \to B$ is bijective.

AlgEquiv.injective theorem

: Function.Injective e

Full source

protected theorem injective : Function.Injective e :=
  EquivLike.injective e

Injectivity of $R$-algebra isomorphisms

Informal description

Every $R$-algebra isomorphism $e: A_1 \to A_2$ is injective.

AlgEquiv.surjective theorem

: Function.Surjective e

Full source

protected theorem surjective : Function.Surjective e :=
  EquivLike.surjective e

Surjectivity of $R$-algebra isomorphisms

Informal description

For any $R$-algebra isomorphism $e : A \simeq_{alg[R]} B$, the underlying function $e : A \to B$ is surjective.

AlgEquiv.refl definition

: A₁ ≃ₐ[R] A₁

Full source

/-- Algebra equivalences are reflexive. -/
@[refl]
def refl : A₁ ≃ₐ[R] A₁ :=
  { (.refl _ : A₁ ≃+* A₁) with commutes' := fun _ => rfl }

Identity $R$-algebra isomorphism

Informal description

The identity map is an $R$-algebra isomorphism from an $R$-algebra $A_1$ to itself, preserving both the ring structure and the scalar multiplication by elements of $R$.

AlgEquiv.instInhabited instance

: Inhabited (A₁ ≃ₐ[R] A₁)

Full source

instance : Inhabited (A₁ ≃ₐ[R] A₁) :=
  ⟨refl⟩

Inhabited Type of $R$-Algebra Automorphisms

Informal description

For any commutative semiring $R$ and $R$-algebra $A_1$, the type of $R$-algebra isomorphisms from $A_1$ to itself is inhabited, with the identity map as a canonical element.

AlgEquiv.refl_toAlgHom theorem

: ↑(refl : A₁ ≃ₐ[R] A₁) = AlgHom.id R A₁

Full source

@[simp]
theorem refl_toAlgHom : ↑(refl : A₁ ≃ₐ[R] A₁) = AlgHom.id R A₁ :=
  rfl

Identity $R$-Algebra Isomorphism Corresponds to Identity Algebra Homomorphism

Informal description

The identity $R$-algebra isomorphism $\text{refl} : A_1 \simeq_{alg[R]} A_1$ corresponds to the identity $R$-algebra homomorphism $\text{AlgHom.id}_R A_1$ when viewed as an algebra homomorphism.

AlgEquiv.coe_refl theorem

: ⇑(refl : A₁ ≃ₐ[R] A₁) = id

Full source

@[simp]
theorem coe_refl : ⇑(refl : A₁ ≃ₐ[R] A₁) = id :=
  rfl

Identity $R$-algebra isomorphism coincides with identity function

Informal description

The underlying function of the identity $R$-algebra isomorphism $\text{refl} : A_1 \simeq_{alg[R]} A_1$ is equal to the identity function $\text{id} : A_1 \to A_1$.

AlgEquiv.symm definition

(e : A₁ ≃ₐ[R] A₂) : A₂ ≃ₐ[R] A₁

Full source

/-- Algebra equivalences are symmetric. -/
@[symm]
def symm (e : A₁ ≃ₐ[R] A₂) : A₂ ≃ₐ[R] A₁ :=
  { e.toRingEquiv.symm with
    commutes' := fun r => by
      rw [← e.toRingEquiv.symm_apply_apply (algebraMap R A₁ r)]
      congr
      simp }

Inverse of an $R$-algebra isomorphism

Informal description

Given an $R$-algebra isomorphism $e : A_1 \simeq_{R} A_2$, the inverse map $e^{-1} : A_2 \simeq_{R} A_1$ is also an $R$-algebra isomorphism. This means that $e^{-1}$ preserves both the ring structure (addition and multiplication) and the scalar multiplication by elements of $R$.

AlgEquiv.invFun_eq_symm theorem

{e : A₁ ≃ₐ[R] A₂} : e.invFun = e.symm

Full source

theorem invFun_eq_symm {e : A₁ ≃ₐ[R] A₂} : e.invFun = e.symm :=
  rfl

Inverse Function of $R$-Algebra Isomorphism Equals Its Symmetric Counterpart

Informal description

For any $R$-algebra isomorphism $e: A_1 \simeq_{alg[R]} A_2$, the inverse function $e^{-1}$ (as a function) coincides with the inverse isomorphism $e.symm$.

AlgEquiv.coe_apply_coe_coe_symm_apply theorem

 {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) (x : A₂) : f ((f : A₁ ≃ₐ[R] A₂).symm x) = x

Full source

@[simp]
theorem coe_apply_coe_coe_symm_apply {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂]
    (f : F) (x : A₂) :
    f ((f : A₁ ≃ₐ[R] A₂).symm x) = x :=
  EquivLike.right_inv f x

Inverse Property of $R$-Algebra Isomorphisms: $f(f^{-1}(x)) = x$

Informal description

For any $R$-algebra isomorphism $f : A_1 \simeq_{alg[R]} A_2$ and any element $x \in A_2$, the application of $f$ to the inverse of $f$ evaluated at $x$ returns $x$, i.e., $f(f^{-1}(x)) = x$.

AlgEquiv.coe_coe_symm_apply_coe_apply theorem

 {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) (x : A₁) : (f : A₁ ≃ₐ[R] A₂).symm (f x) = x

Full source

@[simp]
theorem coe_coe_symm_apply_coe_apply {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂]
    (f : F) (x : A₁) :
    (f : A₁ ≃ₐ[R] A₂).symm (f x) = x :=
  EquivLike.left_inv f x

Inverse of $R$-algebra isomorphism cancels forward map

Informal description

Let $R$ be a commutative semiring, and let $A_1$ and $A_2$ be semirings equipped with $R$-algebra structures. Given an $R$-algebra isomorphism $f : A_1 \simeq_{alg[R]} A_2$ (represented as an element of a type $F$ with `AlgEquivClass F R A₁ A₂`), for any $x \in A_1$, the inverse isomorphism $f^{-1}$ satisfies $f^{-1}(f(x)) = x$.

AlgEquiv.symm_toEquiv_eq_symm theorem

{e : A₁ ≃ₐ[R] A₂} : (e : A₁ ≃ A₂).symm = e.symm

Full source

/-- `simp` normal form of `invFun_eq_symm` -/
@[simp]
theorem symm_toEquiv_eq_symm {e : A₁ ≃ₐ[R] A₂} : (e : A₁ ≃ A₂).symm = e.symm :=
  rfl

Inverse of Underlying Equivalence Equals Inverse Algebra Isomorphism

Informal description

For any $R$-algebra isomorphism $e : A_1 \simeq_{alg[R]} A_2$, the inverse of the underlying bijection $(e : A_1 \simeq A_2)^{-1}$ is equal to the inverse $R$-algebra isomorphism $e^{-1} : A_2 \simeq_{alg[R]} A_1$.

AlgEquiv.symm_symm theorem

(e : A₁ ≃ₐ[R] A₂) : e.symm.symm = e

Full source

@[simp]
theorem symm_symm (e : A₁ ≃ₐ[R] A₂) : e.symm.symm = e := rfl

Double Inverse of $R$-Algebra Isomorphism

Informal description

For any $R$-algebra isomorphism $e : A_1 \simeq_{R} A_2$, the double inverse $e^{-1}$ is equal to $e$ itself, i.e., $(e^{-1})^{-1} = e$.

AlgEquiv.symm_bijective theorem

: Function.Bijective (symm : (A₁ ≃ₐ[R] A₂) → A₂ ≃ₐ[R] A₁)

Full source

theorem symm_bijective : Function.Bijective (symm : (A₁ ≃ₐ[R] A₂) → A₂ ≃ₐ[R] A₁) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Bijectivity of the Inverse Map on $R$-Algebra Isomorphisms

Informal description

The map that sends an $R$-algebra isomorphism $e : A_1 \simeq_{R} A_2$ to its inverse $e^{-1} : A_2 \simeq_{R} A_1$ is bijective. That is: 1. The map is injective: if $e_1^{-1} = e_2^{-1}$ then $e_1 = e_2$. 2. The map is surjective: for every $R$-algebra isomorphism $f : A_2 \simeq_{R} A_1$, there exists an $R$-algebra isomorphism $e : A_1 \simeq_{R} A_2$ such that $e^{-1} = f$.

AlgEquiv.mk_coe' theorem

 (e : A₁ ≃ₐ[R] A₂) (f h₁ h₂ h₃ h₄ h₅) : (⟨⟨f, e, h₁, h₂⟩, h₃, h₄, h₅⟩ : A₂ ≃ₐ[R] A₁) = e.symm

Full source

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

Constructed Isomorphism Equals Inverse

Informal description

Given an $R$-algebra isomorphism $e : A_1 \simeq_{alg[R]} A_2$ and functions $f : A_2 \to A_1$, $h_1$, $h_2$, $h_3$, $h_4$, $h_5$ such that $\langle \langle f, e, h_1, h_2 \rangle, h_3, h_4, h_5 \rangle$ forms an $R$-algebra isomorphism from $A_2$ to $A_1$, then this constructed isomorphism is equal to the inverse $e^{-1} : A_2 \simeq_{alg[R]} A_1$ of $e$.

AlgEquiv.symm_mk.aux definition

(f f') (h₁ h₂ h₃ h₄ h₅)

Full source

/-- Auxiliary definition to avoid looping in `dsimp` with `AlgEquiv.symm_mk`. -/
protected def symm_mk.aux (f f') (h₁ h₂ h₃ h₄ h₅) :=
  (⟨⟨f, f', h₁, h₂⟩, h₃, h₄, h₅⟩ : A₁ ≃ₐ[R] A₂).symm

Auxiliary construction for inverse algebra isomorphism

Informal description

An auxiliary definition used to construct the inverse of an $R$-algebra isomorphism, ensuring that the `dsimp` tactic does not enter an infinite loop when simplifying expressions involving `AlgEquiv.symm_mk`. Given: - A commutative semiring $R$ - Semirings $A_1$ and $A_2$ with $R$-algebra structures - Functions $f: A_1 \to A_2$ and $f': A_2 \to A_1$ that are mutual inverses (i.e., $f \circ f' = \text{id}$ and $f' \circ f = \text{id}$) - Proofs that $f$ preserves addition, multiplication, scalar multiplication, and the multiplicative identity This definition constructs the inverse isomorphism $A_2 \simeq_{R} A_1$ from the given data.

AlgEquiv.symm_mk theorem

 (f f') (h₁ h₂ h₃ h₄ h₅) :
  (⟨⟨f, f', h₁, h₂⟩, h₃, h₄, h₅⟩ : A₁ ≃ₐ[R] A₂).symm =
    { symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅ with
      toFun := f'
      invFun := f }

Full source

@[simp]
theorem symm_mk (f f') (h₁ h₂ h₃ h₄ h₅) :
    (⟨⟨f, f', h₁, h₂⟩, h₃, h₄, h₅⟩ : A₁ ≃ₐ[R] A₂).symm =
      { symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅ with
        toFun := f'
        invFun := f } :=
  rfl

Inverse Construction for $R$-Algebra Isomorphism via Mutual Inverses

Informal description

Given a commutative semiring $R$ and two $R$-algebras $A_1$ and $A_2$, let $f: A_1 \to A_2$ and $f': A_2 \to A_1$ be mutually inverse functions (i.e., $f \circ f' = \text{id}$ and $f' \circ f = \text{id}$) that preserve addition, multiplication, scalar multiplication, and the multiplicative identity. Then, the inverse of the $R$-algebra isomorphism $\langle f, f', h_1, h_2, h_3, h_4, h_5 \rangle : A_1 \simeq_{alg[R]} A_2$ is equal to the $R$-algebra isomorphism constructed from $f'$ and $f$ with the corresponding preservation properties.

AlgEquiv.refl_symm theorem

: (AlgEquiv.refl : A₁ ≃ₐ[R] A₁).symm = AlgEquiv.refl

Full source

@[simp]
theorem refl_symm : (AlgEquiv.refl : A₁ ≃ₐ[R] A₁).symm = AlgEquiv.refl :=
  rfl

Inverse of Identity $R$-Algebra Isomorphism is Identity

Informal description

The inverse of the identity $R$-algebra isomorphism from $A_1$ to itself is equal to the identity isomorphism.

AlgEquiv.toRingEquiv_symm theorem

(f : A₁ ≃ₐ[R] A₁) : (f : A₁ ≃+* A₁).symm = f.symm

Full source

theorem toRingEquiv_symm (f : A₁ ≃ₐ[R] A₁) : (f : A₁ ≃+* A₁).symm = f.symm :=
  rfl

Inverse of Coerced Algebra Isomorphism Equals Algebra Inverse

Informal description

For any $R$-algebra isomorphism $f: A_1 \simeq_{alg[R]} A_1$, the inverse of $f$ considered as a ring isomorphism (via the coercion to $\simeq+*$) equals the inverse of $f$ as an $R$-algebra isomorphism.

AlgEquiv.symm_toRingEquiv theorem

: (e.symm : A₂ ≃+* A₁) = (e : A₁ ≃+* A₂).symm

Full source

@[simp]
theorem symm_toRingEquiv : (e.symm : A₂ ≃+* A₁) = (e : A₁ ≃+* A₂).symm :=
  rfl

Compatibility of Inverse with Underlying Ring Isomorphism in $R$-Algebra Isomorphisms

Informal description

For any $R$-algebra isomorphism $e: A_1 \simeq_{alg[R]} A_2$, the underlying ring isomorphism of its inverse $e^{-1}: A_2 \simeq_{alg[R]} A_1$ is equal to the inverse of the underlying ring isomorphism of $e$. In symbols, if we denote the underlying ring isomorphism of $e$ as $\tilde{e}: A_1 \simeq_{+*} A_2$, then $\widetilde{e^{-1}} = \tilde{e}^{-1}$.

AlgEquiv.symm_toAddEquiv theorem

: (e.symm : A₂ ≃+ A₁) = (e : A₁ ≃+ A₂).symm

Full source

@[simp]
theorem symm_toAddEquiv : (e.symm : A₂ ≃+ A₁) = (e : A₁ ≃+ A₂).symm :=
  rfl

Compatibility of Inverse with Underlying Additive Equivalence in $R$-Algebra Isomorphisms

Informal description

For any $R$-algebra isomorphism $e \colon A_1 \simeq_{alg[R]} A_2$, the underlying additive equivalence of its inverse $e^{-1} \colon A_2 \simeq_{alg[R]} A_1$ is equal to the inverse of the underlying additive equivalence of $e$. In symbols, if we denote the underlying additive equivalence of $e$ as $\tilde{e}_{add} \colon A_1 \simeq_{+} A_2$, then $\widetilde{e^{-1}}_{add} = \tilde{e}_{add}^{-1}$.

AlgEquiv.symm_toMulEquiv theorem

: (e.symm : A₂ ≃* A₁) = (e : A₁ ≃* A₂).symm

Full source

@[simp]
theorem symm_toMulEquiv : (e.symm : A₂ ≃* A₁) = (e : A₁ ≃* A₂).symm :=
  rfl

Inverse of $R$-algebra isomorphism preserves multiplicative equivalence

Informal description

For any $R$-algebra isomorphism $e : A_1 \simeq_{alg[R]} A_2$, the underlying multiplicative equivalence of the inverse $e^{-1} : A_2 \simeq_{alg[R]} A_1$ is equal to the inverse of the multiplicative equivalence underlying $e$. In symbols, if we let $e_{mul} : A_1 \simeq^* A_2$ denote the multiplicative equivalence underlying $e$, then $(e^{-1})_{mul} = (e_{mul})^{-1}$.

AlgEquiv.apply_symm_apply theorem

(e : A₁ ≃ₐ[R] A₂) : ∀ x, e (e.symm x) = x

Full source

@[simp]
theorem apply_symm_apply (e : A₁ ≃ₐ[R] A₂) : ∀ x, e (e.symm x) = x :=
  e.toEquiv.apply_symm_apply

Recovery of Element via $R$-Algebra Isomorphism and its Inverse

Informal description

For any $R$-algebra isomorphism $e \colon A_1 \simeq_{alg[R]} A_2$ and any element $x \in A_2$, applying $e$ to the inverse image $e^{-1}(x)$ recovers the original element $x$, i.e., $e(e^{-1}(x)) = x$.

AlgEquiv.symm_apply_apply theorem

(e : A₁ ≃ₐ[R] A₂) : ∀ x, e.symm (e x) = x

Full source

@[simp]
theorem symm_apply_apply (e : A₁ ≃ₐ[R] A₂) : ∀ x, e.symm (e x) = x :=
  e.toEquiv.symm_apply_apply

Inverse of $R$-algebra isomorphism recovers original element

Informal description

For any $R$-algebra isomorphism $e \colon A_1 \simeq_{R} A_2$ and any element $x \in A_1$, the inverse isomorphism $e^{-1}$ satisfies $e^{-1}(e(x)) = x$.

AlgEquiv.symm_apply_eq theorem

(e : A₁ ≃ₐ[R] A₂) {x y} : e.symm x = y ↔ x = e y

Full source

theorem symm_apply_eq (e : A₁ ≃ₐ[R] A₂) {x y} : e.symm x = y ↔ x = e y :=
  e.toEquiv.symm_apply_eq

Characterization of inverse $R$-algebra isomorphism: $e^{-1}(x) = y \leftrightarrow x = e(y)$

Informal description

Let $R$ be a commutative semiring, and let $A_1$ and $A_2$ be $R$-algebras. For any $R$-algebra isomorphism $e: A_1 \simeq_{alg[R]} A_2$ and elements $x \in A_2$, $y \in A_1$, we have $e^{-1}(x) = y$ if and only if $x = e(y)$.

AlgEquiv.comp_symm theorem

(e : A₁ ≃ₐ[R] A₂) : AlgHom.comp (e : A₁ →ₐ[R] A₂) ↑e.symm = AlgHom.id R A₂

Full source

@[simp]
theorem comp_symm (e : A₁ ≃ₐ[R] A₂) : AlgHom.comp (e : A₁ →ₐ[R] A₂) ↑e.symm = AlgHom.id R A₂ := by
  ext
  simp

Composition of $R$-Algebra Isomorphism with its Inverse Yields Identity

Informal description

Let $R$ be a commutative semiring, and let $A_1$ and $A_2$ be $R$-algebras. For any $R$-algebra isomorphism $e: A_1 \simeq_{alg[R]} A_2$, the composition of $e$ with its inverse $e^{-1}$ (as $R$-algebra homomorphisms) yields the identity homomorphism on $A_2$, i.e., $e \circ e^{-1} = \text{id}_{A_2}$.

AlgEquiv.symm_comp theorem

(e : A₁ ≃ₐ[R] A₂) : AlgHom.comp ↑e.symm (e : A₁ →ₐ[R] A₂) = AlgHom.id R A₁

Full source

@[simp]
theorem symm_comp (e : A₁ ≃ₐ[R] A₂) : AlgHom.comp ↑e.symm (e : A₁ →ₐ[R] A₂) = AlgHom.id R A₁ := by
  ext
  simp

Inverse Composition of $R$-Algebra Isomorphism Yields Identity

Informal description

For any $R$-algebra isomorphism $e \colon A_1 \simeq_{alg[R]} A_2$, the composition of the inverse isomorphism $e^{-1}$ with $e$ is equal to the identity algebra homomorphism on $A_1$, i.e., $e^{-1} \circ e = \text{id}_{A_1}$.

AlgEquiv.leftInverse_symm theorem

(e : A₁ ≃ₐ[R] A₂) : Function.LeftInverse e.symm e

Full source

theorem leftInverse_symm (e : A₁ ≃ₐ[R] A₂) : Function.LeftInverse e.symm e :=
  e.left_inv

Inverse as Left Inverse of $R$-Algebra Isomorphism

Informal description

For any $R$-algebra isomorphism $e: A_1 \simeq_{alg[R]} A_2$, the inverse map $e^{-1}$ is a left inverse of $e$, i.e., $e^{-1} \circ e = \text{id}_{A_1}$.

AlgEquiv.rightInverse_symm theorem

(e : A₁ ≃ₐ[R] A₂) : Function.RightInverse e.symm e

Full source

theorem rightInverse_symm (e : A₁ ≃ₐ[R] A₂) : Function.RightInverse e.symm e :=
  e.right_inv

Inverse as Right Inverse of $R$-Algebra Isomorphism

Informal description

For any $R$-algebra isomorphism $e: A_1 \simeq_{alg[R]} A_2$, the inverse map $e^{-1}$ is a right inverse of $e$, i.e., $e \circ e^{-1} = \text{id}_{A_2}$.

AlgEquiv.Simps.apply definition

(e : A₁ ≃ₐ[R] A₂) : A₁ → A₂

Full source

/-- See Note [custom simps projection] -/
def Simps.apply (e : A₁ ≃ₐ[R] A₂) : A₁ → A₂ :=
  e

Underlying function of an $R$-algebra isomorphism

Informal description

The function maps an $R$-algebra isomorphism $e : A_1 \simeq_{alg[R]} A_2$ to its underlying function $A_1 \to A_2$.

AlgEquiv.Simps.toEquiv definition

(e : A₁ ≃ₐ[R] A₂) : A₁ ≃ A₂

Full source

/-- See Note [custom simps projection] -/
def Simps.toEquiv (e : A₁ ≃ₐ[R] A₂) : A₁ ≃ A₂ :=
  e

Underlying bijection of an $R$-algebra isomorphism

Informal description

The function maps an $R$-algebra isomorphism $e : A_1 \simeq_{alg[R]} A_2$ to its underlying bijection $A_1 \simeq A_2$.

AlgEquiv.Simps.symm_apply definition

(e : A₁ ≃ₐ[R] A₂) : A₂ → A₁

Full source

/-- See Note [custom simps projection] -/
def Simps.symm_apply (e : A₁ ≃ₐ[R] A₂) : A₂ → A₁ :=
  e.symm

Inverse function of an $R$-algebra isomorphism

Informal description

The function maps an $R$-algebra isomorphism $e : A_1 \simeq_{alg[R]} A_2$ to its inverse function $A_2 \to A_1$.

AlgEquiv.trans definition

(e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) : A₁ ≃ₐ[R] A₃

Full source

/-- Algebra equivalences are transitive. -/
@[trans]
def trans (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) : A₁ ≃ₐ[R] A₃ :=
  { e₁.toRingEquiv.trans e₂.toRingEquiv with
    commutes' := fun r => show e₂.toFun (e₁.toFun _) = _ by rw [e₁.commutes', e₂.commutes'] }

Composition of $R$-algebra isomorphisms

Informal description

Given two $R$-algebra isomorphisms $e_1: A_1 \simeq_{alg[R]} A_2$ and $e_2: A_2 \simeq_{alg[R]} A_3$, their composition $e_2 \circ e_1$ forms an $R$-algebra isomorphism $A_1 \simeq_{alg[R]} A_3$ that preserves both the ring structure and the scalar multiplication by elements of $R$.

AlgEquiv.coe_trans theorem

(e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) : ⇑(e₁.trans e₂) = e₂ ∘ e₁

Full source

@[simp]
theorem coe_trans (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) : ⇑(e₁.trans e₂) = e₂ ∘ e₁ :=
  rfl

Composition of $R$-algebra isomorphisms preserves function composition

Informal description

For any $R$-algebra isomorphisms $e_1: A_1 \simeq_{alg[R]} A_2$ and $e_2: A_2 \simeq_{alg[R]} A_3$, 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 A_1$.

AlgEquiv.trans_apply theorem

(e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) (x : A₁) : (e₁.trans e₂) x = e₂ (e₁ x)

Full source

@[simp]
theorem trans_apply (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) (x : A₁) : (e₁.trans e₂) x = e₂ (e₁ x) :=
  rfl

Composition of $R$-algebra isomorphisms applied to an element

Informal description

Let $R$ be a commutative semiring, and let $A_1$, $A_2$, $A_3$ be semirings equipped with $R$-algebra structures. Given $R$-algebra isomorphisms $e_1: A_1 \simeq_{alg[R]} A_2$ and $e_2: A_2 \simeq_{alg[R]} A_3$, for any element $x \in A_1$, the composition $(e_2 \circ e_1)(x)$ equals $e_2(e_1(x))$.

AlgEquiv.symm_trans_apply theorem

 (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) (x : A₃) : (e₁.trans e₂).symm x = e₁.symm (e₂.symm x)

Full source

@[simp]
theorem symm_trans_apply (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) (x : A₃) :
    (e₁.trans e₂).symm x = e₁.symm (e₂.symm x) :=
  rfl

Inverse of Composition of $R$-Algebra Isomorphisms

Informal description

Let $R$ be a commutative semiring, and let $A_1$, $A_2$, $A_3$ be semirings equipped with $R$-algebra structures. Given $R$-algebra isomorphisms $e_1: A_1 \simeq_{alg[R]} A_2$ and $e_2: A_2 \simeq_{alg[R]} A_3$, for any $x \in A_3$, the inverse of the composition $(e_1 \circ e_2)^{-1}(x)$ equals $e_1^{-1}(e_2^{-1}(x))$.

AlgEquiv.arrowCongr definition

(e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') : (A₁ →ₐ[R] A₂) ≃ (A₁' →ₐ[R] A₂')

Full source

/-- If `A₁` is equivalent to `A₁'` and `A₂` is equivalent to `A₂'`, then the type of maps
`A₁ →ₐ[R] A₂` is equivalent to the type of maps `A₁' →ₐ[R] A₂'`. -/
@[simps apply]
def arrowCongr (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') : (A₁ →ₐ[R] A₂) ≃ (A₁' →ₐ[R] A₂') where
  toFun f := (e₂.toAlgHom.comp f).comp e₁.symm.toAlgHom
  invFun f := (e₂.symm.toAlgHom.comp f).comp e₁.toAlgHom
  left_inv f := by
    simp only [AlgHom.comp_assoc, toAlgHom_eq_coe, symm_comp]
    simp only [← AlgHom.comp_assoc, symm_comp, AlgHom.id_comp, AlgHom.comp_id]
  right_inv f := by
    simp only [AlgHom.comp_assoc, toAlgHom_eq_coe, comp_symm]
    simp only [← AlgHom.comp_assoc, comp_symm, AlgHom.id_comp, AlgHom.comp_id]

Equivalence of $R$-algebra homomorphism spaces via isomorphisms

Informal description

Given $R$-algebra isomorphisms $e_1: A_1 \simeq_{R} A_1'$ and $e_2: A_2 \simeq_{R} A_2'$, the function `AlgEquiv.arrowCongr` constructs an equivalence between the types of $R$-algebra homomorphisms $A_1 \to_{alg[R]} A_2$ and $A_1' \to_{alg[R]} A_2'$. Specifically, it maps any $R$-algebra homomorphism $f: A_1 \to_{alg[R]} A_2$ to the composition $e_2 \circ f \circ e_1^{-1}: A_1' \to_{alg[R]} A_2'$, and its inverse maps any $g: A_1' \to_{alg[R]} A_2'$ to $e_2^{-1} \circ g \circ e_1: A_1 \to_{alg[R]} A_2$.

AlgEquiv.arrowCongr_comp theorem

 (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') (e₃ : A₃ ≃ₐ[R] A₃') (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₃) :
  arrowCongr e₁ e₃ (g.comp f) = (arrowCongr e₂ e₃ g).comp (arrowCongr e₁ e₂ f)

Full source

theorem arrowCongr_comp (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂')
    (e₃ : A₃ ≃ₐ[R] A₃') (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₃) :
    arrowCongr e₁ e₃ (g.comp f) = (arrowCongr e₂ e₃ g).comp (arrowCongr e₁ e₂ f) := by
  ext
  simp only [arrowCongr, Equiv.coe_fn_mk, AlgHom.comp_apply]
  congr
  exact (e₂.symm_apply_apply _).symm

Composition of Induced Maps on Algebra Homomorphism Spaces via Isomorphisms

Informal description

Let $R$ be a commutative semiring, and let $A_1, A_1'$, $A_2, A_2'$, $A_3, A_3'$ be semirings equipped with $R$-algebra structures. Given $R$-algebra isomorphisms $e_1: A_1 \simeq_{alg[R]} A_1'$, $e_2: A_2 \simeq_{alg[R]} A_2'$, and $e_3: A_3 \simeq_{alg[R]} A_3'$, and $R$-algebra homomorphisms $f: A_1 \to_{alg[R]} A_2$ and $g: A_2 \to_{alg[R]} A_3$, the following diagram commutes: The composition of the induced maps on homomorphism spaces satisfies: \[ \text{arrowCongr}(e_1, e_3)(g \circ f) = \text{arrowCongr}(e_2, e_3)(g) \circ \text{arrowCongr}(e_1, e_2)(f) \]

AlgEquiv.arrowCongr_refl theorem

: arrowCongr AlgEquiv.refl AlgEquiv.refl = Equiv.refl (A₁ →ₐ[R] A₂)

Full source

@[simp]
theorem arrowCongr_refl : arrowCongr AlgEquiv.refl AlgEquiv.refl = Equiv.refl (A₁ →ₐ[R] A₂) :=
  rfl

Identity Isomorphisms Induce Identity Equivalence on Homomorphism Spaces

Informal description

Given $R$-algebras $A_1$ and $A_2$, the equivalence of $R$-algebra homomorphism spaces obtained by applying the identity isomorphisms on $A_1$ and $A_2$ is equal to the identity equivalence on the space of $R$-algebra homomorphisms from $A_1$ to $A_2$. In other words, if we consider the identity $R$-algebra isomorphisms $\text{id}_{A_1}: A_1 \simeq_{R} A_1$ and $\text{id}_{A_2}: A_2 \simeq_{R} A_2$, then the induced equivalence $\text{arrowCongr}(\text{id}_{A_1}, \text{id}_{A_2})$ between the spaces of $R$-algebra homomorphisms $A_1 \to_{alg[R]} A_2$ and $A_1 \to_{alg[R]} A_2$ is exactly the identity equivalence on $A_1 \to_{alg[R]} A_2$.

AlgEquiv.arrowCongr_trans theorem

 (e₁ : A₁ ≃ₐ[R] A₂) (e₁' : A₁' ≃ₐ[R] A₂') (e₂ : A₂ ≃ₐ[R] A₃) (e₂' : A₂' ≃ₐ[R] A₃') :
  arrowCongr (e₁.trans e₂) (e₁'.trans e₂') = (arrowCongr e₁ e₁').trans (arrowCongr e₂ e₂')

Full source

@[simp]
theorem arrowCongr_trans (e₁ : A₁ ≃ₐ[R] A₂) (e₁' : A₁' ≃ₐ[R] A₂')
    (e₂ : A₂ ≃ₐ[R] A₃) (e₂' : A₂' ≃ₐ[R] A₃') :
    arrowCongr (e₁.trans e₂) (e₁'.trans e₂') = (arrowCongr e₁ e₁').trans (arrowCongr e₂ e₂') :=
  rfl

Composition Property of $\text{arrowCongr}$ for $R$-Algebra Isomorphisms

Informal description

Given $R$-algebra isomorphisms $e_1: A_1 \simeq_{alg[R]} A_2$, $e_1': A_1' \simeq_{alg[R]} A_2'$, $e_2: A_2 \simeq_{alg[R]} A_3$, and $e_2': A_2' \simeq_{alg[R]} A_3'$, the following equality holds: \[ \text{arrowCongr}(e_1 \circ e_2, e_1' \circ e_2') = \text{arrowCongr}(e_1, e_1') \circ \text{arrowCongr}(e_2, e_2') \] Here, $\text{arrowCongr}$ denotes the equivalence between spaces of $R$-algebra homomorphisms induced by the given isomorphisms, and $\circ$ denotes composition of equivalences.

AlgEquiv.arrowCongr_symm theorem

 (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') : (arrowCongr e₁ e₂).symm = arrowCongr e₁.symm e₂.symm

Full source

@[simp]
theorem arrowCongr_symm (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') :
    (arrowCongr e₁ e₂).symm = arrowCongr e₁.symm e₂.symm :=
  rfl

Inverse of $\text{arrowCongr}$ Equivalence for $R$-Algebra Isomorphisms

Informal description

Given $R$-algebra isomorphisms $e_1: A_1 \simeq_{alg[R]} A_1'$ and $e_2: A_2 \simeq_{alg[R]} A_2'$, the inverse of the equivalence $\text{arrowCongr}(e_1, e_2)$ between spaces of $R$-algebra homomorphisms is equal to the equivalence $\text{arrowCongr}(e_1^{-1}, e_2^{-1})$. In other words, the inverse of the map that sends an $R$-algebra homomorphism $f: A_1 \to_{alg[R]} A_2$ to $e_2 \circ f \circ e_1^{-1}: A_1' \to_{alg[R]} A_2'$ is the map that sends $g: A_1' \to_{alg[R]} A_2'$ to $e_2^{-1} \circ g \circ e_1: A_1 \to_{alg[R]} A_2$.

AlgEquiv.equivCongr definition

(e : A₁ ≃ₐ[R] A₂) (e' : A₁' ≃ₐ[R] A₂') : (A₁ ≃ₐ[R] A₁') ≃ A₂ ≃ₐ[R] A₂'

Full source

/-- If `A₁` is equivalent to `A₂` and `A₁'` is equivalent to `A₂'`, then the type of maps
`A₁ ≃ₐ[R] A₁'` is equivalent to the type of maps `A₂ ≃ ₐ[R] A₂'`.

This is the `AlgEquiv` version of `AlgEquiv.arrowCongr`. -/
@[simps apply]
def equivCongr (e : A₁ ≃ₐ[R] A₂) (e' : A₁' ≃ₐ[R] A₂') : (A₁ ≃ₐ[R] A₁') ≃ A₂ ≃ₐ[R] A₂' where
  toFun ψ := e.symm.trans (ψ.trans e')
  invFun ψ := e.trans (ψ.trans e'.symm)
  left_inv ψ := by
    ext
    simp_rw [trans_apply, symm_apply_apply]
  right_inv ψ := by
    ext
    simp_rw [trans_apply, apply_symm_apply]

Equivalence of $R$-algebra isomorphism types via conjugation

Informal description

Given two $R$-algebra isomorphisms $e: A_1 \simeq_{alg[R]} A_2$ and $e': A_1' \simeq_{alg[R]} A_2'$, the function `equivCongr` constructs a bijection between the types of $R$-algebra isomorphisms $A_1 \simeq_{alg[R]} A_1'$ and $A_2 \simeq_{alg[R]} A_2'$. More precisely, for any $R$-algebra isomorphism $\psi: A_1 \simeq_{alg[R]} A_1'$, the corresponding isomorphism $A_2 \simeq_{alg[R]} A_2'$ is given by the composition $e^{-1} \circ \psi \circ e'$, and conversely, any isomorphism $A_2 \simeq_{alg[R]} A_2'$ can be transformed back via $e \circ \psi \circ e'^{-1}$. This bijection preserves the structure of $R$-algebra isomorphisms, ensuring that the resulting maps are still $R$-algebra isomorphisms.

AlgEquiv.equivCongr_refl theorem

: equivCongr AlgEquiv.refl AlgEquiv.refl = Equiv.refl (A₁ ≃ₐ[R] A₁')

Full source

@[simp]
theorem equivCongr_refl : equivCongr AlgEquiv.refl AlgEquiv.refl = Equiv.refl (A₁ ≃ₐ[R] A₁') :=
  rfl

Identity Conjugation Yields Identity Equivalence for $R$-Algebra Isomorphisms

Informal description

The conjugation of $R$-algebra isomorphism types via the identity isomorphisms is equal to the identity equivalence on the type of $R$-algebra isomorphisms from $A_1$ to itself. In other words, the bijection between $(A_1 \simeq_{alg[R]} A_1)$ and itself, induced by the identity isomorphisms, is the identity bijection.

AlgEquiv.equivCongr_symm theorem

(e : A₁ ≃ₐ[R] A₂) (e' : A₁' ≃ₐ[R] A₂') : (equivCongr e e').symm = equivCongr e.symm e'.symm

Full source

@[simp]
theorem equivCongr_symm (e : A₁ ≃ₐ[R] A₂) (e' : A₁' ≃ₐ[R] A₂') :
    (equivCongr e e').symm = equivCongr e.symm e'.symm :=
  rfl

Inverse of Algebra Isomorphism Conjugation Equals Conjugation of Inverses

Informal description

Given two $R$-algebra isomorphisms $e: A_1 \simeq_{alg[R]} A_2$ and $e': A_1' \simeq_{alg[R]} A_2'$, the inverse of the bijection $\text{equivCongr}(e, e')$ between the types of $R$-algebra isomorphisms $A_1 \simeq_{alg[R]} A_1'$ and $A_2 \simeq_{alg[R]} A_2'$ is equal to the bijection $\text{equivCongr}(e^{-1}, e'^{-1})$.

AlgEquiv.equivCongr_trans theorem

 (e₁₂ : A₁ ≃ₐ[R] A₂) (e₁₂' : A₁' ≃ₐ[R] A₂') (e₂₃ : A₂ ≃ₐ[R] A₃) (e₂₃' : A₂' ≃ₐ[R] A₃') :
  (equivCongr e₁₂ e₁₂').trans (equivCongr e₂₃ e₂₃') = equivCongr (e₁₂.trans e₂₃) (e₁₂'.trans e₂₃')

Full source

@[simp]
theorem equivCongr_trans (e₁₂ : A₁ ≃ₐ[R] A₂) (e₁₂' : A₁' ≃ₐ[R] A₂')
    (e₂₃ : A₂ ≃ₐ[R] A₃) (e₂₃' : A₂' ≃ₐ[R] A₃') :
    (equivCongr e₁₂ e₁₂').trans (equivCongr e₂₃ e₂₃') =
      equivCongr (e₁₂.trans e₂₃) (e₁₂'.trans e₂₃') :=
  rfl

Composition of Conjugation Bijections for $R$-Algebra Isomorphisms

Informal description

Given four $R$-algebra isomorphisms $e_{12}: A_1 \simeq_{alg[R]} A_2$, $e_{12}': A_1' \simeq_{alg[R]} A_2'$, $e_{23}: A_2 \simeq_{alg[R]} A_3$, and $e_{23}': A_2' \simeq_{alg[R]} A_3'$, the composition of the conjugation bijections $\text{equivCongr}(e_{12}, e_{12}')$ and $\text{equivCongr}(e_{23}, e_{23}')$ is equal to the conjugation bijection of the composed isomorphisms $\text{equivCongr}(e_{12} \circ e_{23}, e_{12}' \circ e_{23}')$.

AlgEquiv.ofAlgHom definition

 (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂) (h₂ : g.comp f = AlgHom.id R A₁) : A₁ ≃ₐ[R] A₂

Full source

/-- If an algebra morphism has an inverse, it is an algebra isomorphism. -/
@[simps]
def ofAlgHom (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂)
    (h₂ : g.comp f = AlgHom.id R A₁) : A₁ ≃ₐ[R] A₂ :=
  { f with
    toFun := f
    invFun := g
    left_inv := AlgHom.ext_iff.1 h₂
    right_inv := AlgHom.ext_iff.1 h₁ }

Construction of algebra isomorphism from mutual inverses

Informal description

Given two $R$-algebra homomorphisms $f: A_1 \to A_2$ and $g: A_2 \to A_1$ such that $f \circ g$ is the identity on $A_2$ and $g \circ f$ is the identity on $A_1$, this constructs an $R$-algebra isomorphism between $A_1$ and $A_2$ with $f$ as the forward map and $g$ as the inverse map.

AlgEquiv.coe_algHom_ofAlgHom theorem

(f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ h₂) : ↑(ofAlgHom f g h₁ h₂) = f

Full source

theorem coe_algHom_ofAlgHom (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ h₂) :
    ↑(ofAlgHom f g h₁ h₂) = f :=
  rfl

Underlying Homomorphism of Constructed Algebra Isomorphism

Informal description

Let $R$ be a commutative semiring and $A_1$, $A_2$ be semirings equipped with $R$-algebra structures. Given $R$-algebra homomorphisms $f: A_1 \to A_2$ and $g: A_2 \to A_1$ such that $f \circ g$ is the identity on $A_2$ and $g \circ f$ is the identity on $A_1$, the underlying algebra homomorphism of the algebra isomorphism constructed via `ofAlgHom` equals $f$.

AlgEquiv.ofAlgHom_coe_algHom theorem

(f : A₁ ≃ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ h₂) : ofAlgHom (↑f) g h₁ h₂ = f

Full source

@[simp]
theorem ofAlgHom_coe_algHom (f : A₁ ≃ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ h₂) :
    ofAlgHom (↑f) g h₁ h₂ = f :=
  ext fun _ => rfl

Recovery of Algebra Isomorphism from Underlying Homomorphism Construction

Informal description

Let $R$ be a commutative semiring, and let $A_1$ and $A_2$ be semirings equipped with $R$-algebra structures. Given an $R$-algebra isomorphism $f: A_1 \simeq_{alg[R]} A_2$ and an $R$-algebra homomorphism $g: A_2 \to A_1$ satisfying the mutual inverse conditions $f \circ g = \text{id}_{A_2}$ and $g \circ f = \text{id}_{A_1}$, the construction of the algebra isomorphism via `ofAlgHom` applied to the underlying homomorphism of $f$ and $g$ recovers $f$ itself. That is, $\text{ofAlgHom}(f, g, h_1, h_2) = f$.

AlgEquiv.ofAlgHom_symm theorem

 (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ h₂) : (ofAlgHom f g h₁ h₂).symm = ofAlgHom g f h₂ h₁

Full source

theorem ofAlgHom_symm (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ h₂) :
    (ofAlgHom f g h₁ h₂).symm = ofAlgHom g f h₂ h₁ :=
  rfl

Inverse of Algebra Isomorphism Constructed from Mutual Inverses

Informal description

Given $R$-algebra homomorphisms $f: A_1 \to A_2$ and $g: A_2 \to A_1$ such that $f \circ g = \text{id}_{A_2}$ and $g \circ f = \text{id}_{A_1}$, the inverse of the $R$-algebra isomorphism $\text{ofAlgHom}(f, g, h_1, h_2)$ is equal to $\text{ofAlgHom}(g, f, h_2, h_1)$.

AlgEquiv.ofBijective definition

(f : A₁ →ₐ[R] A₂) (hf : Function.Bijective f) : A₁ ≃ₐ[R] A₂

Full source

/-- Promotes a bijective algebra homomorphism to an algebra equivalence. -/
noncomputable def ofBijective (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective f) : A₁ ≃ₐ[R] A₂ :=
  { RingEquiv.ofBijective (f : A₁ →+* A₂) hf, f with }

$R$-algebra isomorphism from a bijective $R$-algebra homomorphism

Informal description

Given a bijective $R$-algebra homomorphism $f: A_1 \to A_2$ between two $R$-algebras $A_1$ and $A_2$, this function constructs an $R$-algebra isomorphism $A_1 \simeq_{R} A_2$ by combining the bijection with the ring homomorphism structure of $f$.

AlgEquiv.coe_ofBijective theorem

{f : A₁ →ₐ[R] A₂} {hf : Function.Bijective f} : (AlgEquiv.ofBijective f hf : A₁ → A₂) = f

Full source

@[simp]
theorem coe_ofBijective {f : A₁ →ₐ[R] A₂} {hf : Function.Bijective f} :
    (AlgEquiv.ofBijective f hf : A₁ → A₂) = f :=
  rfl

Underlying function of $R$-algebra isomorphism from bijective homomorphism equals original homomorphism

Informal description

Let $R$ be a commutative semiring, and let $A_1$ and $A_2$ be semirings equipped with $R$-algebra structures. Given a bijective $R$-algebra homomorphism $f: A_1 \to A_2$, the underlying function of the $R$-algebra isomorphism $\text{AlgEquiv.ofBijective}\, f\, hf$ is equal to $f$.

AlgEquiv.ofBijective_apply theorem

{f : A₁ →ₐ[R] A₂} {hf : Function.Bijective f} (a : A₁) : (AlgEquiv.ofBijective f hf) a = f a

Full source

theorem ofBijective_apply {f : A₁ →ₐ[R] A₂} {hf : Function.Bijective f} (a : A₁) :
    (AlgEquiv.ofBijective f hf) a = f a :=
  rfl

Evaluation of $R$-algebra isomorphism constructed from bijective homomorphism

Informal description

Let $R$ be a commutative semiring, and let $A_1$ and $A_2$ be semirings equipped with $R$-algebra structures. Given a bijective $R$-algebra homomorphism $f: A_1 \to A_2$ and an element $a \in A_1$, the $R$-algebra isomorphism $\text{AlgEquiv.ofBijective}\,f\,hf$ applied to $a$ equals $f(a)$.

AlgEquiv.toLinearEquiv definition

(e : A₁ ≃ₐ[R] A₂) : A₁ ≃ₗ[R] A₂

Full source

/-- Forgetting the multiplicative structures, an equivalence of algebras is a linear equivalence. -/
@[simps apply]
def toLinearEquiv (e : A₁ ≃ₐ[R] A₂) : A₁ ≃ₗ[R] A₂ :=
  { e with
    toFun := e
    map_smul' := map_smul e
    invFun := e.symm }

Linear equivalence induced by an $R$-algebra isomorphism

Informal description

Given an $R$-algebra isomorphism $e \colon A_1 \simeq_{alg[R]} A_2$, the function maps $e$ to the corresponding linear equivalence $A_1 \simeq_{lin[R]} A_2$, which is a bijective linear map preserving the $R$-module structure. More precisely, the linear equivalence has: - The same underlying function as $e$, - The property that it preserves scalar multiplication: $e(r \cdot x) = r \cdot e(x)$ for all $r \in R$ and $x \in A_1$, - The inverse function given by the inverse algebra isomorphism $e^{-1}$.

AlgEquiv.toLinearEquiv_refl theorem

: (AlgEquiv.refl : A₁ ≃ₐ[R] A₁).toLinearEquiv = LinearEquiv.refl R A₁

Full source

@[simp]
theorem toLinearEquiv_refl : (AlgEquiv.refl : A₁ ≃ₐ[R] A₁).toLinearEquiv = LinearEquiv.refl R A₁ :=
  rfl

Identity $R$-Algebra Isomorphism Induces Identity Linear Equivalence

Informal description

For any $R$-algebra $A_1$, the linear equivalence induced by the identity $R$-algebra isomorphism $\text{AlgEquiv.refl} \colon A_1 \simeq_{\text{alg}[R]} A_1$ is equal to the identity linear equivalence $\text{LinearEquiv.refl} \colon A_1 \simeq_{\text{lin}[R]} A_1$.

AlgEquiv.toLinearEquiv_symm theorem

(e : A₁ ≃ₐ[R] A₂) : e.toLinearEquiv.symm = e.symm.toLinearEquiv

Full source

@[simp]
theorem toLinearEquiv_symm (e : A₁ ≃ₐ[R] A₂) : e.toLinearEquiv.symm = e.symm.toLinearEquiv :=
  rfl

Inverse of Linear Equivalence from Algebra Isomorphism Equals Linear Equivalence of Inverse Isomorphism

Informal description

For any $R$-algebra isomorphism $e \colon A_1 \simeq_{alg[R]} A_2$, the linear equivalence obtained from the inverse of $e$ is equal to the inverse of the linear equivalence obtained from $e$. In other words, $(e^{-1})_{lin[R]} = (e_{lin[R]})^{-1}$.

AlgEquiv.toLinearEquiv_trans theorem

 (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) : (e₁.trans e₂).toLinearEquiv = e₁.toLinearEquiv.trans e₂.toLinearEquiv

Full source

@[simp]
theorem toLinearEquiv_trans (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) :
    (e₁.trans e₂).toLinearEquiv = e₁.toLinearEquiv.trans e₂.toLinearEquiv :=
  rfl

Compatibility of Linear Equivalence with Composition of Algebra Isomorphisms

Informal description

For any $R$-algebra isomorphisms $e_1 \colon A_1 \simeq_{alg[R]} A_2$ and $e_2 \colon A_2 \simeq_{alg[R]} A_3$, the linear equivalence induced by their composition $(e_1 \circ e_2)$ is equal to the composition of their induced linear equivalences. That is, $(e_1 \circ e_2).toLinearEquiv = e_1.toLinearEquiv \circ e_2.toLinearEquiv$.

AlgEquiv.toLinearEquiv_injective theorem

: Function.Injective (toLinearEquiv : _ → A₁ ≃ₗ[R] A₂)

Full source

theorem toLinearEquiv_injective : Function.Injective (toLinearEquiv : _ → A₁ ≃ₗ[R] A₂) :=
  fun _ _ h => ext <| LinearEquiv.congr_fun h

Injectivity of the Linear Equivalence Induced by an $R$-Algebra Isomorphism

Informal description

The map that sends an $R$-algebra isomorphism $e \colon A_1 \simeq_{alg[R]} A_2$ to its induced linear equivalence $e \colon A_1 \simeq_{lin[R]} A_2$ is injective. In other words, if two $R$-algebra isomorphisms induce the same linear equivalence, then they must be equal as $R$-algebra isomorphisms.

AlgEquiv.toLinearMap definition

: A₁ →ₗ[R] A₂

Full source

/-- Interpret an algebra equivalence as a linear map. -/
def toLinearMap : A₁ →ₗ[R] A₂ :=
  e.toAlgHom.toLinearMap

Underlying linear map of an $R$-algebra isomorphism

Informal description

The function maps an $R$-algebra isomorphism $e: A_1 \simeq_{alg[R]} A_2$ to its underlying $R$-linear map $e: A_1 \to_{lin[R]} A_2$, which preserves the additive structure and scalar multiplication by elements of $R$.

AlgEquiv.toAlgHom_toLinearMap theorem

: (e : A₁ →ₐ[R] A₂).toLinearMap = e.toLinearMap

Full source

@[simp]
theorem toAlgHom_toLinearMap : (e : A₁ →ₐ[R] A₂).toLinearMap = e.toLinearMap :=
  rfl

Equality of Underlying Linear Maps for Algebra Isomorphism and Homomorphism

Informal description

For any $R$-algebra isomorphism $e \colon A_1 \to A_2$, the underlying linear map of the corresponding algebra homomorphism equals the underlying linear map of $e$.

AlgEquiv.toLinearMap_ofAlgHom theorem

(f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ h₂) : (ofAlgHom f g h₁ h₂).toLinearMap = f.toLinearMap

Full source

theorem toLinearMap_ofAlgHom (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ h₂) :
    (ofAlgHom f g h₁ h₂).toLinearMap = f.toLinearMap :=
  LinearMap.ext fun _ => rfl

Underlying Linear Map of Algebra Isomorphism Constructed from Mutual Inverses

Informal description

Let $R$ be a commutative semiring, and let $A_1$ and $A_2$ be $R$-algebras. Given $R$-algebra homomorphisms $f: A_1 \to A_2$ and $g: A_2 \to A_1$ such that $f \circ g$ is the identity on $A_2$ and $g \circ f$ is the identity on $A_1$, the underlying linear map of the algebra isomorphism $\text{ofAlgHom}(f, g, h_1, h_2): A_1 \simeq_{alg[R]} A_2$ is equal to the underlying linear map of $f$.

AlgEquiv.toLinearEquiv_toLinearMap theorem

: e.toLinearEquiv.toLinearMap = e.toLinearMap

Full source

@[simp]
theorem toLinearEquiv_toLinearMap : e.toLinearEquiv.toLinearMap = e.toLinearMap :=
  rfl

Equality of Linear Maps Induced by Algebra Isomorphism

Informal description

For any $R$-algebra isomorphism $e \colon A_1 \simeq_{alg[R]} A_2$, the underlying linear map of the corresponding linear equivalence $e.toLinearEquiv$ is equal to the underlying linear map of $e$ itself, i.e., $e.toLinearEquiv.toLinearMap = e.toLinearMap$.

AlgEquiv.toLinearMap_apply theorem

(x : A₁) : e.toLinearMap x = e x

Full source

@[simp]
theorem toLinearMap_apply (x : A₁) : e.toLinearMap x = e x :=
  rfl

Equality of $R$-algebra isomorphism and its underlying linear map on elements

Informal description

For any $R$-algebra isomorphism $e \colon A_1 \simeq_{alg[R]} A_2$ and any element $x \in A_1$, the application of the underlying linear map $e.toLinearMap$ to $x$ equals the application of $e$ to $x$, i.e., $e.toLinearMap(x) = e(x)$.

AlgEquiv.toLinearMap_injective theorem

: Function.Injective (toLinearMap : _ → A₁ →ₗ[R] A₂)

Full source

theorem toLinearMap_injective : Function.Injective (toLinearMap : _ → A₁ →ₗ[R] A₂) := fun _ _ h =>
  ext <| LinearMap.congr_fun h

Injectivity of the Underlying Linear Map Construction for $R$-Algebra Isomorphisms

Informal description

The map that sends an $R$-algebra isomorphism $e \colon A_1 \simeq_{\text{Alg}[R]} A_2$ to its underlying $R$-linear map $e \colon A_1 \to_{lin[R]} A_2$ is injective. In other words, if two $R$-algebra isomorphisms induce the same linear map, then they must be equal.

AlgEquiv.trans_toLinearMap theorem

(f : A₁ ≃ₐ[R] A₂) (g : A₂ ≃ₐ[R] A₃) : (f.trans g).toLinearMap = g.toLinearMap.comp f.toLinearMap

Full source

@[simp]
theorem trans_toLinearMap (f : A₁ ≃ₐ[R] A₂) (g : A₂ ≃ₐ[R] A₃) :
    (f.trans g).toLinearMap = g.toLinearMap.comp f.toLinearMap :=
  rfl

Composition of $R$-algebra isomorphisms corresponds to composition of underlying linear maps

Informal description

For any $R$-algebra isomorphisms $f \colon A_1 \simeq_{\text{Alg}[R]} A_2$ and $g \colon A_2 \simeq_{\text{Alg}[R]} A_3$, the underlying linear map of their composition $f \circ g$ is equal to the composition of their underlying linear maps, i.e., $(f \circ g).toLinearMap = g.toLinearMap \circ f.toLinearMap$.

AlgEquiv.ofLinearEquiv definition

: A₁ ≃ₐ[R] A₂

Full source

/--
Upgrade a linear equivalence to an algebra equivalence,
given that it distributes over multiplication and the identity
-/
@[simps apply]
def ofLinearEquiv : A₁ ≃ₐ[R] A₂ :=
  { l with
    toFun := l
    invFun := l.symm
    map_mul' := map_mul
    commutes' := (AlgHom.ofLinearMap l map_one map_mul : A₁ →ₐ[R] A₂).commutes }

Upgrading a linear equivalence to an algebra isomorphism

Informal description

Given a linear equivalence $ l : A_1 \simeq A_2 $ between $ R $-algebras $ A_1 $ and $ A_2 $, if $ l $ preserves the multiplicative identity (i.e., $ l(1) = 1 $) and distributes over multiplication (i.e., $ l(x \cdot y) = l(x) \cdot l(y) $ for all $ x, y \in A_1 $), then $ l $ can be upgraded to an $ R $-algebra isomorphism $ A_1 \simeq_{\text{Alg}[R]} A_2 $. This isomorphism consists of: - The underlying bijection $ l $ from $ A_1 $ to $ A_2 $ - Its inverse $ l^{-1} $ from $ A_2 $ to $ A_1 $ - The property that $ l $ preserves multiplication and the multiplicative identity - The property that $ l $ commutes with scalar multiplication by elements of $ R $

AlgEquiv.ofLinearEquiv_symm.aux definition

Full source

/-- Auxiliary definition to avoid looping in `dsimp` with `AlgEquiv.ofLinearEquiv_symm`. -/
protected def ofLinearEquiv_symm.aux := (ofLinearEquiv l map_one map_mul).symm

Auxiliary construction for inverse of algebra isomorphism from linear equivalence

Informal description

The auxiliary function used in the construction of the inverse of an $R$-algebra isomorphism obtained from a linear equivalence. Given a linear equivalence $l : A_1 \simeq A_2$ between $R$-algebras $A_1$ and $A_2$, along with proofs that $l$ preserves the multiplicative identity ($l(1) = 1$) and distributes over multiplication ($l(x \cdot y) = l(x) \cdot l(y)$ for all $x, y \in A_1$), this function constructs the inverse of the resulting $R$-algebra isomorphism.

AlgEquiv.ofLinearEquiv_symm theorem

 :
  (ofLinearEquiv l map_one map_mul).symm =
    ofLinearEquiv l.symm (_root_.map_one <| ofLinearEquiv_symm.aux l map_one map_mul)
      (_root_.map_mul <| ofLinearEquiv_symm.aux l map_one map_mul)

Full source

@[simp]
theorem ofLinearEquiv_symm :
    (ofLinearEquiv l map_one map_mul).symm =
      ofLinearEquiv l.symm
        (_root_.map_one <| ofLinearEquiv_symm.aux l map_one map_mul)
        (_root_.map_mul <| ofLinearEquiv_symm.aux l map_one map_mul) :=
  rfl

Inverse of $R$-Algebra Isomorphism Induced by Linear Equivalence

Informal description

Let $R$ be a commutative semiring, and let $A_1$ and $A_2$ be semirings equipped with $R$-algebra structures. Given a linear equivalence $l : A_1 \simeq A_2$ that preserves the multiplicative identity ($l(1) = 1$) and distributes over multiplication ($l(x \cdot y) = l(x) \cdot l(y)$ for all $x, y \in A_1$), the inverse of the induced $R$-algebra isomorphism $\text{ofLinearEquiv}(l, \text{map\_one}, \text{map\_mul})$ is equal to the $R$-algebra isomorphism induced by the inverse linear equivalence $l^{-1}$, where the preservation of identity and multiplication is given by the auxiliary construction $\text{ofLinearEquiv\_symm.aux}(l, \text{map\_one}, \text{map\_mul})$.

AlgEquiv.ofLinearEquiv_toLinearEquiv theorem

(map_mul) (map_one) : ofLinearEquiv e.toLinearEquiv map_mul map_one = e

Full source

@[simp]
theorem ofLinearEquiv_toLinearEquiv (map_mul) (map_one) :
    ofLinearEquiv e.toLinearEquiv map_mul map_one = e :=
  rfl

Reconstruction of Algebra Isomorphism from its Linear Equivalence

Informal description

Let $R$ be a commutative semiring, and let $A_1$ and $A_2$ be semirings equipped with $R$-algebra structures. Given an $R$-algebra isomorphism $e \colon A_1 \simeq_{\text{Alg}[R]} A_2$, the $R$-algebra isomorphism constructed from its induced linear equivalence $e.toLinearEquiv$ (with proofs that it preserves multiplication and the multiplicative identity) is equal to $e$ itself.

AlgEquiv.toLinearEquiv_ofLinearEquiv theorem

: toLinearEquiv (ofLinearEquiv l map_one map_mul) = l

Full source

@[simp]
theorem toLinearEquiv_ofLinearEquiv : toLinearEquiv (ofLinearEquiv l map_one map_mul) = l :=
  rfl

Linear Equivalence Underlying Algebra Isomorphism is Original

Informal description

Given a linear equivalence $l \colon A_1 \simeq A_2$ between $R$-algebras that preserves the multiplicative identity ($l(1) = 1$) and multiplication ($l(x \cdot y) = l(x) \cdot l(y)$ for all $x, y \in A_1$), the linear equivalence induced by the corresponding $R$-algebra isomorphism $\text{ofLinearEquiv}(l, \text{map\_one}, \text{map\_mul})$ is equal to $l$ itself.

AlgEquiv.ofRingEquiv definition

{f : A₁ ≃+* A₂} (hf : ∀ x, f (algebraMap R A₁ x) = algebraMap R A₂ x) : A₁ ≃ₐ[R] A₂

Full source

/-- Promotes a linear `RingEquiv` to an `AlgEquiv`. -/
@[simps apply symm_apply toEquiv]
def ofRingEquiv {f : A₁ ≃+* A₂} (hf : ∀ x, f (algebraMap R A₁ x) = algebraMap R A₂ x) :
    A₁ ≃ₐ[R] A₂ :=
  { f with
    toFun := f
    invFun := f.symm
    commutes' := hf }

$R$-algebra isomorphism from ring isomorphism commuting with algebra maps

Informal description

Given a ring isomorphism $f: A_1 \simeq+* A_2$ between $R$-algebras $A_1$ and $A_2$ that commutes with the algebra maps (i.e., $f(\text{algebraMap}_R A_1(x)) = \text{algebraMap}_R A_2(x)$ for all $x \in R$), this constructs an $R$-algebra isomorphism between $A_1$ and $A_2$ with the same underlying function as $f$.

AlgEquiv.aut instance

: Group (A₁ ≃ₐ[R] A₁)

Full source

@[simps -isSimp one mul, stacks 09HR]
instance aut : Group (A₁ ≃ₐ[R] A₁) where
  mul ϕ ψ := ψ.trans ϕ
  mul_assoc _ _ _ := rfl
  one := refl
  one_mul _ := ext fun _ => rfl
  mul_one _ := ext fun _ => rfl
  inv := symm
  inv_mul_cancel ϕ := ext <| symm_apply_apply ϕ

Group of $R$-algebra Automorphisms

Informal description

The set of $R$-algebra automorphisms of an $R$-algebra $A_1$ forms a group under composition.

AlgEquiv.one_apply theorem

(x : A₁) : (1 : A₁ ≃ₐ[R] A₁) x = x

Full source

@[simp]
theorem one_apply (x : A₁) : (1 : A₁ ≃ₐ[R] A₁) x = x :=
  rfl

Identity Automorphism Acts Trivially on $R$-Algebra Elements

Informal description

For any $R$-algebra $A_1$ and any element $x \in A_1$, the identity automorphism $1 \in \text{Aut}_{R}(A_1)$ acts trivially on $x$, i.e., $1(x) = x$.

AlgEquiv.mul_apply theorem

(e₁ e₂ : A₁ ≃ₐ[R] A₁) (x : A₁) : (e₁ * e₂) x = e₁ (e₂ x)

Full source

@[simp]
theorem mul_apply (e₁ e₂ : A₁ ≃ₐ[R] A₁) (x : A₁) : (e₁ * e₂) x = e₁ (e₂ x) :=
  rfl

Composition of $R$-algebra automorphisms applies sequentially

Informal description

For any $R$-algebra automorphisms $e_1, e_2$ of an $R$-algebra $A_1$ and any element $x \in A_1$, the composition $(e_1 \circ e_2)(x)$ equals $e_1(e_2(x))$.

AlgEquiv.aut_inv theorem

(ϕ : A₁ ≃ₐ[R] A₁) : ϕ⁻¹ = ϕ.symm

Full source

lemma aut_inv (ϕ : A₁ ≃ₐ[R] A₁) : ϕ⁻¹ = ϕ.symm := rfl

Inverse of $R$-algebra automorphism equals its isomorphism inverse

Informal description

For any $R$-algebra automorphism $\phi$ of an $R$-algebra $A_1$, the group inverse $\phi^{-1}$ is equal to the $R$-algebra isomorphism inverse $\phi^{\text{symm}}$.

AlgEquiv.coe_pow theorem

(e : A₁ ≃ₐ[R] A₁) (n : ℕ) : ⇑(e ^ n) = e^[n]

Full source

@[simp] theorem coe_pow (e : A₁ ≃ₐ[R] A₁) (n : ℕ) : ⇑(e ^ n) = e^[n] :=
  n.rec (by ext; simp) fun _ ih ↦ by ext; simp [pow_succ, ih]

Iteration of $R$-algebra automorphisms via powers: $(e^n)(x) = e^[n](x)$

Informal description

For any $R$-algebra automorphism $e \colon A_1 \to A_1$ and any natural number $n$, the $n$-th power of $e$ (under composition in the automorphism group) corresponds to the $n$-th iterate of $e$ as a function, i.e., $(e^n)(x) = e^[n](x)$ for all $x \in A_1$.

AlgEquiv.autCongr definition

(ϕ : A₁ ≃ₐ[R] A₂) : (A₁ ≃ₐ[R] A₁) ≃* A₂ ≃ₐ[R] A₂

Full source

/-- An algebra isomorphism induces a group isomorphism between automorphism groups.

This is a more bundled version of `AlgEquiv.equivCongr`. -/
@[simps apply]
def autCongr (ϕ : A₁ ≃ₐ[R] A₂) : (A₁ ≃ₐ[R] A₁) ≃* A₂ ≃ₐ[R] A₂ where
  __ := equivCongr ϕ ϕ
  toFun ψ := ϕ.symm.trans (ψ.trans ϕ)
  invFun ψ := ϕ.trans (ψ.trans ϕ.symm)
  map_mul' ψ χ := by
    ext
    simp only [mul_apply, trans_apply, symm_apply_apply]

Conjugation of $R$-algebra automorphism groups via an isomorphism

Informal description

Given an $R$-algebra isomorphism $\phi: A_1 \simeq_{alg[R]} A_2$, the function `autCongr` constructs a multiplicative equivalence between the automorphism groups $(A_1 \simeq_{alg[R]} A_1)$ and $(A_2 \simeq_{alg[R]} A_2)$. Specifically, for any automorphism $\psi: A_1 \simeq_{alg[R]} A_1$, the corresponding automorphism of $A_2$ is given by the composition $\phi^{-1} \circ \psi \circ \phi$, and conversely, any automorphism of $A_2$ can be transformed back to an automorphism of $A_1$ via $\phi \circ \psi \circ \phi^{-1}$. This equivalence preserves the group structure, meaning it respects the composition of automorphisms.

AlgEquiv.autCongr_refl theorem

: autCongr AlgEquiv.refl = MulEquiv.refl (A₁ ≃ₐ[R] A₁)

Full source

@[simp]
theorem autCongr_refl : autCongr AlgEquiv.refl = MulEquiv.refl (A₁ ≃ₐ[R] A₁) := rfl

Identity Conjugation Preserves Automorphism Group Identity

Informal description

The conjugation of the automorphism group of an $R$-algebra $A_1$ by the identity $R$-algebra isomorphism $\mathrm{refl}: A_1 \simeq_{alg[R]} A_1$ is equal to the multiplicative identity isomorphism on the automorphism group $(A_1 \simeq_{alg[R]} A_1)$. In other words, the map $\mathrm{autCongr}(\mathrm{refl})$ is the identity map on the group of $R$-algebra automorphisms of $A_1$.

AlgEquiv.autCongr_symm theorem

(ϕ : A₁ ≃ₐ[R] A₂) : (autCongr ϕ).symm = autCongr ϕ.symm

Full source

@[simp]
theorem autCongr_symm (ϕ : A₁ ≃ₐ[R] A₂) : (autCongr ϕ).symm = autCongr ϕ.symm :=
  rfl

Inverse of Automorphism Conjugation via Algebra Isomorphism

Informal description

Given an $R$-algebra isomorphism $\phi: A_1 \simeq_{alg[R]} A_2$, the inverse of the automorphism conjugation map $\text{autCongr}(\phi)$ is equal to the automorphism conjugation map of the inverse isomorphism $\phi^{-1}$. In other words, $(\text{autCongr}(\phi))^{-1} = \text{autCongr}(\phi^{-1})$.

AlgEquiv.autCongr_trans theorem

(ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₂ ≃ₐ[R] A₃) : (autCongr ϕ).trans (autCongr ψ) = autCongr (ϕ.trans ψ)

Full source

@[simp]
theorem autCongr_trans (ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₂ ≃ₐ[R] A₃) :
    (autCongr ϕ).trans (autCongr ψ) = autCongr (ϕ.trans ψ) :=
  rfl

Compatibility of Automorphism Group Conjugation with Composition of Algebra Isomorphisms

Informal description

Given $R$-algebra isomorphisms $\phi: A_1 \simeq_{alg[R]} A_2$ and $\psi: A_2 \simeq_{alg[R]} A_3$, the composition of the induced automorphism group equivalences $\text{autCongr}(\phi)$ and $\text{autCongr}(\psi)$ is equal to the equivalence induced by the composition $\phi \circ \psi$. That is, $(\text{autCongr}(\phi)) \circ (\text{autCongr}(\psi)) = \text{autCongr}(\phi \circ \psi)$.

AlgEquiv.applyMulSemiringAction instance

: MulSemiringAction (A₁ ≃ₐ[R] A₁) A₁

Full source

/-- The tautological action by `A₁ ≃ₐ[R] A₁` on `A₁`.

This generalizes `Function.End.applyMulAction`. -/
instance applyMulSemiringAction : MulSemiringAction (A₁ ≃ₐ[R] A₁) A₁ where
  smul := (· <| ·)
  smul_zero := map_zero
  smul_add := map_add
  smul_one := map_one
  smul_mul := map_mul
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

Action of Algebra Automorphisms by Evaluation

Informal description

The group of $R$-algebra automorphisms of an $R$-algebra $A_1$ acts on $A_1$ by semiring homomorphisms. Specifically, for any automorphism $f \in A_1 \simeq_{alg[R]} A_1$ and element $a \in A_1$, the action is defined by $f \cdot a = f(a)$.

AlgEquiv.smul_def theorem

(f : A₁ ≃ₐ[R] A₁) (a : A₁) : f • a = f a

Full source

@[simp]
protected theorem smul_def (f : A₁ ≃ₐ[R] A₁) (a : A₁) : f • a = f a :=
  rfl

Action of Algebra Automorphism via Evaluation: $f \cdot a = f(a)$

Informal description

For any $R$-algebra automorphism $f \colon A_1 \to A_1$ and any element $a \in A_1$, the scalar multiplication action of $f$ on $a$ is equal to the evaluation of $f$ at $a$, i.e., $f \cdot a = f(a)$.

AlgEquiv.apply_faithfulSMul instance

: FaithfulSMul (A₁ ≃ₐ[R] A₁) A₁

Full source

instance apply_faithfulSMul : FaithfulSMul (A₁ ≃ₐ[R] A₁) A₁ :=
  ⟨AlgEquiv.ext⟩

Faithful Action of Algebra Automorphisms by Evaluation

Informal description

The group of $R$-algebra automorphisms of an $R$-algebra $A_1$ acts faithfully on $A_1$ via evaluation. That is, the action $(f, a) \mapsto f(a)$ is injective in the first argument.

AlgEquiv.apply_smulCommClass instance

{S} [SMul S R] [SMul S A₁] [IsScalarTower S R A₁] : SMulCommClass S (A₁ ≃ₐ[R] A₁) A₁

Full source

instance apply_smulCommClass {S} [SMul S R] [SMul S A₁] [IsScalarTower S R A₁] :
    SMulCommClass S (A₁ ≃ₐ[R] A₁) A₁ where
  smul_comm r e a := (e.toLinearEquiv.map_smul_of_tower r a).symm

Commutation of Scalar Multiplication with Algebra Automorphisms in a Scalar Tower

Informal description

For any scalar multiplication action of $S$ on $R$ and $A_1$, and given that $S$, $R$, and $A_1$ form a scalar tower (i.e., the scalar multiplication by $S$ on $A_1$ factors through $R$), the scalar multiplications by $S$ and by $R$-algebra automorphisms of $A_1$ on $A_1$ commute with each other. More precisely, for any $s \in S$, $f \in A_1 \simeq_{alg[R]} A_1$, and $a \in A_1$, we have $s \cdot (f \cdot a) = f \cdot (s \cdot a)$.

AlgEquiv.apply_smulCommClass' instance

{S} [SMul S R] [SMul S A₁] [IsScalarTower S R A₁] : SMulCommClass (A₁ ≃ₐ[R] A₁) S A₁

Full source

instance apply_smulCommClass' {S} [SMul S R] [SMul S A₁] [IsScalarTower S R A₁] :
    SMulCommClass (A₁ ≃ₐ[R] A₁) S A₁ :=
  SMulCommClass.symm _ _ _

Commutation of Algebra Automorphisms and Scalar Multiplication in a Scalar Tower

Informal description

For any scalar multiplication action of $S$ on $R$ and $A_1$, and given that $S$, $R$, and $A_1$ form a scalar tower (i.e., the scalar multiplication by $S$ on $A_1$ factors through $R$), the scalar multiplications by $R$-algebra automorphisms of $A_1$ and by $S$ on $A_1$ commute with each other. More precisely, for any $f \in A_1 \simeq_{alg[R]} A_1$, $s \in S$, and $a \in A_1$, we have $f \cdot (s \cdot a) = s \cdot (f \cdot a)$.

AlgEquiv.instMulDistribMulActionUnits instance

: MulDistribMulAction (A₁ ≃ₐ[R] A₁) A₁ˣ

Full source

instance : MulDistribMulAction (A₁ ≃ₐ[R] A₁) A₁ˣ where
  smul := fun f => Units.map f
  one_smul := fun x => by ext; rfl
  mul_smul := fun x y z => by ext; rfl
  smul_mul := fun x y z => by ext; exact map_mul x _ _
  smul_one := fun x => by ext; exact map_one x

Multiplicative Distributive Action of $R$-Algebra Automorphisms on Units

Informal description

The group of $R$-algebra automorphisms of an $R$-algebra $A_1$ acts multiplicatively and distributively on the group of units $A_1^\times$ of $A_1$. This means that for any automorphism $f \in \text{Aut}_{R}(A_1)$ and any units $x, y \in A_1^\times$, the action satisfies $f \cdot (x * y) = (f \cdot x) * (f \cdot y)$.

AlgEquiv.smul_units_def theorem

(f : A₁ ≃ₐ[R] A₁) (x : A₁ˣ) : f • x = Units.map f x

Full source

@[simp]
theorem smul_units_def (f : A₁ ≃ₐ[R] A₁) (x : A₁ˣ) :
    f • x = Units.map f x := rfl

Action of $R$-algebra automorphisms on units via $\text{Units.map}$

Informal description

For any $R$-algebra automorphism $f \colon A_1 \to A_1$ and any unit $x \in A_1^\times$, the action of $f$ on $x$ is equal to the image of $x$ under the induced group homomorphism $\text{Units.map}\, f \colon A_1^\times \to A_1^\times$. In other words, $f \cdot x = \text{Units.map}\, f\, x$.

MulSemiringAction.toRingEquiv_algEquiv theorem

(σ : A₁ ≃ₐ[R] A₁) : MulSemiringAction.toRingEquiv _ A₁ σ = σ

Full source

@[simp]
lemma _root_.MulSemiringAction.toRingEquiv_algEquiv (σ : A₁ ≃ₐ[R] A₁) :
    MulSemiringAction.toRingEquiv _ A₁ σ = σ := rfl

$R$-algebra automorphism coincides with its induced ring automorphism

Informal description

For any $R$-algebra automorphism $\sigma \colon A_1 \simeq_{alg[R]} A_1$ of an $R$-algebra $A_1$, the ring automorphism obtained via the multiplicative semiring action coincides with $\sigma$ itself. In other words, the canonical map from $R$-algebra automorphisms to ring automorphisms is the identity on $\sigma$.

AlgEquiv.algebraMap_eq_apply theorem

(e : A₁ ≃ₐ[R] A₂) {y : R} {x : A₁} : algebraMap R A₂ y = e x ↔ algebraMap R A₁ y = x

Full source

@[simp]
theorem algebraMap_eq_apply (e : A₁ ≃ₐ[R] A₂) {y : R} {x : A₁} :
    algebraMapalgebraMap R A₂ y = e x ↔ algebraMap R A₁ y = x :=
  ⟨fun h => by simpa using e.symm.toAlgHom.algebraMap_eq_apply h, fun h =>
    e.toAlgHom.algebraMap_eq_apply h⟩

Equivalence of Algebra Map Conditions under $R$-Algebra Isomorphism

Informal description

Let $R$ be a commutative semiring, and let $A_1$ and $A_2$ be semirings equipped with $R$-algebra structures. Given an $R$-algebra isomorphism $e \colon A_1 \simeq_{R} A_2$, an element $y \in R$, and an element $x \in A_1$, the following equivalence holds: \[ \text{algebraMap}_{R \to A_2}(y) = e(x) \quad \text{if and only if} \quad \text{algebraMap}_{R \to A_1}(y) = x. \] Here, $\text{algebraMap}_{R \to A_i}$ denotes the canonical $R$-algebra structure map from $R$ to $A_i$ for $i = 1, 2$.

AlgEquiv.toLinearMapHom definition

(R A) [CommSemiring R] [Semiring A] [Algebra R A] : (A ≃ₐ[R] A) →* A →ₗ[R] A

Full source

/-- `AlgEquiv.toLinearMap` as a `MonoidHom`. -/
@[simps]
def toLinearMapHom (R A) [CommSemiring R] [Semiring A] [Algebra R A] :
    (A ≃ₐ[R] A) →* A →ₗ[R] A where
  toFun := AlgEquiv.toLinearMap
  map_one' := rfl
  map_mul' := fun _ _ ↦ rfl

Monoid homomorphism from $R$-algebra automorphisms to linear maps

Informal description

The function maps an $R$-algebra automorphism $\sigma \colon A \simeq_{alg[R]} A$ to its underlying $R$-linear map $\sigma \colon A \to_{lin[R]} A$, forming a monoid homomorphism from the group of $R$-algebra automorphisms of $A$ to the multiplicative monoid of $R$-linear endomorphisms of $A$.

AlgEquiv.pow_toLinearMap theorem

(σ : A₁ ≃ₐ[R] A₁) (n : ℕ) : (σ ^ n).toLinearMap = σ.toLinearMap ^ n

Full source

lemma pow_toLinearMap (σ : A₁ ≃ₐ[R] A₁) (n : ℕ) :
    (σ ^ n).toLinearMap = σ.toLinearMap ^ n :=
  (AlgEquiv.toLinearMapHom R A₁).map_pow σ n

Power of $R$-algebra automorphism's linear map equals linear map of power automorphism

Informal description

Let $A_1$ be an $R$-algebra and $\sigma \colon A_1 \simeq_{alg[R]} A_1$ be an $R$-algebra automorphism. For any natural number $n$, the underlying linear map of the $n$-th power automorphism $\sigma^n$ is equal to the $n$-th power of the underlying linear map of $\sigma$, i.e., \[ (\sigma^n).toLinearMap = (\sigma.toLinearMap)^n. \]

AlgEquiv.one_toLinearMap theorem

: (1 : A₁ ≃ₐ[R] A₁).toLinearMap = 1

Full source

@[simp]
lemma one_toLinearMap :
    (1 : A₁ ≃ₐ[R] A₁).toLinearMap = 1 := rfl

Identity Automorphism's Linear Map is Identity

Informal description

For any $R$-algebra $A_1$, the underlying linear map of the identity $R$-algebra automorphism $1 \colon A_1 \simeq_{alg[R]} A_1$ is equal to the identity linear map $1 \colon A_1 \to_{lin[R]} A_1$.

AlgEquiv.algHomUnitsEquiv definition

(R S : Type*) [CommSemiring R] [Semiring S] [Algebra R S] : (S →ₐ[R] S)ˣ ≃* (S ≃ₐ[R] S)

Full source

/-- The units group of `S →ₐ[R] S` is `S ≃ₐ[R] S`.
See `LinearMap.GeneralLinearGroup.generalLinearEquiv` for the linear map version. -/
@[simps]
def algHomUnitsEquiv (R S : Type*) [CommSemiring R] [Semiring S] [Algebra R S] :
    (S →ₐ[R] S)ˣ(S →ₐ[R] S)ˣ ≃* (S ≃ₐ[R] S) where
  toFun := fun f ↦
    { (f : S →ₐ[R] S) with
      invFun := ↑(f⁻¹)
      left_inv := (fun x ↦ show (↑(f⁻¹ * f) : S →ₐ[R] S) x = x by rw [inv_mul_cancel]; rfl)
      right_inv := (fun x ↦ show (↑(f * f⁻¹) : S →ₐ[R] S) x = x by rw [mul_inv_cancel]; rfl) }
  invFun := fun f ↦ ⟨f, f.symm, f.comp_symm, f.symm_comp⟩
  left_inv := fun _ ↦ rfl
  right_inv := fun _ ↦ rfl
  map_mul' := fun _ _ ↦ rfl

Equivalence between invertible $R$-algebra endomorphisms and $R$-algebra automorphisms

Informal description

The group of units of the $R$-algebra endomorphisms of $S$ is isomorphic as a group to the group of $R$-algebra automorphisms of $S$. More precisely, there is a multiplicative equivalence between: 1. The group of invertible elements in the monoid of $R$-algebra endomorphisms $S \to_{alg[R]} S$ 2. The group of $R$-algebra automorphisms $S \simeq_{alg[R]} S$ The equivalence maps: - An invertible endomorphism $f$ to the automorphism with inverse $f^{-1}$ - An automorphism $f$ to the pair $(f, f^{-1})$ as an invertible endomorphism

Finite.algEquiv instance

[Finite (A₁ →ₐ[R] A₂)] : Finite (A₁ ≃ₐ[R] A₂)

Full source

/-- See also `Finite.algHom` -/
instance _root_.Finite.algEquiv [Finite (A₁ →ₐ[R] A₂)] : Finite (A₁ ≃ₐ[R] A₂) :=
  Finite.of_injective _ AlgEquiv.coe_algHom_injective

Finiteness of $R$-Algebra Isomorphisms from Finiteness of $R$-Algebra Homomorphisms

Informal description

For any commutative semiring $R$ and semirings $A_1$, $A_2$ equipped with $R$-algebra structures, if the type of $R$-algebra homomorphisms from $A_1$ to $A_2$ is finite, then the type of $R$-algebra isomorphisms between $A_1$ and $A_2$ is also finite.

MulSemiringAction.toAlgEquiv definition

(g : G) : A ≃ₐ[R] A

Full source

/-- Each element of the group defines an algebra equivalence.

This is a stronger version of `MulSemiringAction.toRingEquiv` and
`DistribMulAction.toLinearEquiv`. -/
@[simps! apply symm_apply toEquiv]
def toAlgEquiv (g : G) : A ≃ₐ[R] A :=
  { MulSemiringAction.toRingEquiv _ _ g, MulSemiringAction.toAlgHom R A g with }

$R$-algebra automorphism induced by group action

Informal description

For a group $G$ acting multiplicatively on an $R$-algebra $A$, each element $g \in G$ defines an $R$-algebra automorphism of $A$. This automorphism preserves both the ring structure (addition and multiplication) and the scalar multiplication by elements of $R$.

MulSemiringAction.toAlgEquiv_injective theorem

[FaithfulSMul G A] : Function.Injective (MulSemiringAction.toAlgEquiv R A : G → A ≃ₐ[R] A)

Full source

theorem toAlgEquiv_injective [FaithfulSMul G A] :
    Function.Injective (MulSemiringAction.toAlgEquiv R A : G → A ≃ₐ[R] A) := fun _ _ h =>
  eq_of_smul_eq_smul fun r => AlgEquiv.ext_iff.1 h r

Injectivity of Group Action Induced $R$-Algebra Automorphisms

Informal description

Let $G$ be a group acting faithfully on an $R$-algebra $A$ via multiplicative semiring actions. Then the map that sends each group element $g \in G$ to its induced $R$-algebra automorphism $\text{toAlgEquiv}_R A(g) : A \simeq_{alg[R]} A$ is injective.

MulSemiringAction.toAlgAut definition

: G →* A ≃ₐ[R] A

Full source

/-- Each element of the group defines an algebra equivalence.

This is a stronger version of `MulSemiringAction.toRingAut` and
`DistribMulAction.toModuleEnd`. -/
@[simps]
def toAlgAut : G →* A ≃ₐ[R] A where
  toFun := toAlgEquiv R A
  map_one' := AlgEquiv.ext <| one_smul _
  map_mul' g h := AlgEquiv.ext <| mul_smul g h

Group homomorphism to $R$-algebra automorphisms induced by multiplicative action

Informal description

Given a group $G$ acting multiplicatively on an $R$-algebra $A$, the function maps each element $g \in G$ to an $R$-algebra automorphism of $A$ that preserves both the ring structure and the scalar multiplication by elements of $R$. This mapping is a group homomorphism from $G$ to the group of $R$-algebra automorphisms of $A$. More precisely, the function satisfies: - $f(1_G) = \text{id}_A$ (preserves the identity) - $f(g \cdot h) = f(g) \circ f(h)$ for all $g, h \in G$ (preserves the group operation) where $f(g)$ denotes the $R$-algebra automorphism corresponding to $g \in G$.

Mathlib.Algebra.Algebra.Equiv

Main definitions

Notations