Zulip Chat Archive

Stream: maths

Topic: local rings


Johan Commelin (Mar 05 2019 at 18:08):

@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 (Mar 05 2019 at 19:22):

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

Mario Carneiro (Mar 05 2019 at 19:23):

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

Mario Carneiro (Mar 05 2019 at 19:24):

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

Johan Commelin (Mar 07 2019 at 08:51):

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


Last updated: Dec 20 2023 at 11:08 UTC