the most pointless construction

Stream: general

[Kenny Lau]

I constructed the left adjoint of the forgetful functor from (the category of fields with 0^-1 = 0) to (the category of nonzero comm rings where every element is a unit)

[Johan Commelin]

Awesome... ...

[Johan Commelin]

That's an equivalence. But not constructively so? I don't know. Whatever :grinning:

[Kenny Lau]

Sneak peak:

inductive pre_to_field : Type u
| of : α → pre_to_field
| add : pre_to_field → pre_to_field → pre_to_field
| mul : pre_to_field → pre_to_field → pre_to_field
| inv : pre_to_field → pre_to_field

def mk (x : α) : to_field α :=
⟦pre_to_field.of x⟧

theorem mk.bijective : function.bijective (@mk α _ _) :=
⟨λ x y H, let ⟨z, hxz, hyz⟩ := quotient.exact H in eq.trans hxz hyz.symm,
λ x, quotient.induction_on x $ λ p, let ⟨z, hz⟩ := pre_to_field.unique_rel p in
⟨z, quotient.sound ⟨z, rfl, hz.1⟩⟩⟩

def eval {β : Type v} [field' β] (f : α → β) [is_ring_hom f] (p : to_field α) : β :=
quotient.lift_on p (pre_to_field.eval f) $ λ p q ⟨x, hpx, hqx⟩,
by rw [pre_to_field.eval_of_rel f hpx, pre_to_field.eval_of_rel f hqx]

[Mario Carneiro]

is this the free meadow?

[Johan Commelin]

I never understood why "champ algebrique" was translated into English as "algebraic stack" instead of "algebraic acre".

[Kenny Lau]

@Mario Carneiro does this have its place in mathlib?

[Kenny Lau]

we can redefine the reals to have "computable" inverse :P

[Mario Carneiro]

what's field'?

[Kenny Lau]

good question

[Kenny Lau]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/field'

[Kenny Lau]

see this thread :P

[Mario Carneiro]

what's to_field?

[Kenny Lau]

def to_field [ring α] [is_division_ring α] : Type u :=
quotient (pre_to_field.setoid α)

[Mario Carneiro]

I think field' should be discrete_field

[Kenny Lau]

I don't think so

[Kenny Lau]

because we don't assume modules, abelian groups, rings, semirings, etc, to have decidable equality

[Mario Carneiro]

that's true, but decidability is sort of part of a field - it's basically impossible to define a field structure without decidable equality

[Kenny Lau]

I just did it :P

[Mario Carneiro]

what about 0 != 1? What's pre_to_field.setoid?

[Kenny Lau]

import algebra.ring

universes u v

variables (α : Type u)

class is_division_ring [ring α] : Prop :=
(exists_inv : ∀ {x : α}, x ≠ 0 → ∃ y, x * y = 1)

section
set_option old_structure_cmd true
class field' (α : Type u) extends division_ring α, comm_ring α :=
(inv_zero : (0:α)⁻¹ = 0)
end

theorem inv_zero' [field' α] : (0:α)⁻¹ = 0 :=
field'.inv_zero α

theorem mul_eq_one_comm {α} [ring α] [is_division_ring α] {x y : α} (hxy : x * y = 1) : y * x = 1 :=
classical.by_cases
  (assume hy0 : y = 0, by rw [← hxy, hy0, zero_mul, mul_zero])
  (assume hy0 : y ≠ 0, let ⟨z, hz⟩ := is_division_ring.exists_inv hy0 in
    by rw [← mul_one x, ← hz, ← mul_assoc x, hxy, one_mul])

inductive pre_to_field : Type u
| of : α → pre_to_field
| add : pre_to_field → pre_to_field → pre_to_field
| mul : pre_to_field → pre_to_field → pre_to_field
| inv : pre_to_field → pre_to_field

namespace pre_to_field

variables {α}

def rel [semiring α] : (pre_to_field α) → α → Prop
| (of p)    z := p = z
| (add p q) z := ∃ x y, rel p x ∧ rel q y ∧ x + y = z
| (mul p q) z := ∃ x y, rel p x ∧ rel q y ∧ x * y = z
| (inv p)   z := rel p 0 ∧ z = 0 ∨ ∃ x, rel p x ∧ x * z = 1

