Exponential characteristic

Stream: new members

[Jakob Scholbach]

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

[Johan Commelin]

@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

[Jakob Scholbach]

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!

[Jakob Scholbach]

@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!

[Johan Commelin]

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

[Jakob Scholbach]

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!