(Semi)ring equivs #
In this file we define an extension of Equiv
called RingEquiv
, which is a datatype representing
an isomorphism of Semiring
s, Ring
s, DivisionRing
s, or Field
s.
Notations #
infixl ` ≃+* `:25 := RingEquiv
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 RingEquiv
now avoid the unbundled isMulHom
and isAddHom
, as these are
deprecated.
Definition of multiplication in the groups of automorphisms agrees with function composition,
multiplication in Equiv.Perm
, and multiplication in CategoryTheory.End
, not with
CategoryTheory.CategoryStruct.comp
.
Tags #
Equiv, MulEquiv, AddEquiv, RingEquiv, MulAut, AddAut, RingAut
makes a NonUnitalRingHom
from the bijective inverse of a NonUnitalRingHom
Instances For
makes a RingHom
from the bijective inverse of a RingHom
Instances For
- toFun : R → S
- invFun : S → R
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
- map_mul' : ∀ (x y : R), Equiv.toFun s.toEquiv (x * y) = Equiv.toFun s.toEquiv x * Equiv.toFun s.toEquiv y
The proposition that the function preserves multiplication
- map_add' : ∀ (x y : R), Equiv.toFun s.toEquiv (x + y) = Equiv.toFun s.toEquiv x + Equiv.toFun s.toEquiv y
The proposition that the function preserves addition
An equivalence between two (non-unital non-associative semi)rings that preserves the algebraic structure.
Instances For
- coe : F → R → S
- inv : F → S → R
- left_inv : ∀ (e : F), Function.LeftInverse (EquivLike.inv e) (EquivLike.coe e)
- right_inv : ∀ (e : F), Function.RightInverse (EquivLike.inv e) (EquivLike.coe e)
- coe_injective' : ∀ (e g : F), EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.inv g → e = g
By definition, a ring isomorphism preserves the additive structure.
RingEquivClass F R S
states that F
is a type of ring structure preserving equivalences.
You should extend this class when you extend RingEquiv
.
Instances
Turn an element of a type F
satisfying RingEquivClass F α β
into an actual
RingEquiv
. This is declared as the default coercion from F
to α ≃+* β
.
Instances For
Any type satisfying RingEquivClass
can be cast into RingEquiv
via
RingEquivClass.toRingEquiv
.
A non-unital commutative ring is isomorphic to its opposite.
Instances For
A ring isomorphism sends zero to zero.
Produce a ring isomorphism from a bijective ring homomorphism.
Instances For
A family of ring isomorphisms ∀ j, (R j ≃+* S j)
generates a
ring isomorphisms between ∀ j, R j
and ∀ j, S j
.
This is the RingEquiv
version of Equiv.piCongrRight
, and the dependent version of
RingEquiv.arrowCongr
.
Instances For
A ring isomorphism sends one to one.
RingEquiv.coe_mulEquiv_refl
and RingEquiv.coe_addEquiv_refl
are proved above
in higher generality
RingEquiv.coe_mulEquiv_trans
and RingEquiv.coe_addEquiv_trans
are proved above
in higher generality
Reinterpret a ring equivalence as a non-unital ring homomorphism.
Instances For
Reinterpret a ring equivalence as a ring homomorphism.
Instances For
The two paths coercion can take to a NonUnitalRingEquiv
are equivalent
Reinterpret a ring equivalence as a monoid homomorphism.
Instances For
Reinterpret a ring equivalence as an AddMonoid
homomorphism.
Instances For
The two paths coercion can take to an AddMonoidHom
are equivalent
The two paths coercion can take to a MonoidHom
are equivalent
The two paths coercion can take to an Equiv
are equivalent
Construct an equivalence of rings from homomorphisms in both directions, which are inverses.
Instances For
Construct an equivalence of rings from unital homomorphisms in both directions, which are inverses.
Instances For
If two rings are isomorphic, and the second doesn't have zero divisors, then so does the first.