local rings

Stream: maths

[Johan Commelin]

@Mario Carneiro Is there a reason why you are not using the type class system for is_local_ring here?

def nonunits_ideal (h : is_local_ring α) : ideal α :=
{ carrier := nonunits α,
  zero := zero_mem_nonunits.2 h.zero_ne_one,
  add := begin
    rcases id h with ⟨M, mM, hM⟩,
    have : ∀ x ∈ nonunits α, x ∈ M,
    { intros x hx,
      rcases (ideal.span {x} : ideal α).exists_le_maximal _ with ⟨N, mN, hN⟩,
      { cases hM N mN,
        rwa [ideal.span_le, singleton_subset_iff] at hN },
      { exact mt ideal.span_singleton_eq_top.1 hx } },
    intros x y hx hy,
    exact coe_subset_nonunits mM.1 (M.add_mem (this _ hx) (this _ hy))
  end,
  smul := λ a x, mul_mem_nonunits_right }

[Mario Carneiro]

is is_local_ring a class? I don't think it was when I wrote that

[Mario Carneiro]

actually it might be one of those "not really a class" classes like nat.prime

[Mario Carneiro]

it's only used instance implicit when it needs to be for some other instance

[Johan Commelin]

@Mario Carneiro Hmmm, I see. What is the objection to treating this a an "actually really a class" class?