Zulip Chat Archive

Stream: new members

Topic: Exponential characteristic


view this post on Zulip Jakob Scholbach (Mar 04 2021 at 16:44):

Following @Adam Topaz 's suggestion (https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Unwinding.20definitions.20involving.20if.20else/near/228138682) , and as part of a project attempting to write some basics about separable extensions etc., I have written a small file containing the basic definition of the exponential characteristic. Since I am fairly sure this is still premature from the point of view of the pro's around, I would like to collect some advice / suggestions for improvement before I might eventually suggest this to become a part of mathlib. Thanks!

import algebra.char_p.basic
import algebra.char_zero
import data.nat.prime

universe u
variables (α : Type u) [integral_domain α]

/-- The exponential characteristic of an integral domain. -/
class exp_char (p : ): Prop :=
  (exp_char_def : (p = 1  char_zero α)  (p>0  char_p α p))

lemma exp_char_one_of_char_zero (p q : ) [hp: char_p α p] [hq : exp_char α q]:
  p = 0  q = 1 :=
begin
  cases hq.exp_char_def with q_one q_pos,
  {
    intro p0,
    exact q_one.1,
  },
  {
    intro p0,
    have : p = q, { apply char_p.eq α, exact hp, exact q_pos.2,},
    have : q > 0, { exact q_pos.1 },
    linarith,
  }
end

lemma char_zero_of_exp_char_one (p q : ) [hp: char_p α p] [hq : exp_char α q] :
  q = 1  p = 0 :=
begin
  cases hq.exp_char_def with q_one q_pos,
  { -- q = 1
    haveI := q_one.2,
    have char0' : char_p α 0, { apply_instance },
    have p0 : p = 0 := begin apply char_p.eq α hp char0', end,
    intro q1,
    exact p0,
  },
  { -- q > 0
    intro q1,
    have hq : char_p α 1, { have : char_p α q, { exact q_pos.2 }, rw q1 at this, exact this },
    have : p = 1, { apply char_p.eq α, exact hp, exact hq },
    cases char_p.char_is_prime_or_zero α p with pprime p0,
    { have : 1 < p, { exact nat.prime.one_lt pprime },
      linarith
    },
    { exact p0 }
  }
end

lemma exp_char_one_iff_char_zero (p q : ) [char_p α p] [exp_char α q] :
  q = 1  p = 0 :=
begin
  split,
  { apply char_zero_of_exp_char_one α p q },
  { apply exp_char_one_of_char_zero α p q }
end

/-- The characteristic of a domain equals the exponential characteristic iff the former is positive. -/
lemma char_eq_exp_char_iff (p q : ) [hp: char_p α p] [hq : exp_char α q] :
  p = q  0 < p :=
begin
  cases hq.exp_char_def with q_one q_pos,
  { -- q = 1
    split,
    { intro hpq, rw q_one.1 at hpq, linarith },
    { -- 0 < p → p = q
      haveI := q_one.2,
      have char0' : char_p α 0, { apply_instance },
      have p0 : p = 0 := begin apply char_p.eq α hp char0', end,
      intro ppos,
      linarith
    }
  },
  {
    -- q > 0
    split,
    { -- p = q → 0 < p
      intro hpq, linarith
    },
    { -- 0 < p → p = q
      intro ppos,
      apply char_p.eq α,
      assumption,
      exact q_pos.2
    }
  }
end

theorem exp_char_is_prime_or_one (α : Type u) [integral_domain α] (q : ) [hq : exp_char α q] :
  nat.prime q  q = 1 :=
begin
  by_cases q = 1,
  { exact or.inr h },
  { cases char_p.exists α with p hp,
    haveI := hp,
    have p_ne_zero : p  0,
    { by_contra,
      have p_zero : p = 0, { by_contra, finish },
      have q_one : q = 1, { apply exp_char_one_of_char_zero α p q, assumption },
      finish
    },
    have p_eq_q : p = q,
    { apply (char_eq_exp_char_iff α p q).mpr,
      exact pos_iff_ne_zero.mpr p_ne_zero
    },
    cases char_p.char_is_prime_or_zero α p with pprime p0,
    { have : nat.prime q, { rw p_eq_q at pprime, exact pprime },
      exact or.inl this
    },
    { finish }
  }
end

view this post on Zulip Johan Commelin (Mar 04 2021 at 16:49):

@Jakob Scholbach I'll take a longer look asap, but feel free to call integral domains R or A. The old mathlib style to call every type \alpha has been abandoned in favour of more meaningful variable names

view this post on Zulip Jakob Scholbach (Mar 05 2021 at 16:46):

Yes, thanks. I realize that I should change some of the statements to make it more useful. I will ping you once I have a version that deserves your attention!

view this post on Zulip Jakob Scholbach (Mar 10 2021 at 20:02):

@Johan Commelin : I have made a few edits (pasted right in the first post above), including your requested notational change, but also a few other changes so that it becomes more usable for this ongoing project about separable extensions. If you have time to review it, I would be happy to get some feedback - thanks!

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:20):

@Jakob Scholbach This is certainly starting to look like the start of a useful API around exp_char

view this post on Zulip Jakob Scholbach (Mar 11 2021 at 09:51):

Yes, I have very little insight about what should be contained in such an API. Also, I have little insight as to how to write down these (easy) proofs efficiently, and possibly in a way that is useful for other contexts. So, please mercilessly point out all shortcomings!


Last updated: May 11 2021 at 23:11 UTC