Isomorphisms of R
-algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines bundled isomorphisms of R
-algebras.
Main definitions #
Notations #
- to_fun : A → B
- inv_fun : B → A
- left_inv : function.left_inverse self.inv_fun self.to_fun
- right_inv : function.right_inverse self.inv_fun self.to_fun
- map_mul' : ∀ (x y : A), self.to_fun (x * y) = self.to_fun x * self.to_fun y
- map_add' : ∀ (x y : A), self.to_fun (x + y) = self.to_fun x + self.to_fun y
- commutes' : ∀ (r : R), self.to_fun (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r
An equivalence of algebras is an equivalence of rings commuting with the actions of scalars.
Instances for alg_equiv
- alg_equiv.has_sizeof_inst
- alg_equiv_class.alg_equiv.has_coe_t
- alg_equiv.alg_equiv_class
- alg_equiv.has_coe_to_fun
- alg_equiv.has_coe_to_ring_equiv
- alg_equiv.inhabited
- alg_equiv.aut
- alg_equiv.apply_mul_semiring_action
- alg_equiv.apply_has_faithful_smul
- alg_equiv.apply_smul_comm_class
- alg_equiv.apply_smul_comm_class'
- alg_equiv.subsingleton_left
- alg_equiv.subsingleton_right
- alg_equiv.fintype
- krull_topology
- alg_equiv.topological_group
- coe : F → A → B
- inv : F → B → A
- left_inv : ∀ (e : F), function.left_inverse (alg_equiv_class.inv e) (alg_equiv_class.coe e)
- right_inv : ∀ (e : F), function.right_inverse (alg_equiv_class.inv e) (alg_equiv_class.coe e)
- coe_injective' : ∀ (e g : F), alg_equiv_class.coe e = alg_equiv_class.coe g → alg_equiv_class.inv e = alg_equiv_class.inv g → e = g
- map_mul : ∀ (f : F) (a b : A), ⇑f (a * b) = ⇑f a * ⇑f b
- map_add : ∀ (f : F) (a b : A), ⇑f (a + b) = ⇑f a + ⇑f b
- commutes : ∀ (f : F) (r : R), ⇑f (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r
alg_equiv_class F R A B
states that F
is a type of algebra structure preserving
equivalences. You should extend this class when you extend alg_equiv
.
Instances of this typeclass
Instances of other typeclasses for alg_equiv_class
- alg_equiv_class.has_sizeof_inst
Equations
- alg_equiv_class.to_alg_hom_class F R A B = {coe := coe_fn fun_like.has_coe_to_fun, coe_injective' := _, map_mul := _, map_one := _, map_add := _, map_zero := _, commutes := _}
Equations
- alg_equiv_class.to_linear_equiv_class F R A B = {coe := alg_equiv_class.coe h, inv := alg_equiv_class.inv h, left_inv := _, right_inv := _, coe_injective' := _, map_add := _, map_smulₛₗ := _}
Equations
- alg_equiv.alg_equiv_class = {coe := alg_equiv.to_fun _inst_6, inv := alg_equiv.inv_fun _inst_6, left_inv := _, right_inv := _, coe_injective' := _, map_mul := _, map_add := _, commutes := _}
Helper instance for when there's too many metavariables to apply
fun_like.has_coe_to_fun
directly.
Equations
- alg_equiv.has_coe_to_fun = {coe := alg_equiv.to_fun _inst_6}
Equations
- alg_equiv.has_coe_to_ring_equiv = {coe := alg_equiv.to_ring_equiv _inst_6}
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 alg_hom_class.has_coe_t
instance.
Algebra equivalences are reflexive.
Equations
- alg_equiv.inhabited = {default := alg_equiv.refl _inst_5}
See Note [custom simps projection]
Equations
- alg_equiv.simps.symm_apply e = ⇑(e.symm)
Algebra equivalences are transitive.
Equations
- e₁.trans e₂ = {to_fun := (e₁.to_ring_equiv.trans e₂.to_ring_equiv).to_fun, inv_fun := (e₁.to_ring_equiv.trans e₂.to_ring_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
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₂'
.
Equations
- e₁.arrow_congr e₂ = {to_fun := λ (f : A₁ →ₐ[R] A₂), (e₂.to_alg_hom.comp f).comp e₁.symm.to_alg_hom, inv_fun := λ (f : A₁' →ₐ[R] A₂'), (e₂.symm.to_alg_hom.comp f).comp e₁.to_alg_hom, left_inv := _, right_inv := _}
If an algebra morphism has an inverse, it is a algebra isomorphism.
Promotes a bijective algebra homomorphism to an algebra equivalence.
Upgrade a linear equivalence to an algebra equivalence, given that it distributes over multiplication and action of scalars.
Promotes a linear ring_equiv to an alg_equiv.
Equations
- alg_equiv.aut = {mul := λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ, mul_assoc := _, one := alg_equiv.refl _inst_5, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default alg_equiv.refl (λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ) alg_equiv.aut._proof_4 alg_equiv.aut._proof_5, npow_zero' := _, npow_succ' := _, inv := alg_equiv.symm _inst_5, div := div_inv_monoid.div._default (λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ) alg_equiv.aut._proof_8 alg_equiv.refl alg_equiv.aut._proof_9 alg_equiv.aut._proof_10 (div_inv_monoid.npow._default alg_equiv.refl (λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ) alg_equiv.aut._proof_4 alg_equiv.aut._proof_5) alg_equiv.aut._proof_11 alg_equiv.aut._proof_12 alg_equiv.symm, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default (λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ) alg_equiv.aut._proof_14 alg_equiv.refl alg_equiv.aut._proof_15 alg_equiv.aut._proof_16 (div_inv_monoid.npow._default alg_equiv.refl (λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ) alg_equiv.aut._proof_4 alg_equiv.aut._proof_5) alg_equiv.aut._proof_17 alg_equiv.aut._proof_18 alg_equiv.symm, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
The tautological action by A₁ ≃ₐ[R] A₁
on A₁
.
This generalizes function.End.apply_mul_action
.
Equations
- alg_equiv.apply_mul_semiring_action = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := λ (_x : A₁ ≃ₐ[R] A₁) (_y : A₁), ⇑_x _y}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, smul_one := _, smul_mul := _}
Each element of the group defines a algebra equivalence.
This is a stronger version of mul_semiring_action.to_ring_equiv
and
distrib_mul_action.to_linear_equiv
.
Equations
- mul_semiring_action.to_alg_equiv R A g = {to_fun := (mul_semiring_action.to_ring_equiv G A g).to_fun, inv_fun := (mul_semiring_action.to_ring_equiv G A g).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}