Skip to content

Instantly share code, notes, and snippets.

@kbuzzard
Created May 11, 2021
Embed
What would you like to do?
350 lines of mathlib defs in a self-contained file so I could debug an issue
universe u
set_option old_structure_cmd true
/- 0,+ -/
class add_zero_class (M : Type u) extends has_zero M, has_add M :=
(zero_add : ∀ (a : M), 0 + a = a)
(add_zero : ∀ (a : M), a + 0 = a)
class add_semigroup (G : Type u) extends has_add G :=
(add_assoc : ∀ a b c : G, a + b + c = a + (b + c))
class add_monoid (M : Type u) extends add_semigroup M, add_zero_class M.
class add_comm_semigroup (G : Type u) extends add_semigroup G :=
(add_comm : ∀ a b : G, a + b = b + a)
class add_comm_monoid (M : Type u) extends add_monoid M, add_comm_semigroup M
/- 1,* -/
class mul_one_class (M : Type u) extends has_one M, has_mul M :=
(one_mul : ∀ (a : M), 1 * a = a)
(mul_one : ∀ (a : M), a * 1 = a)
class semigroup (G : Type u) extends has_mul G :=
(mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))
class comm_semigroup (G : Type u) extends semigroup G :=
(mul_comm : ∀ a b : G, a * b = b * a)
def npow_rec {M : Type*} [has_one M] [has_mul M] : ℕ → M → M
| 0 a := 1
| (n+1) a := a * npow_rec n a
class monoid (M : Type u) extends semigroup M, mul_one_class M :=
(npow : ℕ → M → M := npow_rec)
class comm_monoid (M : Type u) extends monoid M, comm_semigroup M
instance monoid.has_pow {M : Type u} [monoid M] : has_pow M ℕ := ⟨λ x n, monoid.npow n x⟩
/- 0 1 * -/
class mul_zero_class (M₀ : Type*) extends has_mul M₀, has_zero M₀ :=
(zero_mul : ∀ a : M₀, 0 * a = 0)
(mul_zero : ∀ a : M₀, a * 0 = 0)
class semigroup_with_zero (S₀ : Type*) extends semigroup S₀, mul_zero_class S₀.
class mul_zero_one_class (M₀ : Type*) extends mul_one_class M₀, mul_zero_class M₀.
class monoid_with_zero (M₀ : Type*) extends monoid M₀, mul_zero_one_class M₀.
/- 0 1 + * -/
class distrib (R : Type*) extends has_mul R, has_add R :=
(left_distrib : ∀ a b c : R, a * (b + c) = (a * b) + (a * c))
(right_distrib : ∀ a b c : R, (a + b) * c = (a * c) + (b * c))
class non_unital_non_assoc_semiring (α : Type u) extends
add_comm_monoid α, distrib α, mul_zero_class α
class non_unital_semiring (α : Type u) extends
non_unital_non_assoc_semiring α, semigroup_with_zero α
class non_assoc_semiring (α : Type u) extends
non_unital_non_assoc_semiring α, mul_zero_one_class α
class semiring (α : Type u) extends non_unital_semiring α, non_assoc_semiring α, monoid_with_zero α
class comm_semiring (α : Type u) extends semiring α, comm_monoid α
/- Morphisms -/
structure zero_hom (M : Type*) (N : Type*) [has_zero M] [has_zero N] :=
(to_fun : M → N)
(map_zero' : to_fun 0 = 0)
structure add_hom (M : Type*) (N : Type*) [has_add M] [has_add N] :=
(to_fun : M → N)
(map_add' : ∀ x y, to_fun (x + y) = to_fun x + to_fun y)
structure add_monoid_hom (M : Type*) (N : Type*) [add_zero_class M] [add_zero_class N]
extends zero_hom M N, add_hom M N
structure one_hom (M : Type*) (N : Type*) [has_one M] [has_one N] :=
(to_fun : M → N)
(map_one' : to_fun 1 = 1)
structure mul_hom (M : Type*) (N : Type*) [has_mul M] [has_mul N] :=
(to_fun : M → N)
(map_mul' : ∀ x y, to_fun (x * y) = to_fun x * to_fun y)
structure monoid_hom (M : Type*) (N : Type*) [mul_one_class M] [mul_one_class N]
extends one_hom M N, mul_hom M N
structure monoid_with_zero_hom (M : Type*) (N : Type*) [mul_zero_one_class M] [mul_zero_one_class N]
extends zero_hom M N, monoid_hom M N
structure ring_hom (α : Type*) (β : Type*) [semiring α] [semiring β]
extends monoid_hom α β, add_monoid_hom α β, monoid_with_zero_hom α β
infixr ` →+* `:25 := ring_hom
instance ring_hom.has_coe_to_fun {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β} :
has_coe_to_fun (α →+* β) := ⟨_, ring_hom.to_fun⟩
def ring_hom.id (α : Type*) [semiring α] : α →+* α :=
{ to_fun := id,
map_zero' := sorry,
map_one' := sorry,
map_add' := sorry,
map_mul' := sorry }
def ring_hom.comp {α β γ : Type*} [rα : semiring α] [rβ : semiring β] {rγ : semiring γ}
(hnp : β →+* γ) (hmn : α →+* β) : α →+* γ :=
{ to_fun := hnp ∘ hmn,
map_zero' := sorry,
map_one' := sorry,
map_add' := sorry,
map_mul' := sorry }
/- subobjects -/
structure add_submonoid (M : Type*) [add_zero_class M] :=
(carrier : set M)
(zero_mem' : (0 : M) ∈ carrier)
(add_mem' {a b} : a ∈ carrier → b ∈ carrier → a + b ∈ carrier)
structure submonoid (M : Type*) [mul_one_class M] :=
(carrier : set M)
(one_mem' : (1 : M) ∈ carrier)
(mul_mem' {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier)
structure subsemiring (R : Type u) [semiring R] extends submonoid R, add_submonoid R
/- nat and facts -/
class fact (p : Prop) : Prop := (out [] : p)
def nat.prime (p : ℕ) := 2 ≤ p ∧ ∀ m ∣ p, m = 1 ∨ m = p
protected def nat.cast {α : Type*} [has_zero α] [has_one α] [has_add α] : ℕ → α
| 0 := 0
| (n+1) := nat.cast n + 1
@[priority 900] instance nat.cast_coe {α : Type*} [_inst_1 : has_zero α] [_inst_2 : has_one α]
[_inst_3 : has_add α] : has_coe_t ℕ α := ⟨nat.cast⟩
class char_p (R : Type*) [add_monoid R] [has_one R] (p : ℕ) : Prop :=
(cast_eq_zero_iff [] : ∀ x:ℕ, (x:R) = 0 ↔ p ∣ x)
/- Pi -/
namespace pi
universes v
variable {I : Type u} -- The indexing type
variable {f : I → Type v} -- The family of types already equipped with instances
variables (x y : Π i, f i) (i : I)
instance has_one [∀ i, has_one $ f i] : has_one (Π i : I, f i) := ⟨λ _, 1⟩
instance has_zero [∀ i, has_zero $ f i] : has_zero (Π i : I, f i) := ⟨λ _, 0⟩
instance has_add [∀ i, has_add $ f i] : has_add (Π i : I, f i) := ⟨λ f g i, f i + g i⟩
instance has_mul [∀ i, has_mul $ f i] : has_mul (Π i : I, f i) := ⟨λ f g i, f i * g i⟩
instance mul_one_class [∀ i, mul_one_class $ f i] : mul_one_class (Π i : I, f i) :=
{ one := (1 : Π i, f i), mul := (*), one_mul := sorry, mul_one := sorry }
instance semiring [∀ i, semiring $ f i] : semiring (Π i : I, f i) :=
{ zero := (0 : Π i, f i), one := 1, add := (+), mul := (*),
add_assoc := sorry,
zero_add := sorry,
add_zero := sorry,
add_comm := sorry,
left_distrib := sorry,
right_distrib := sorry,
zero_mul := sorry,
mul_zero := sorry,
mul_assoc := sorry,
one_mul := sorry,
mul_one := sorry,
}
instance comm_semiring [∀ i, comm_semiring $ f i] : comm_semiring (Π i : I, f i) :=
{ zero := (0 : Π i, f i), one := 1, add := (+), mul := (*),
add_assoc := sorry,
zero_add := sorry,
add_zero := sorry,
add_comm := sorry,
left_distrib := sorry,
right_distrib := sorry,
zero_mul := sorry,
mul_zero := sorry,
mul_assoc := sorry,
one_mul := sorry,
mul_one := sorry,
mul_comm := sorry }
end pi
/- setlike -/
class set_like (A : Type*) (B : out_param $ Type*) :=
(coe : A → set B)
(coe_injective' : function.injective coe)
instance submonoid.set_like {M : Type*} [mul_one_class M] : set_like (submonoid M) M :=
⟨submonoid.carrier, sorry⟩
instance add_submonoid.set_like {M : Type*} [add_zero_class M] : set_like (add_submonoid M) M :=
⟨add_submonoid.carrier, sorry⟩
instance subsemiring.set_like {R : Type*} [semiring R] : set_like (subsemiring R) R :=
⟨subsemiring.carrier, sorry⟩
namespace set_like
variables {A : Type*} {B : Type*} [i : set_like A B]
include i
instance : has_coe_t A (set B) := ⟨set_like.coe⟩
@[priority 100]
instance : has_mem B A := ⟨λ x p, x ∈ (p : set B)⟩
-- `dangerous_instance` does not know that `B` is used only as an `out_param`
instance : has_coe_to_sort A := ⟨_, λ p, {x : B // x ∈ p}⟩
end set_like
/- coercion from subobject to object -/
theorem subtype.coe_injective {α : Type*} {p : α → Prop} :
function.injective (coe : subtype p → α) := sorry
protected def function.injective.add_semigroup {M₁ : Type*} {M₂ : Type*} [has_add M₁] [add_semigroup M₂]
(f : M₁ → M₂) (hf : function.injective f)
(add : ∀ x y, f (x + y) = f x + f y) :
add_semigroup M₁ :=
{ add_assoc := sorry,
..‹has_add M₁› }
protected def function.injective.semigroup {M₁ : Type*} {M₂ : Type*} [has_mul M₁] [semigroup M₂] (f : M₁ → M₂)
(hf : function.injective f)
(mul : ∀ x y, f (x * y) = f x * f y) :
semigroup M₁ :=
{ mul_assoc := sorry,
..‹has_mul M₁› }
protected def function.injective.add_comm_semigroup {M₁ : Type*} {M₂ : Type*} [has_add M₁]
[add_comm_semigroup M₂] (f : M₁ → M₂) (hf : function.injective f)
(add : ∀ x y, f (x + y) = f x + f y) :
add_comm_semigroup M₁ :=
{ add_comm := sorry,
.. hf.add_semigroup f add }
protected def function.injective.add_zero_class {M₁ : Type*} {M₂ : Type*} [has_zero M₁] [has_add M₁]
[add_zero_class M₂] (f : M₁ → M₂) (hf : function.injective f)
(zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) :
add_zero_class M₁ :=
{ zero_add := sorry,
add_zero := sorry,
..‹has_zero M₁›, ..‹has_add M₁› }
protected def function.injective.mul_one_class {M₁ : Type*} {M₂ : Type*} [has_one M₁] [has_mul M₁] [mul_one_class M₂] (f : M₁ → M₂) (hf : function.injective f)
(one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) :
mul_one_class M₁ :=
{ one_mul := sorry,
mul_one := sorry,
..‹has_one M₁›, ..‹has_mul M₁› }
protected def function.injective.add_monoid {M₁ : Type*} {M₂ : Type*} [has_zero M₁] [has_add M₁] [add_monoid M₂]
(f : M₁ → M₂) (hf : function.injective f)
(zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) :
add_monoid M₁ :=
{ .. hf.add_semigroup f add, .. hf.add_zero_class f zero add }
protected def function.injective.monoid {M₁ : Type*} {M₂ : Type*} [has_one M₁] [has_mul M₁] [monoid M₂]
(f : M₁ → M₂) (hf : function.injective f)
(one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) :
monoid M₁ :=
{ .. hf.semigroup f mul, .. hf.mul_one_class f one mul }
protected def function.injective.add_comm_monoid {M₁ : Type*} {M₂ : Type*} [has_zero M₁] [has_add M₁]
[add_comm_monoid M₂] (f : M₁ → M₂) (hf : function.injective f)
(zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) :
add_comm_monoid M₁ :=
{ .. hf.add_comm_semigroup f add, .. hf.add_monoid f zero add }
instance add_submonoid.has_zero {M : Type*} [add_zero_class M] (S : add_submonoid M): has_zero S := ⟨⟨0, sorry⟩⟩
instance submonoid.has_one {M : Type*} [mul_one_class M] (S : submonoid M): has_one S := ⟨⟨1, sorry⟩⟩
instance submonoid.has_add {M : Type*} [add_zero_class M] (S : add_submonoid M): has_add S := ⟨λ a b, ⟨a.1 + b.1, sorry⟩⟩
instance submonoid.has_mul {M : Type*} [mul_one_class M] (S : submonoid M): has_mul S := ⟨λ a b, ⟨a.1 * b.1, sorry⟩⟩
instance submonoid.to_monoid {M : Type*} [monoid M] (S : submonoid M) : monoid S :=
subtype.coe_injective.monoid coe sorry sorry
instance add_submonoid.to_add_comm_monoid {M} [add_comm_monoid M] (S : add_submonoid M) : add_comm_monoid S :=
subtype.coe_injective.add_comm_monoid coe rfl (λ _ _, rfl)
instance subsemiring.to_semiring {R : Type u} [semiring R] (s : subsemiring R) : semiring s :=
{ mul_zero := sorry,
zero_mul := sorry,
right_distrib := sorry,
left_distrib := sorry,
.. s.to_submonoid.to_monoid, .. s.to_add_submonoid.to_add_comm_monoid }
instance subsemiring.to_comm_semiring {R} [comm_semiring R] (s : subsemiring R) : comm_semiring s :=
{ mul_comm := sorry, ..s.to_semiring}
/- char p ring theory -/
def monoid.perfection (M : Type*) [comm_monoid M] (p : ℕ) : submonoid (ℕ → M) :=
{ carrier := { f | ∀ n, f (n + 1) ^ p = f n },
one_mem' := sorry,
mul_mem' := sorry }
def ring.perfection (R : Type*) [comm_semiring R]
(p : ℕ) [hp : fact p.prime] [char_p R p] :
subsemiring (ℕ → R) :=
{ zero_mem' := sorry,
add_mem' := sorry,
.. monoid.perfection R p }
instance char_p.subsemiring (R : Type u) [semiring R] (p : ℕ) [char_p R p] (S : subsemiring R) :
char_p S p := ⟨sorry⟩
instance char_p.pi (ι : Type u) [hi : nonempty ι] (R : Type*) [semiring R] (p : ℕ) [char_p R p] :
char_p (ι → R) p := ⟨sorry⟩
def frobenius (R : Type*) [comm_semiring R] (p : ℕ) [fact p.prime] [char_p R p] : R →+* R :=
{ to_fun := λ x, x^p,
map_one' := sorry,
map_mul' := sorry,
map_zero' := sorry,
map_add' := sorry }
def perfection.coeff (R : Type*) [comm_semiring R] (p : ℕ) [hp : fact (nat.prime p)]
[_inst_2 : char_p R p] (n : ℕ) : ring.perfection R p →+* R :=
{ to_fun := λ f, f.1 n,
map_one' := rfl,
map_mul' := λ f g, rfl,
map_zero' := rfl,
map_add' := λ f g, rfl }
/-- The `p`-th root of an element of the perfection. -/
def pth_root (R : Type*) [comm_semiring R] (p : ℕ) [hp : fact (nat.prime p)] [char_p R p] :
ring.perfection R p →+* ring.perfection R p :=
{ to_fun := λ f, ⟨λ n, perfection.coeff R p (n + 1) f, λ n, f.2 _⟩,
map_one' := rfl,
map_mul' := λ f g, rfl,
map_zero' := rfl,
map_add' := λ f g, rfl }
lemma frobenius_pth_root {R : Type u} {p : ℕ} [comm_semiring R] [hp : fact (nat.prime p)] [char_p R p] :
(frobenius (ring.perfection R p) p).comp (pth_root R p) = ring_hom.id (ring.perfection R p) :=
sorry
-- Type* not Type u causes timeout
lemma frobenius_pth_root_bad {R : Type*} {p : ℕ} [comm_semiring R] [hp : fact (nat.prime p)] [char_p R p] :
(frobenius (ring.perfection R p) p).comp (pth_root R p) = ring_hom.id (ring.perfection R p) :=
sorry
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment