characteristic of fields

Stream: general

[Kenny Lau]

@Mario Carneiro @Johan Commelin @Kevin Buzzard how should we define the char of a field?

[Mario Carneiro]

I think your definition should be on semirings instead of zero/one/mul classes

[Mario Carneiro]

I guess it could be on rings, since a nonzero characteristic semiring is a ring

[Chris Hughes]

Should it be a class or just a Prop?

[Mario Carneiro]

a prop, it is a prop

[Mario Carneiro]

oh wait you aren't asking about char_p

[Kenny Lau]

both

[Chris Hughes]

I'm asking about char.

[Kenny Lau]

I'm asking about this thing in general

[Kenny Lau]

how did metamath / other languages deal with this?

[Kenny Lau]

and is char(Q) 0 or 1?

[Mario Carneiro]

char(Q) is 0

[Kenny Lau]

in where?

[Mario Carneiro]

in metamath

[Mario Carneiro]

and in math

[Kenny Lau]

but how is char defined?

[Kenny Lau]

I feel like there's 1,000,000 subtleties

[Mario Carneiro]

the order of 1

[Kenny Lau]

how is order defined?

[Chris Hughes]

We don't have order_of on non finite groups

[Mario Carneiro]

and the order of a group element is the smallest nonzero power of the element that is 1

[Mario Carneiro]

or 0 if it doesn't exist

[Kenny Lau]

so that's a def not a prop?

[Kenny Lau]

ok I don't like this

[Mario Carneiro]

metamath doesn't care about computability tho

[Kenny Lau]

do we have another approach?

[Mario Carneiro]

there is a computable definition yielding a roption nat

[Mario Carneiro]

and if we define get_or_else for roption then we can make it 0 otherwise

[Kenny Lau]

would it be usable?

[Mario Carneiro]

I am a fan of roption definitions; it would give you a relational interface

[Mario Carneiro]

p \in char R

[Kevin Buzzard]

The characteristic of a ring is the kernel of the canonical ring homomorphism from the integers to the ring.

[Mario Carneiro]

there is also the ideal option

[Kenny Lau]

The characteristic of a ring is the kernel of the canonical ring homomorphism from the integers to the ring.

next

[Kevin Buzzard]

That's the best definition.

[Mario Carneiro]

that's just restating x^n = 0 though

[Mario Carneiro]

maybe a better question is not what is the characteristic but what is it for

[Mario Carneiro]

We have PID defined, right? Is it constructive exists?

[Kenny Lau]

class is_principal_ideal (S : set α) : Prop :=
(principal : ∃ a : α, S = {x | a ∣ x})

class principal_ideal_domain (α : Type*) extends integral_domain α :=
(principal : ∀ (S : set α) [is_ideal S], is_principal_ideal S)

[Kenny Lau]

yes

[Mario Carneiro]

well no

[Kevin Buzzard]

That looks right to me. Is Mario asking about whether there's a function from ideals to generators though?

[Mario Carneiro]

yeah

[Kevin Buzzard]

A maths PID is what Kenny just quoted.

[Mario Carneiro]

I guess there is no constructive proof that Z is a PID then?

[Kevin Buzzard]

Of course the notion of PID was not invented by constructivists.

[Kenny Lau]

nothing involving arbitrary sets can be constructive

[Kevin Buzzard]

History is written by the victors

[Mario Carneiro]

that's not exactly true kenny, it's possible that the ideal structure can be leveraged to give a generator

[Kevin Buzzard]

I guess there is no constructive proof that Z is a PID then?

The standard proof in textbooks ("if the ideal is zero then done, if not then choose the smallest positive integer") is constructive.

[Mario Carneiro]

well, constructive with LEM

[Kenny Lau]

you can't decide if the ideal is zero

[Mario Carneiro]

you can't determine if an arbitrary ideal is zero

[Kevin Buzzard]

In Z??

[Mario Carneiro]

that's exactly the problem with defining characteristic

[Kenny Lau]

give me an algorithm

[Mario Carneiro]

the set of periods of an element is an ideal of Z

[Mario Carneiro]

but you can't tell if it is zero

[Kevin Buzzard]

