(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
Equations
Instances For
makes a RingHom
from the bijective inverse of a RingHom
Equations
Instances For
An equivalence between two (non-unital non-associative semi)rings that preserves the algebraic structure.
- toFun : R → S
- invFun : S → R
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
Instances For
RingEquivClass F R S
states that F
is a type of ring structure preserving equivalences.
You should extend this class when you extend RingEquiv
.
By definition, a ring isomorphism preserves the additive structure.
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 α ≃+* β
.
Equations
Instances For
Any type satisfying RingEquivClass
can be cast into RingEquiv
via
RingEquivClass.toRingEquiv
.
Equations
Alias of RingEquiv.coe_refl
.
Auxiliary definition to avoid looping in dsimp
with RingEquiv.symm_mk
.
Equations
Instances For
A non-unital commutative ring is isomorphic to its opposite.
Equations
Instances For
A ring isomorphism sends zero to zero.
Produce a ring isomorphism from a bijective ring homomorphism.
Equations
Instances For
Product of a singleton family of (non-unital non-associative semi)rings is isomorphic to the only member of this family.
Equations
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
.
Equations
Instances For
Transport dependent functions through an equivalence of the base space.
This is Equiv.piCongrLeft'
as a RingEquiv
.
Equations
Instances For
Transport dependent functions through an equivalence of the base space.
This is Equiv.piCongrLeft
as a RingEquiv
.
Equations
Instances For
Splits the indices of ring ∀ (i : ι), Y i
along the predicate p
. This is
Equiv.piEquivPiSubtypeProd
as a RingEquiv
.
Equations
Instances For
Product of ring equivalences. This is Equiv.prodCongr
as a RingEquiv
.
Equations
Instances For
This is Equiv.piOptionEquivProd
as a RingEquiv
.
Equations
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.
Equations
Instances For
Reinterpret a ring equivalence as a ring homomorphism.
Equations
Instances For
The two paths coercion can take to a NonUnitalRingEquiv
are equivalent
Reinterpret a ring equivalence as a monoid homomorphism.
Equations
Instances For
Reinterpret a ring equivalence as an AddMonoid
homomorphism.
Equations
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.
Equations
Instances For
Construct an equivalence of rings from unital homomorphisms in both directions, which are inverses.
Equations
Instances For
Gives a RingEquiv
from an element of a MulEquivClass
preserving addition.
Equations
Instances For
Gives a RingEquiv
from an element of an AddEquivClass
preserving addition.
Equations
Instances For
If a ring homomorphism has an inverse, it is a ring isomorphism.
Equations
Instances For
If two rings are isomorphic, and the second doesn't have zero divisors, then so does the first.