## Stream: general

### Topic: local ring diamond?

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


#### Kenny Lau (Dec 19 2019 at 10:39):

the rfl errors because local_of_is_local_ring eta-expands _inst_1

#### Kenny Lau (Dec 19 2019 at 10:39):

which is necessary because nonzero_comm_ring uses old_structure_cmd

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

#### 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.

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

#### Mario Carneiro (Dec 19 2019 at 12:35):

i.e. equality up to eta expansion

#### 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),
replace hu := congr_arg (λ z, (↑u⁻¹ : α) * z) 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 (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