I'm not going to talk about this any more. It's silly.

[Mario Carneiro]

I think we have our answer Kenny

[Kevin Buzzard]

:-)

[Mario Carneiro]

totalize it

[Kenny Lau]

could you summarize the answer?

[Kevin Buzzard]

Are you going to assume LEM?

[Mario Carneiro]

char Q = 0

[Mario Carneiro]

noncomputable

[Mario Carneiro]

live with it

[Kenny Lau]

no roption?

[Mario Carneiro]

if you insist, you can define char' A : roption nat

[Mario Carneiro]

and define char in terms of it

[Mario Carneiro]

but most of the theory will be about char

[Kenny Lau]

it won't be a class then

[Patrick Massot]

kenny_char : roption Prop (because who knows?)

[Mario Carneiro]

also, char is a type

[Kenny Lau]

but every ring has a unique char

[Mario Carneiro]

characters

[Mario Carneiro]

there is also the ideal definition, dunno how useful it is but that's constructive too

[Patrick Massot]

Let's write it in French then! car

[Kenny Lau]

I mean, it's useful to make "char A = p" into a class

[Mario Carneiro]

I agree on that

[Mario Carneiro]

char_p is fine and unproblematic

[Kenny Lau]

oh ok

[Reid Barton]

but every ring has a unique char

isn't this not true constructively? or am I really confused

[Mario Carneiro]

no, that's true

[Kenny Lau]

I'm talking about the reason to make it into a typeclass

[Mario Carneiro]

if a ring has two characteristics then they are equal

[Kenny Lau]

class char_p (α : Type u) [has_zero α] [has_one α] [has_add α] (p : ℕ) : Prop :=
(cast_eq_zero : (p:α) = 0)

Do we all agree that this definition is deficit?

[Reid Barton]

It's the "has" part I am worried about

[Reid Barton]

I agree "unique" is okay.

[Mario Carneiro]

no you can't prove existence of a characteristic (number) in general without LEM

[Mario Carneiro]

the ideal is fine of course

[Reid Barton]

right, okay

[Reid Barton]

I guess there is no constructive proof that Z is a PID then?

I think you can even prove constructively that "Z is a PID" => LEM

[Reid Barton]

by taking a proposition P and defining the ideal I = {x | x = 0 \/ P}

[Reid Barton]

and then looking at whether its generator is zero or not

[Kenny Lau]

class char_p (α : Type u) [semiring α] (p : ℕ) : Prop :=
(cast_eq_zero_iff : ∀ x:ℕ, (x:α) = 0 ↔ p ∣ x)

[Kenny Lau]

how about this

[Kenny Lau]

class char_p (α : Type u) [semiring α] (p : ℕ) : Prop :=
(cast_eq_zero_iff : ∀ x:ℕ, (x:α) = 0 ↔ p ∣ x)

theorem char_p.cast_eq_zero {α : Type u} [semiring α] {p : ℕ} [char_p α p] : (p:α) = 0 :=
(char_p.cast_eq_zero_iff α p p).2 (dvd_refl p)

theorem char_p.eq (α : Type u) [semiring α] (p q : ℕ) [char_p α p] [char_p α q] : p = q :=
nat.dvd_antisymm
  ((char_p.cast_eq_zero_iff α p q).1 char_p.cast_eq_zero)
  ((char_p.cast_eq_zero_iff α q p).1 char_p.cast_eq_zero)

[Kenny Lau]

I think your definition should be on semirings instead of zero/one/mul classes

but char_zero is defined on [add_monoid \a] [has_one \a]?

[Mario Carneiro]

or that

[Kenny Lau]

existe uma diferencia?

[Kenny Lau]

class char_p (α : Type u) [semiring α] (p : ℕ) : Prop :=
(cast_eq_zero_iff : ∀ x:ℕ, (x:α) = 0 ↔ p ∣ x)

theorem char_p.cast_eq_zero (α : Type u) [semiring α] (p : ℕ) [char_p α p] : (p:α) = 0 :=
(char_p.cast_eq_zero_iff α p p).2 (dvd_refl p)

