Subrings of ordered rings

We study subrings of ordered rings and prove their basic properties.

Main definitions and results

• Subring.orderedSubtype: the inclusion S → R of a subring as an ordered ring homomorphism
• various ordered instances: a subring of an IsOrderedRing or an IsStrictOrderRing is again the respective kind of ordered ring.

instance Subring.toIsOrderedRing {R : Type u_1} {S : Type u_2} [Ring R] [PartialOrder R] [SetLike S R] [SubringClass S R] [IsOrderedRing R] (s : S) : IsOrderedRing ↥s

A subring of an ordered ring is an ordered ring.

instance Subring.toIsStrictOrderedRing {R : Type u_1} {S : Type u_2} [Ring R] [PartialOrder R] [SetLike S R] [SubringClass S R] [IsStrictOrderedRing R] (s : S) : IsStrictOrderedRing ↥s

A subring of a strict ordered ring is a strict ordered ring.

def Subring.orderedSubtype {R : Type u_1} [Ring R] [PartialOrder R] (s : Subring R) : ↥s →+*o R

The inclusion S → R of a subring, as an ordered ring homomorphism.

Equations

• s.orderedSubtype = { toRingHom := s.subtype, monotone' := ⋯ }

theorem Subring.orderedSubtype_coe {R : Type u_1} [Ring R] [PartialOrder R] (s : Subring R) : ↑s.orderedSubtype = s.subtype