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 OrderedRing, OrderedCommRing, LinearOrderedRing, toLinearOrderedCommRing is again an ordering ring

@[instance 75]

instance SubringClass.toOrderedRing {R : Type u_1} {S : Type u_2} [SetLike S R] (s : S) [OrderedRing R] [SubringClass S R] : OrderedRing ↥s

A subring of an OrderedRing is an OrderedRing.

Equations

• SubringClass.toOrderedRing s = OrderedRing.mk ⋯ ⋯ ⋯

@[instance 75]

instance SubringClass.toOrderedCommRing {R : Type u_1} {S : Type u_2} [SetLike S R] (s : S) [OrderedCommRing R] [SubringClass S R] : OrderedCommRing ↥s

A subring of an OrderedCommRing is an OrderedCommRing.

Equations

• SubringClass.toOrderedCommRing s = OrderedCommRing.mk ⋯

@[instance 75]

instance SubringClass.toLinearOrderedRing {R : Type u_1} {S : Type u_2} [SetLike S R] (s : S) [LinearOrderedRing R] [SubringClass S R] : LinearOrderedRing ↥s

A subring of a LinearOrderedRing is a LinearOrderedRing.

Equations

• SubringClass.toLinearOrderedRing s = LinearOrderedRing.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

@[instance 75]

instance SubringClass.toLinearOrderedCommRing {R : Type u_1} {S : Type u_2} [SetLike S R] (s : S) [LinearOrderedCommRing R] [SubringClass S R] : LinearOrderedCommRing ↥s

A subring of a LinearOrderedCommRing is a LinearOrderedCommRing.

Equations

• SubringClass.toLinearOrderedCommRing s = LinearOrderedCommRing.mk ⋯

instance Subring.toOrderedRing {R : Type u_1} [OrderedRing R] (s : Subring R) : OrderedRing ↥s

A subring of an OrderedRing is an OrderedRing.

Equations

• s.toOrderedRing = SubringClass.toOrderedRing s

instance Subring.toOrderedCommRing {R : Type u_1} [OrderedCommRing R] (s : Subring R) : OrderedCommRing ↥s

A subring of an OrderedCommRing is an OrderedCommRing.

Equations

• s.toOrderedCommRing = SubringClass.toOrderedCommRing s

instance Subring.toLinearOrderedRing {R : Type u_1} [LinearOrderedRing R] (s : Subring R) : LinearOrderedRing ↥s

A subring of a LinearOrderedRing is a LinearOrderedRing.

Equations

• s.toLinearOrderedRing = SubringClass.toLinearOrderedRing s

instance Subring.toLinearOrderedCommRing {R : Type u_1} [LinearOrderedCommRing R] (s : Subring R) : LinearOrderedCommRing ↥s

A subring of a LinearOrderedCommRing is a LinearOrderedCommRing.

Equations

• s.toLinearOrderedCommRing = SubringClass.toLinearOrderedCommRing s

def Subring.orderedSubtype {R : Type u_2} [OrderedRing 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_2} [OrderedRing R] (s : Subring R) : ↑s.orderedSubtype = s.subtype