Zulip Chat Archive

Stream: general

Topic: local ring diamond?


view this post on Zulip Kenny Lau (Dec 19 2019 at 10:39):

import algebra.associated linear_algebra.basic order.zorn

universes u
variables {α : Type u}

section prio
set_option default_priority 100 -- see Note [default priority]
class local_ring (α : Type u) extends nonzero_comm_ring α :=
(is_local :  (a : α), (is_unit a)  (is_unit (1 - a)))
end prio

def is_local_ring (α : Type u) [comm_ring α] : Prop :=
((0:α)  1)   (a : α), (is_unit a)  (is_unit (1 - a))

def local_of_is_local_ring [comm_ring α] (h : is_local_ring α) : local_ring α :=
{ zero_ne_one := h.1,
  is_local := h.2,
  .. comm_ring α }

variables {R : Type u} [comm_ring R] (hr : is_local_ring R)

#check (rfl : _inst_1 = @nonzero_comm_ring.to_comm_ring.{u} R
    (@local_ring.to_nonzero_comm_ring.{u} R (@local_of_is_local_ring.{u} R _inst_1 hr)))

view this post on Zulip Kenny Lau (Dec 19 2019 at 10:39):

the rfl errors because local_of_is_local_ring eta-expands _inst_1

view this post on Zulip Kenny Lau (Dec 19 2019 at 10:39):

which is necessary because nonzero_comm_ring uses old_structure_cmd

view this post on Zulip Kenny Lau (Dec 19 2019 at 10:40):

so nonzero_comm_ring.mk takes in all the parameters of comm_ring instead of just one parameter for comm_ring

view this post on Zulip Johan Commelin (Dec 19 2019 at 11:26):

What does this mean... is old_structure_cmd bad, or should we have used it here as well? This is one of those non-mathematical issues that I'm really bad at.

view this post on Zulip Mario Carneiro (Dec 19 2019 at 12:34):

Non rfl equality of instances isn't usually a problem. We only need that extracting projections from instances is defeq

view this post on Zulip Mario Carneiro (Dec 19 2019 at 12:35):

i.e. equality up to eta expansion

view this post on Zulip Kenny Lau (Dec 19 2019 at 19:49):

import algebra.associated linear_algebra.basic order.zorn

universes u
variables {α : Type u}

def nonunits (α : Type u) [monoid α] : set α := { a | ¬is_unit a }

theorem mul_mem_nonunits_right [comm_monoid α] {a b : α} :
  b  nonunits α  a * b  nonunits α :=
mt is_unit_of_mul_is_unit_right

section prio
set_option default_priority 100 -- see Note [default priority]
class local_ring (α : Type u) extends nonzero_comm_ring α :=
(is_local :  (a : α), (is_unit a)  (is_unit (1 - a)))
end prio

theorem zero_mem_nonunits [semiring α] : 0  nonunits α  (0:α)  1 :=
not_congr is_unit_zero_iff

lemma nonunits_add [local_ring α] {x y} (hx : x  nonunits α) (hy : y  nonunits α) :
  x + y  nonunits α :=
begin
  rintros u, hu,
  apply hy,
  suffices : is_unit ((u⁻¹ : α) * y),
  { rcases this with s, hs,
    use u * s,
    convert congr_arg (λ z, (u : α) * z) hs,
    rw  mul_assoc, simp },
  rw show (u⁻¹ * y) = (1 - u⁻¹ * x),
  { rw eq_sub_iff_add_eq,
    replace hu := congr_arg (λ z, (u⁻¹ : α) * z) hu,
    simpa [mul_add] using hu },
  apply classical.or_iff_not_imp_left.1 (local_ring.is_local _),
  exact mul_mem_nonunits_right hx
end

def nonunits_ideal (α : Type u) [local_ring α] : ideal α :=
{ carrier := nonunits α,
  zero := zero_mem_nonunits.2 $ zero_ne_one,
  add := λ x y hx hy, nonunits_add hx hy,
  smul := λ a x, mul_mem_nonunits_right }

def is_local_ring (α : Type u) [comm_ring α] : Prop :=
((0:α)  1)   (a : α), (is_unit a)  (is_unit (1 - a))

def local_of_is_local_ring [comm_ring α] (h : is_local_ring α) : local_ring α :=
{ zero_ne_one := h.1,
  is_local := h.2,
  .. comm_ring α }

variables {R : Type u} [comm_ring R]

theorem add_mem_nonunits (hr : is_local_ring R) {x y : R} (hx : x  nonunits R) (hy : y  nonunits R) :
  x + y  nonunits R :=
(@@nonunits_ideal R $ local_of_is_local_ring hr).add_mem hx hy

view this post on Zulip Kenny Lau (Dec 19 2019 at 19:49):

the last line errors because the two instances are not defeq


Last updated: May 14 2021 at 03:27 UTC