theorem char_p.eq (α : Type u) [semiring α] (p q : ℕ) [char_p α p] [char_p α q] : p = q :=
nat.dvd_antisymm
  ((char_p.cast_eq_zero_iff α p q).1 (char_p.cast_eq_zero _ _))
  ((char_p.cast_eq_zero_iff α q p).1 (char_p.cast_eq_zero _ _))

instance char_p.of_char_zero (α : Type u) [semiring α] [char_zero α] : char_p α 0 :=
⟨λ x, by rw [zero_dvd_iff, ← nat.cast_zero, nat.cast_inj]⟩

theorem char_p.exists (α : Type u) [semiring α] : ∃ p, char_p α p :=
by letI := classical.dec_eq α; exact
classical.by_cases
  (assume H : ∀ p:ℕ, (p:α) = 0 → p = 0, ⟨0,
    ⟨λ x, by rw [zero_dvd_iff]; exact ⟨H x, by rintro rfl; refl⟩⟩⟩)
  (λ H, ⟨nat.find (classical.not_forall.1 H), ⟨λ x,
    ⟨λ H1, nat.dvd_of_mod_eq_zero (by_contradiction $ λ H2,
      nat.find_min (classical.not_forall.1 H)
        (nat.mod_lt x $ nat.pos_of_ne_zero $ not_of_not_imp $
          nat.find_spec (classical.not_forall.1 H))
        (not_imp_of_and_not ⟨by rwa [← nat.mod_add_div x (nat.find (classical.not_forall.1 H)),
          nat.cast_add, nat.cast_mul, of_not_not (not_not_of_not_imp $ nat.find_spec (classical.not_forall.1 H)),
          zero_mul, add_zero] at H1, H2⟩)),
    λ H1, by rw [← nat.mul_div_cancel' H1, nat.cast_mul,
      of_not_not (not_not_of_not_imp $ nat.find_spec (classical.not_forall.1 H)), zero_mul]⟩⟩⟩)

theorem char_p.exists_unique (α : Type u) [semiring α] : ∃! p, char_p α p :=
let ⟨c, H⟩ := char_p.exists α in
⟨c, H, λ y H2, by resetI; apply char_p.eq α⟩

[Kenny Lau]

How does this look? @Mario Carneiro @Patrick Massot

[Kenny Lau]

@Kevin Buzzard

[Kevin Buzzard]

class char_p (α : Type u) [semiring α] (p : ℕ) : Prop :=
(cast_eq_zero_iff : ∀ x:ℕ, (x:α) = 0 ↔ p ∣ x)

I see you went for the ideal idea after all ;-)

[Mario Carneiro]

char_p.eq should definitely not have square brackets

[Kevin Buzzard]

is_char_p?

[Mario Carneiro]

Maybe it should be a property of Z, then you can literally say is_ideal (char_p A)

[Kenny Lau]

wait I'm confused

[Kenny Lau]

theorem char_p.eq (α : Type u) [semiring α] (p q : ℕ) (c1 : char_p α p) (c2 : char_p α q) : p = q :=
nat.dvd_antisymm
  ((char_p.cast_eq_zero_iff α p q).1 (char_p.cast_eq_zero _ _))
  ((char_p.cast_eq_zero_iff α q p).1 (char_p.cast_eq_zero _ _))

[Kenny Lau]

how can the proof still work now that I turned [] to ()?

[Mario Carneiro]

maybe kevin knows... I told him the solution to this puzzle a few weeks ago

[Kenny Lau]

anyway how is this now?

class char_p (α : Type u) [semiring α] (p : ℕ) : Prop :=
(cast_eq_zero_iff : ∀ x:ℕ, (x:α) = 0 ↔ p ∣ x)

theorem char_p.cast_eq_zero (α : Type u) [semiring α] (p : ℕ) [char_p α p] : (p:α) = 0 :=
(char_p.cast_eq_zero_iff α p p).2 (dvd_refl p)

theorem char_p.eq (α : Type u) [semiring α] {p q : ℕ} (c1 : char_p α p) (c2 : char_p α q) : p = q :=
nat.dvd_antisymm
  ((char_p.cast_eq_zero_iff α p q).1 (char_p.cast_eq_zero _ _))
  ((char_p.cast_eq_zero_iff α q p).1 (char_p.cast_eq_zero _ _))

