inhabited subrings?

Stream: general

[Kevin Buzzard]

import ring_theory.subring.basic

example (R : Type*) [ring R] (S : subring R) : inhabited S := infer_instance -- fails

instance do_we_actually_want_this (R : Type*) [ring R] (S : subring R) : inhabited S := ⟨0⟩

example (R : Type*) [ring R] (S : subring R) : inhabited S := infer_instance -- works

A @[derive inhabited] was failing for me because this instance was missing. Do we want it for general sub-algebraic-objects or is this somehow ridiculous? The coerced subring is a ring, so...oh! rings aren't inhabited?

import ring_theory.subring.basic

@[to_additive what_about_this_additive_version]
instance what_about_this (S : Type*) [monoid S] : inhabited S := ⟨1⟩

example (R : Type*) [ring R] (S : subring R) : inhabited S := infer_instance -- works

ha ha this creates a diamond on semirings though! Is this why we don't have it?

[Eric Wieser]

what_about_this is a bad instance, the other one is good

[Reid Barton]

What's the rule here? 0 is okay but not 1?

[Yaël Dillies]

No, it's whether you're talking about subobjects or not.

[Reid Barton]

I see, that makes more sense.