def neg [has_neg α] : pre_to_field α → pre_to_field α
| (of p)    := of (-p)
| (add x y) := add (neg x) (neg y)
| (mul x y) := mul (neg x) y
| (inv x)   := inv (neg x)

theorem rel_neg [ring α] : Π {p} {z : α}, rel p z → rel (neg p) (-z)
| (of p)    z hpz                   := congr_arg has_neg.neg hpz
| (add p q) z ⟨x, y, hpx, hqy, hxyz⟩ := ⟨-x, -y, rel_neg hpx, rel_neg hqy, by rw [← hxyz, neg_add]⟩
| (mul p q) z ⟨x, y, hpx, hqy, hxyz⟩ := ⟨-x, y, rel_neg hpx, hqy, by rw [← hxyz, neg_mul_eq_neg_mul]⟩
| (inv p)   z (or.inl ⟨hp0, hz0⟩)    := or.inl ⟨@neg_zero α _ ▸ rel_neg hp0, neg_eq_zero.2 hz0⟩
| (inv p)   z (or.inr ⟨x, hpx, hxz⟩) := or.inr ⟨-x, rel_neg hpx, by rw [neg_mul_neg, hxz]⟩

variables [ring α] [is_division_ring α]

lemma unique_rel (p : pre_to_field α) :
  ∃!x, rel p x :=
pre_to_field.rec_on p
  (λ x, ⟨x, rfl, λ y hxy, hxy.symm⟩)
  (λ p q ⟨x, hpx, hpx2⟩ ⟨y, hqy, hqy2⟩, ⟨x+y, ⟨x, y, hpx, hqy, rfl⟩,
    λ z ⟨x', y', hpx', hqy', hxyz⟩, hpx2 x' hpx' ▸ hqy2 y' hqy' ▸ hxyz.symm⟩)
  (λ p q ⟨x, hpx, hpx2⟩ ⟨y, hqy, hqy2⟩, ⟨x*y, ⟨x, y, hpx, hqy, rfl⟩,
    λ z ⟨x', y', hpx', hqy', hxyz⟩, hpx2 x' hpx' ▸ hqy2 y' hqy' ▸ hxyz.symm⟩)
  (λ p ⟨x, hpx, hpx2⟩, classical.by_cases
    (assume hx0 : x = 0, ⟨0, or.inl ⟨hx0 ▸ hpx, rfl⟩, λ y hy,
      or.cases_on hy and.right $ λ ⟨z, hpz, hzy⟩,
      by rw [← one_mul y, ← hzy, hpx2 z hpz, hx0, zero_mul, zero_mul]⟩)
    (assume hx0 : x ≠ 0, let ⟨y, hxy⟩ := is_division_ring.exists_inv hx0 in
      ⟨y, or.inr ⟨x, hpx, hxy⟩, λ z hz, or.cases_on hz
        (λ ⟨hp0, hz0⟩, by rw [hz0, ← one_mul y, ← hxy, ← hpx2 0 hp0, zero_mul, zero_mul])
        (λ ⟨s, hps, hsz⟩, by rw [← mul_one y, ← hsz, ← mul_assoc, hpx2 s hps, mul_eq_one_comm hxy, one_mul])⟩))

variables {β : Type v}

def eval [division_ring β] (f : α → β) : pre_to_field α → β
| (of p)    := f p
| (add x y) := eval x + eval y
| (mul x y) := eval x * eval y
| (inv p)   := (eval p)⁻¹