instance char_p.of_char_zero (α : Type u) [semiring α] [char_zero α] : char_p α 0 :=
⟨λ x, by rw [zero_dvd_iff, ← nat.cast_zero, nat.cast_inj]⟩

theorem char_p.exists (α : Type u) [semiring α] : ∃ p, char_p α p :=
by letI := classical.dec_eq α; exact
classical.by_cases
  (assume H : ∀ p:ℕ, (p:α) = 0 → p = 0, ⟨0,
    ⟨λ x, by rw [zero_dvd_iff]; exact ⟨H x, by rintro rfl; refl⟩⟩⟩)
  (λ H, ⟨nat.find (classical.not_forall.1 H), ⟨λ x,
    ⟨λ H1, nat.dvd_of_mod_eq_zero (by_contradiction $ λ H2,
      nat.find_min (classical.not_forall.1 H)
        (nat.mod_lt x $ nat.pos_of_ne_zero $ not_of_not_imp $
          nat.find_spec (classical.not_forall.1 H))
        (not_imp_of_and_not ⟨by rwa [← nat.mod_add_div x (nat.find (classical.not_forall.1 H)),
          nat.cast_add, nat.cast_mul, of_not_not (not_not_of_not_imp $ nat.find_spec (classical.not_forall.1 H)),
          zero_mul, add_zero] at H1, H2⟩)),
    λ H1, by rw [← nat.mul_div_cancel' H1, nat.cast_mul,
      of_not_not (not_not_of_not_imp $ nat.find_spec (classical.not_forall.1 H)), zero_mul]⟩⟩⟩)

theorem char_p.exists_unique (α : Type u) [semiring α] : ∃! p, char_p α p :=
let ⟨c, H⟩ := char_p.exists α in
⟨c, H, λ y H2, char_p.eq α H2 H⟩

[Mario Carneiro]

char_p.exists should be defining a function... called char

[Kenny Lau]

we can functionize that

[Kevin Buzzard]

He told Johannes too.

[Kenny Lau]

invalid definition, a declaration named 'char' has already been declared

[Kenny Lau]

hard luck

[Kenny Lau]

noncomputable def ring_char (α : Type u) [semiring α] : ℕ :=
classical.some (char_p.exists_unique α)

theorem ring_char.spec (α : Type u) [semiring α] : ∀ x:ℕ, (x:α) = 0 ↔ ring_char α ∣ x :=
by letI := (classical.some_spec (char_p.exists_unique α)).1;
unfold ring_char; exact char_p.cast_eq_zero_iff α (ring_char α)

theorem ring_char.eq (α : Type u) [semiring α] {p : ℕ} (C : char_p α p) : p = ring_char α :=
(classical.some_spec (char_p.exists_unique α)).2 p C

[Kenny Lau]

how is this?

[Kevin Buzzard]

how can the proof still work now that I turned [] to ()?

Type class inference just grabs anything it can find to the left of the colon. The round and square brackets are just for the signature of the theorem, they don't affect how type class inference works in the proof. This is not so well-known because it's not common to put a typeclass left of the colon and not in a square bracket.

[Kevin Buzzard]

I discovered it a few weeks ago when I was trying to understand Patrick's type class hell with his completions and had exactly the same reaction.

[Kevin Buzzard]

I've had to construct that argument from memory because my search for the conversation failed. Hopefully it's some sort of approximation to the truth.

[Bryan Gin-ge Chen]

I guess it's this conversation? I found it by searching for "left of colon".

[Kenny Lau]

@Mario Carneiro Could you help me with some typeclass problems? It's in L324 here: https://github.com/kckennylau/Lean/blob/master/perfect_closure.lean#L324

[Kenny Lau]

Lean can't figure out the coercion in (↑x : perfect_closure α p)

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/Separation.20stuff/near/134261591

[Kevin Buzzard]

You owe Mario a light bulb

[Kenny Lau]

done

[Kevin Buzzard]

(thanks Bryan)

[Kenny Lau]

@Mario Carneiro never mind it's stupid