(Semi)ring equivs
In this file we define extension of equiv called ring_equiv, which is a datatype representing an
isomorphism of semirings, rings, division_rings, or fields. We also introduce the
corresponding group of automorphisms ring_aut.
Notations
The extended equiv have coercions to functions, and the coercion is the canonical notation when treating the isomorphism as maps.
Implementation notes
The fields for ring_equiv now avoid the unbundled is_mul_hom and is_add_hom, as these are
deprecated.
Definition of multiplication in the groups of automorphisms agrees with function composition,
multiplication in equiv.perm, and multiplication in category_theory.End, not with
category_theory.comp.
Tags
equiv, mul_equiv, add_equiv, ring_equiv, mul_aut, add_aut, ring_aut
Equations
- ring_equiv.has_coe_to_fun = {F := λ (x : R ≃+* S), R → S, coe := ring_equiv.to_fun _inst_4}
Equations
- ring_equiv.has_coe_to_mul_equiv = {coe := ring_equiv.to_mul_equiv _inst_4}
Equations
- ring_equiv.has_coe_to_add_equiv = {coe := ring_equiv.to_add_equiv _inst_4}
The identity map is a ring isomorphism.
Equations
- ring_equiv.refl R = {to_fun := (mul_equiv.refl R).to_fun, inv_fun := (mul_equiv.refl R).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
The inverse of a ring isomorphism is a ring isomorphism.
Transitivity of ring_equiv.
Equations
- e₁.trans e₂ = {to_fun := (e₁.to_mul_equiv.trans e₂.to_mul_equiv).to_fun, inv_fun := (e₁.to_mul_equiv.trans e₂.to_mul_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
A commutative ring is isomorphic to its opposite.
Equations
- ring_equiv.to_opposite R = {to_fun := opposite.equiv_to_opposite.to_fun, inv_fun := opposite.equiv_to_opposite.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
Produce a ring isomorphism from a bijective ring homomorphism.
Equations
- ring_equiv.of_bijective f hf = {to_fun := (equiv.of_bijective ⇑f hf).to_fun, inv_fun := (equiv.of_bijective ⇑f hf).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
Reinterpret a ring equivalence as a ring homomorphism.
Equations
- e.to_ring_hom = {to_fun := e.to_mul_equiv.to_monoid_hom.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
Equations
- ring_equiv.has_coe_to_ring_hom = {coe := ring_equiv.to_ring_hom _inst_2}
Reinterpret a ring equivalence as an add_monoid homomorphism.
Gives a ring_equiv from a mul_equiv preserving addition.
If two rings are isomorphic, and the second is an integral domain, then so is the first.
If two rings are isomorphic, and the second is an integral domain, then so is the first.
Equations
- ring_equiv.integral_domain B e = {add := ring.add _inst_5, add_assoc := _, zero := ring.zero _inst_5, zero_add := _, add_zero := _, neg := ring.neg _inst_5, add_left_neg := _, add_comm := _, mul := ring.mul _inst_5, mul_assoc := _, one := ring.one _inst_5, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
The group operation on automorphisms of a ring is defined by λ g h, ring_equiv.trans h g. This means that multiplication agrees with composition, (g*h)(x) = g (h x) .
Equations
- ring_aut.group R = {mul := λ (g h : R ≃+* R), h.trans g, mul_assoc := _, one := ring_equiv.refl R _inst_2, one_mul := _, mul_one := _, inv := ring_equiv.symm _inst_2, mul_left_inv := _}
Equations
- ring_aut.inhabited R = {default := 1}
Monoid homomorphism from ring automorphisms to additive automorphisms.
Equations
- ring_aut.to_add_aut R = {to_fun := ring_equiv.to_add_equiv _inst_2, map_one' := _, map_mul' := _}
Monoid homomorphism from ring automorphisms to multiplicative automorphisms.
Equations
- ring_aut.to_mul_aut R = {to_fun := ring_equiv.to_mul_equiv _inst_2, map_one' := _, map_mul' := _}
Monoid homomorphism from ring automorphisms to permutations.
Equations
- ring_aut.to_perm R = {to_fun := ring_equiv.to_equiv _inst_2, map_one' := _, map_mul' := _}