theorem eval_of_rel [field' β] (f : α → β) [is_ring_hom f] :
  Π {p} {x : α} (hpx : pre_to_field.rel p x), eval f p = f x
| (of p)    z hpz                   := congr_arg f hpz
| (add p q) z ⟨x, y, hpx, hqy, hxyz⟩ := by rw [eval, eval_of_rel hpx, eval_of_rel hqy, ← hxyz, is_ring_hom.map_add f]
| (mul p q) z ⟨x, y, hpx, hqy, hxyz⟩ := by rw [eval, eval_of_rel hpx, eval_of_rel hqy, ← hxyz, is_ring_hom.map_mul f]
| (inv p)   z (or.inl ⟨hp0, hz0⟩)    := by rw [eval, eval_of_rel hp0, hz0, is_ring_hom.map_zero f, inv_zero']
| (inv p)   z (or.inr ⟨x, hpx, hxz⟩) := by rw [eval, eval_of_rel hpx, ← mul_one (f x)⁻¹, ← is_ring_hom.map_one f,
    ← hxz, is_ring_hom.map_mul f, ← mul_assoc,
    inv_mul_cancel (assume hfx : f x = 0, @zero_ne_one β _ $
      by rw [← is_ring_hom.map_one f, ← hxz, is_ring_hom.map_mul f, hfx, zero_mul]),
    one_mul]

variables (α)

instance : setoid (pre_to_field α) :=
{ r := λ p q, ∃ x, rel p x ∧ rel q x,
  iseqv := ⟨λ p, let ⟨x, hx⟩ := unique_rel p in ⟨x, hx.1, hx.1⟩,
    λ p q ⟨x, hpx, hqx⟩, ⟨x, hqx, hpx⟩,
    λ p q r ⟨x, hpx, hqx⟩ ⟨y, hqy, hry⟩, ⟨x, hpx, unique_of_exists_unique (unique_rel q) hqy hqx ▸ hry⟩⟩ }

end pre_to_field


def to_field [ring α] [is_division_ring α] : Type u :=
quotient (pre_to_field.setoid α)

namespace to_field

variables {α} [ring α] [is_division_ring α]

def mk (x : α) : to_field α :=
⟦pre_to_field.of x⟧

variables (α)

theorem mk.bijective : function.bijective (@mk α _ _) :=
⟨λ x y H, let ⟨z, hxz, hyz⟩ := quotient.exact H in eq.trans hxz hyz.symm,
λ x, quotient.induction_on x $ λ p, let ⟨z, hz⟩ := pre_to_field.unique_rel p in
⟨z, quotient.sound ⟨z, rfl, hz.1⟩⟩⟩

instance : has_add (to_field α) :=
⟨λ x y, quotient.lift_on₂ x y (λ p q, ⟦pre_to_field.add p q⟧) $ λ p q r s ⟨x, hpx, hrx⟩ ⟨y, hqy, hsy⟩, quotient.sound
⟨x + y, ⟨x, y, hpx, hqy, rfl⟩, ⟨x, y, hrx, hsy, rfl⟩⟩⟩

instance : has_neg (to_field α) :=
⟨λ x, quotient.lift_on x (λ p, ⟦pre_to_field.neg p⟧) $ λ p q ⟨x, hpx, hqx⟩, quotient.sound
⟨-x, pre_to_field.rel_neg hpx, pre_to_field.rel_neg hqx⟩⟩

instance : has_mul (to_field α) :=
⟨λ x y, quotient.lift_on₂ x y (λ p q, ⟦pre_to_field.mul p q⟧) $ λ p q r s ⟨x, hpx, hrx⟩ ⟨y, hqy, hsy⟩, quotient.sound
⟨x * y, ⟨x, y, hpx, hqy, rfl⟩, ⟨x, y, hrx, hsy, rfl⟩⟩⟩

instance : has_inv (to_field α) :=
⟨λ x, quotient.lift_on x (λ p, ⟦pre_to_field.inv p⟧) $ λ p q ⟨x, hpx, hqx⟩, quotient.sound $
classical.by_cases
  (assume hx0 : x = 0, ⟨0, or.inl ⟨hx0 ▸ hpx, rfl⟩, or.inl ⟨hx0 ▸ hqx, rfl⟩⟩)
  (assume hx0 : x ≠ 0, let ⟨y, hy⟩ := is_division_ring.exists_inv hx0 in ⟨y, or.inr ⟨x, hpx, hy⟩, or.inr ⟨x, hqx, hy⟩⟩)⟩

variables {α}

@[elab_as_eliminator] protected lemma induction_on
  {C : to_field α → Prop} (x : to_field α)
  (ih : ∀ z, C (mk z)) : C x :=
let ⟨z, hz⟩ := (mk.bijective α).2 x in hz ▸ ih z

@[elab_as_eliminator] protected lemma induction_on₂
  {C : to_field α → to_field α → Prop} (x y : to_field α)
  (ih : ∀ p q, C (mk p) (mk q)) : C x y :=
to_field.induction_on x $ λ p, to_field.induction_on y $ λ q, ih p q

@[elab_as_eliminator] protected lemma induction_on₃
  {C : to_field α → to_field α → to_field α → Prop} (x y z : to_field α)
  (ih : ∀ p q r, C (mk p) (mk q) (mk r)) : C x y z :=
to_field.induction_on x $ λ p, to_field.induction_on y $ λ q, to_field.induction_on z $ λ r, ih p q r

@[simp] lemma mk_add (x y : α) : mk (x + y) = mk x + mk y :=
quotient.sound ⟨x + y, rfl, ⟨x, y, rfl, rfl, rfl⟩⟩

@[simp] lemma mk_neg (x : α) : mk (-x) = -mk x := rfl

@[simp] lemma mk_mul (x y : α) : mk (x * y) = mk x * mk y :=
quotient.sound ⟨x * y, rfl, ⟨x, y, rfl, rfl, rfl⟩⟩

lemma mk_inv {x y : α} (hxy : x * y = 1) : (mk x)⁻¹ = mk y :=
quotient.sound ⟨y, or.inr ⟨x, rfl, hxy⟩, rfl⟩

variables (α)
instance : ring (to_field α) :=
{ zero := mk 0,
  one := mk 1,
  add_assoc := λ x y z, to_field.induction_on₃ x y z $ λ p q r,
    by rw [← mk_add, ← mk_add, ← mk_add, ← mk_add, add_assoc],
  zero_add := λ x, to_field.induction_on x $ λ p,
    by rw [← mk_add, zero_add],
  add_zero := λ x, to_field.induction_on x $ λ p,
    by rw [← mk_add, add_zero],
  add_left_neg := λ x, to_field.induction_on x $ λ p,
    by rw [← mk_neg, ← mk_add, add_left_neg]; refl,
  add_comm := λ x y, to_field.induction_on₂ x y $ λ p q,
    by rw [← mk_add, ← mk_add, add_comm],
  mul_assoc := λ x y z, to_field.induction_on₃ x y z $ λ p q r,
    by rw [← mk_mul, ← mk_mul, ← mk_mul, ← mk_mul, mul_assoc],
  one_mul := λ x, to_field.induction_on x $ λ p,
    by rw [← mk_mul, one_mul],
  mul_one := λ x, to_field.induction_on x $ λ p,
    by rw [← mk_mul, mul_one],
  left_distrib := λ x y z, to_field.induction_on₃ x y z $ λ p q r,
    by rw [← mk_add, ← mk_mul, ← mk_mul, ← mk_mul, ← mk_add, mul_add],
  right_distrib := λ x y z, to_field.induction_on₃ x y z $ λ p q r,
    by rw [← mk_add, ← mk_mul, ← mk_mul, ← mk_mul, ← mk_add, add_mul],
  .. to_field.has_add α,
  .. to_field.has_neg α,
  .. to_field.has_mul α }

@[simp] lemma mk_zero : mk (0 : α) = 0 := rfl
@[simp] lemma mk_one : mk (1 : α) = 1 := rfl

instance mk.is_ring_hom : is_ring_hom (@mk α _ _) :=
⟨mk_one α, mk_mul, mk_add⟩

variables {α}
def eval {β : Type v} [field' β] (f : α → β) [is_ring_hom f] (p : to_field α) : β :=
quotient.lift_on p (pre_to_field.eval f) $ λ p q ⟨x, hpx, hqx⟩,
by rw [pre_to_field.eval_of_rel f hpx, pre_to_field.eval_of_rel f hqx]

instance eval.is_ring_hom {β : Type v} [field' β] (f : α → β) [is_ring_hom f] : is_ring_hom (eval f) :=
⟨by convert is_ring_hom.map_one f,
λ p q, quotient.induction_on₂ p q $ λ x y, rfl,
λ p q, quotient.induction_on₂ p q $ λ x y, rfl⟩

end to_field

namespace to_field

instance [comm_ring α] [is_division_ring α] : comm_ring (to_field α) :=
{ mul_comm := λ x y, to_field.induction_on₂ x y $ λ p q,
    by rw [← mk_mul, ← mk_mul, mul_comm],
  .. to_field.ring α }

instance [nonzero_comm_ring α] [is_division_ring α] : field (to_field α) :=
{ zero_ne_one := λ H, zero_ne_one $ (mk.bijective α).1 H,
  mul_inv_cancel := λ x, to_field.induction_on x $ λ p hp0,
    let ⟨y, hy⟩ := is_division_ring.exists_inv (mt (congr_arg mk) hp0) in
    by rw [mk_inv hy, ← mk_mul, hy, mk_one],
  inv_mul_cancel := λ x, to_field.induction_on x $ λ p hp0,
    let ⟨y, hy⟩ := is_division_ring.exists_inv (mt (congr_arg mk) hp0) in
    by rw [mk_inv hy, ← mk_mul, mul_eq_one_comm hy, mk_one],
  .. to_field.comm_ring α,
  .. to_field.has_inv α }

end to_field

[Kenny Lau]

oh and to give a concrete example: the Cauchy sequence construction of the real numbers allow you to define it as a ring constructively; then to_field real would be an example of a field where the inverse of 0 is 0, but it has no decidable equality.

[Chris Hughes]

But you can't do it with computable inverses is the point I think.

[Kenny Lau]

to_field real has computable inverse, inv zero = zero, and no decidable equality

[Mario Carneiro]

I see a classical.by_cases in there though

[Kenny Lau]

classical.by_cases is computable

[Mario Carneiro]

In order to work with the axioms of a division ring you don't actually need decidable eq but rather eq LEM

[Mario Carneiro]

but we don't have a typeclass for that

[Kenny Lau]

I just find it inconvenient that the inverse of zero is left unspecified in field (which makes subfield weird, as seen in #742), and too strict that discrete_field requires decidable equality

[Kenny Lau]

I think field' is the correct structure

[Mario Carneiro]

I agree that field is stupid, that's why I've been telling everyone to use discrete_field instead

[Kenny Lau]

but we don't assume add_comm_group or semiring or module to have decidable equality either, so decidable equality seems too strong

[Mario Carneiro]

That's because none of those have case analysis on equaling zero

[Mario Carneiro]

I think the proper constructive analogue of field is ring

[Mario Carneiro]

Also, we do have plenty of structures that assume decidable equality, specifically the order structures

[Mario Carneiro]

decidable_linear_ordered_semigroup and so on

[Kenny Lau]

but the category of discrete rings is not closed under direct limit

[Mario Carneiro]

is the category of fields?

[Kenny Lau]

yes

[Mario Carneiro]

in that case, I have no idea what you are talking about

[Kenny Lau]

what?

[Mario Carneiro]

I don't have any conception of how direct limits work

[Mario Carneiro]

or what the issues are

[Kenny Lau]

https://github.com/leanprover-community/mathlib/blob/cf8a619bde24d327387dd7321a8da55fd3bbd585/src/algebra/direct_limit.lean#L503-L555

[Kenny Lau]

the issue is that to_field works great with direct limit

[Kenny Lau]

the category of field is closed under direct limit

[Kenny Lau]

and the category of discrete field might also be (I haven't thought about it)

[Kenny Lau]

but the category of discrete rings, I'm 50% certain that it must not be closed under direct limit

[Mario Carneiro]

I didn't say anything about discrete rings though

[Kenny Lau]

so you think that field' should not even exist?

[Mario Carneiro]

I'm asserting that all interesting fields are decidable

[Kenny Lau]

and I gave you a concrete counter-example

[Kenny Lau]

there's no way to make real decidable

[Mario Carneiro]

You want a different structure than field'... you want a ring where inverses exist

[Mario Carneiro]

exist in the weak sense

[Kenny Lau]

well then theorems become a bit clumsy

[Kenny Lau]

so no that's not what I want

[Mario Carneiro]

to_field gives you a way to explicitly refer to these elements that are only known to exist propositionally

[Mario Carneiro]

but the cost is that you "only" get a bijection rather than an equiv

[Kenny Lau]

is there a situation where the hypothetical inverse function to_field real -> real is helpful?

[Mario Carneiro]

sure... if you want to talk about the inverse of a real number

[Kenny Lau]

I mean, let's say we replaced real with to_field real

[Kenny Lau]

everywhere in mathlib

[Kenny Lau]

so the canonical structure of the real numbers is a field where the inverse of zero is zero, without decidable equality

[Kenny Lau]

also I think the category of discrete fields is not closed under direct limit

[Mario Carneiro]

The real numbers are a quotient of Cauchy sequences. to_field real is a quotient of field expressions with constants in real... so it's like you just adjoined inverses for everything

[Kenny Lau]

you never use the Cauchy sequences anyway

[Mario Carneiro]

How do you define the supremum?

[Kenny Lau]

ok let's put this in context

[Kenny Lau]

what should I replace https://github.com/leanprover-community/mathlib/blob/cf8a619bde24d327387dd7321a8da55fd3bbd585/src/algebra/direct_limit.lean#L503-L555 by?

[Kenny Lau]

I definitely want direct limit of fields

[Kenny Lau]

so don't tell me replace it with EOF

[Mario Carneiro]

go classical, man

[Kenny Lau]

classical != noncomputable

[Mario Carneiro]

go noncomputable, man

[Kenny Lau]

really?

[Mario Carneiro]

if it requires you to invent entirely new algebraic structures just to get this theorem, yes it seems like a valid approach

[Kenny Lau]

what's wrong with inventing new algebraic structures

[Mario Carneiro]

well you have to make sure they play well with everything else

[Mario Carneiro]

particularly if you are planning on replacing the original

[Mario Carneiro]

I should say that I am actually quite impressed with the whole construction; I didn't know this was possible until you showed me

[Kenny Lau]

thanks for your appreciation

[Mario Carneiro]

But I'm 110% sure kevin will say you are wasting your time

[Kenny Lau]

... on a more related note, does this have its place in mathlib?

[Kenny Lau]

class is_division_ring [ring α] : Prop :=
(exists_inv : ∀ {x : α}, x ≠ 0 → ∃ y, x * y = 1)

[Mario Carneiro]

This seems a bit easier to deal with. This is what division rings should have been

[Mario Carneiro]

IIUC real is a division ring in this sense

[Kenny Lau]

so in which file should I put this?

[Kevin Buzzard]

(wasting your time) -- I simply do not understand the issues here and with things like this I only attempt to understand the issues when they actually affect my own work (like I never understood why lean treated quotients differently from equivalence classes until it began to matter to me). I'm not sure this will ever matter to me but I can quite believe there is a discussion to be had

[Sebastien Gouezel]

Why shouldn't we assume that all our structures have decidable equality? I am sure there are interesting things to be discussed here, but I don't really get them. I think what I would like to see is a concrete example where it creates a problem to assume decidable equality everywhere.

[Mario Carneiro]

I think the main problem is that this can make definitions noncomputable when they should be computable, e.g. rational arithmetic

[Mario Carneiro]

and this can block some rfl proofs of trivial facts

[Mario Carneiro]

(that's the pragmatic answer; there might also be religious reasons)

[Sebastien Gouezel]

I am very much interested in pragmatic answers, thanks. And what if general decidable equality is declared with priority 0, and specific computable instances are declared with higher priority, say 50. Would that still block anything?

[Mario Carneiro]

The problem isn't so much with finding the wrong instance as it is with intermediate constructions being more classical than they could be with more care

[Mario Carneiro]

i.e. if you use that int is a ring then you are depending on the axiom of choice, because an intermediate step decided not to use decidable equality when it was available

[Sebastien Gouezel]

I still don't get why it could be important in proofs, since they are irrelevant anyway. In definitions where one might want to compute, sure. But my question is even more pragmatic: if one removed everything about linear_order in mathlib, using only decidable_linear_order everywhere, would that break something? If one assumed in the very definition of ring, and group, and everything, that equality is decidable, would that break something?

[Kenny Lau]

"Proofs are irrelevant" -- every Lean user ever

[Johannes Hölzl]

Lean 3 users, there is still HoTT Lean

[Johannes Hölzl]

But I would also prefer to add decidability to most things: (additive) semigroups, orders etc.

[Sebastien Gouezel]

"Proofs are irrelevant" -- every Lean user ever

This quote is crazy, and I can't believe I said it myself. Don't tell that to my fellow mathematicians, please.