(Semi)ring equivs
In this file we define extension of equiv
called ring_equiv
, which is a datatype representing an
isomorphism of semiring
s, ring
s, division_ring
s, or field
s. 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
- to_fun : R → S
- inv_fun : S → R
- left_inv : function.left_inverse c.inv_fun c.to_fun
- right_inv : function.right_inverse c.inv_fun c.to_fun
- map_mul' : ∀ (x y : R), c.to_fun (x * y) = (c.to_fun x) * c.to_fun y
- map_add' : ∀ (x y : R), c.to_fun (x + y) = c.to_fun x + c.to_fun y
An equivalence between two (semi)rings that preserves the algebraic structure.
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' := _}
Equations
- ring_equiv.inhabited R = {default := ring_equiv.refl R _inst_2}
See Note [custom simps projection]
Equations
- ring_equiv.simps.inv_fun e = ⇑(e.symm)
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.
Construct an equivalence of rings from homomorphisms in both directions, which are inverses.
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, sub := ring.sub _inst_5, sub_eq_add_neg := _, 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 := _}
In a division ring K
, the unit group units K
is equivalent to the subtype of nonzero elements.