Documentation

TauCeti.Algebra.Ring.Opposite

Inverse pairs for the double-opposite ring equivalence #

The canonical equivalence RingEquiv.opOp A identifies a semiring with its double opposite. The inverse-pair instances here allow semilinear maps along this equivalence to invert and compose.

source
instance TauCeti.opOpRingHomInvPair (A : Type u_1) [Semiring A] :
RingHomInvPair ↑(RingEquiv.opOp A) ↑(RingEquiv.opOp A).symm

The canonical double-opposite ring equivalence and its inverse form an inverse pair.

source
instance TauCeti.opOpRingHomInvPairSymm (A : Type u_1) [Semiring A] :
RingHomInvPair ↑(RingEquiv.opOp A).symm ↑(RingEquiv.opOp A)

The inverse double-opposite ring equivalence and the forward equivalence form an inverse pair.