(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≃+* `: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
The proposition that the function preserves multiplication
map_mul' : ∀ (x y : R), Equiv.toFun toEquiv (x * y) = Equiv.toFun toEquiv x * Equiv.toFun toEquiv yThe proposition that the function preserves addition
map_add' : ∀ (x y : R), Equiv.toFun toEquiv (x + y) = Equiv.toFun toEquiv x + Equiv.toFun toEquiv y
An equivalence between two (non-unital non-associative semi)rings that preserves the algebraic structure.
Instances For
Notation for RingEquiv
.
Equations
- «term_≃+*_» = Lean.ParserDescr.trailingNode `term_≃+*_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃+* ") (Lean.ParserDescr.cat `term 26))
The equivalence of additive monoids underlying an equivalence of (semi)rings.
Equations
- RingEquiv.toAddEquiv self = { toEquiv := self.toEquiv, map_add' := (_ : ∀ (x y : R), Equiv.toFun self.toEquiv (x + y) = Equiv.toFun self.toEquiv x + Equiv.toFun self.toEquiv y) }
The equivalence of multiplicative monoids underlying an equivalence of (semi)rings.
Equations
- RingEquiv.toMulEquiv self = { toEquiv := self.toEquiv, map_mul' := (_ : ∀ (x y : R), Equiv.toFun self.toEquiv (x * y) = Equiv.toFun self.toEquiv x * Equiv.toFun self.toEquiv y) }
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
Equations
- RingEquivClass.toAddEquivClass = AddEquivClass.mk (_ : ∀ (f : F) (a b : R), ↑f (a + b) = ↑f a + ↑f b)
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
- One or more equations did not get rendered due to their size.
Any type satisfying RingEquivClass
can be cast into RingEquiv
via
RingEquivClass.toRingEquiv
.
Equations
- instCoeTCRingEquiv = { coe := RingEquivClass.toRingEquiv }
Equations
- RingEquiv.instInhabitedRingEquiv R = { default := RingEquiv.refl R }
A non-unital commutative ring is isomorphic to its opposite.
Equations
- One or more equations did not get rendered due to their size.
A ring isomorphism sends zero to zero.
Produce a ring isomorphism from a bijective ring homomorphism.
Equations
- One or more equations did not get rendered due to their size.
A family of ring isomorphisms ∀ j, (R j ≃+* S j)∀ j, (R j ≃+* S j)≃+* S j)
generates a
ring isomorphisms between ∀ j, R j∀ j, R j
and ∀ j, S j∀ j, S j
.
This is the RingEquiv
version of Equiv.piCongrRight
, and the dependent version of
RingEquiv.arrowCongr
.
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
Equations
- RingEquiv.instCoeToNonUnitalRingHom = { coe := RingEquiv.toNonUnitalRingHom }
Reinterpret a ring equivalence as a ring homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Equations
- RingEquiv.instCoeToRingHom = { coe := RingEquiv.toRingHom }
The two paths coercion can take to a NonUnitalRingEquiv
are equivalent
Reinterpret a ring equivalence as a monoid homomorphism.
Equations
Reinterpret a ring equivalence as an AddMonoid
homomorphism.
Equations
The two paths coercion can take to an AddMonoidHom
are equivalent
The two paths coercion can take to an 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
- One or more equations did not get rendered due to their size.
Construct an equivalence of rings from unital homomorphisms in both directions, which are inverses.
Equations
- One or more equations did not get rendered due to their size.
Gives a RingEquiv
from an element of a MulEquivClass
preserving addition.
Equations
- One or more equations did not get rendered due to their size.
Gives a RingEquiv
from an element of an AddEquivClass
preserving addition.
Equations
- One or more equations did not get rendered due to their size.
If two rings are isomorphic, and the second doesn't have zero divisors, then so does the first.