## Stream: new members

### Topic: Exponential characteristic

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


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

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

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

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

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