local ring diamond?

Stream: general

[Kenny Lau]

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)))

[Kenny Lau]

the rfl errors because local_of_is_local_ring eta-expands _inst_1

[Kenny Lau]

which is necessary because nonzero_comm_ring uses old_structure_cmd

[Kenny Lau]

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

[Johan Commelin]

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.

[Mario Carneiro]

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

[Mario Carneiro]

i.e. equality up to eta expansion

[Kenny Lau]

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

[Kenny Lau]

the last line errors because the two instances are not defeq