## Stream: maths

### Topic: derivation

#### Kenny Lau (Jul 12 2019 at 15:21):

import ring_theory.algebra

universes u v w u₁ v₁ w₁

variables (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [algebra R A]
variables (M : Type w) [add_comm_group M] [module A M]

-- include R A
-- def module.comap := M
-- omit R A

-- def module.to_comap : M → module.comap R A M := id
-- def module.of_comap : module.comap R A M → M := id

-- namespace module.comap

-- instance : add_comm_group (module.comap R A M) := _inst_4

-- instance module_right : module A (module.comap R A M) := _inst_5

-- instance module_left : module R (module.comap R A M) :=
-- { smul := λ r m, module.to_comap R A M (algebra_map A r • module.of_comap R A M m),
--   one_smul := λ m, show module.to_comap R A M (algebra_map A (1:R) • module.of_comap R A M m) = m,
--     by rw [algebra.map_one, one_smul]; refl,
--   mul_smul := λ r1 r2 m, show module.to_comap R A M (algebra_map A _ • _) = _,
--     by rw [algebra.map_mul, mul_smul]; refl,
--   smul_add := λ r m1 m2, by convert smul_add (algebra_map A r) (module.of_comap R A M m1) (module.of_comap R A M m2),
--   smul_zero := λ r, by convert smul_zero (algebra_map A r),
--   add_smul := λ r1 r2 m, show module.to_comap R A M (algebra_map A _ • _) = _,
--   zero_smul := λ m, show module.to_comap R A M (algebra_map A (0:R) • module.of_comap R A M m) = 0,
--     by rw [algebra.map_zero, zero_smul]; refl }

-- end module.comap

structure derivation :=
(to_fun : A → M)
(add : ∀ x y, to_fun (x + y) = to_fun x + to_fun y)
(mul : ∀ x y, to_fun (x * y) = x • to_fun y + y • to_fun x)
(algebra : ∀ r : R, to_fun (algebra_map A r) = 0)

theorem mul_comm₄ {α : Type u} [comm_semigroup α] (a b c d : α) :
(a * b) * (c * d) = (a * c) * (b * d) :=
by rw [mul_assoc, mul_assoc, mul_left_comm b]

namespace derivation

instance : has_coe_to_fun (derivation R A M) :=
⟨λ D, A → M, derivation.to_fun⟩

section
variables {R A M} (D : derivation R A M) (r : R) (a b : A)
theorem map_add : D (a + b) = D a + D b := D.add a b
theorem map_zero : D 0 = 0 := @@is_add_group_hom.map_zero _ _ _ ⟨D.add⟩
theorem map_neg : D (-a) = -D a := @@is_add_group_hom.map_neg _ _ _ ⟨D.add⟩ _
theorem map_sub : D (a - b) = D a - D b := @@is_add_group_hom.map_sub _ _ _ ⟨D.add⟩ _ _
theorem map_mul : D (a * b) = a • D b + b • D a := D.mul a b
theorem map_mul_comm : D (a * b) = b • D a + a • D b := (D.mul a b).trans $add_comm _ _ theorem map_algebra_map : D (algebra_map A r) = 0 := D.algebra r @[extensionality] theorem ext : Π {D1 D2 : derivation R A M}, (∀ a, D1 a = D2 a) → D1 = D2 | ⟨f, _, _, _⟩ ⟨g, _, _, _⟩ H := mk.inj_eq.mpr$ funext H
end

instance : add_comm_group (derivation R A M) :=
by refine
{ add := λ D1 D2, ⟨λ a, D1 a + D2 a,
λ a1 a2, by rw [D1.map_mul, D2.map_mul, smul_add, smul_add, add_comm₄],
λ r, by rw [D1.map_algebra_map, D2.map_algebra_map, add_zero]⟩,
zero := ⟨λ a, 0,
λ a1 a2, by rw add_zero,
λ a1 a2, by rw [smul_zero, smul_zero, add_zero],
λ r, rfl⟩,
neg := λ D, ⟨λ a, -D a,
λ a1 a2, by rw [D.map_add, neg_add],
λ a1 a2, by rw [D.map_mul, neg_add, smul_neg, smul_neg],
λ r, by rw [D.map_algebra_map, neg_zero]⟩,
.. };
{ intros, ext, exact add_assoc _ _ _ <|> exact zero_add _ <|>
exact add_zero _ <|> exact add_left_neg _ <|> exact add_comm _ _ }

instance : module A (derivation R A M) :=
{ smul := λ a D, ⟨λ b, a • D b,
λ a1 a2, by rw [D.map_add, smul_add],
λ a1 a2, by rw [D.map_mul, smul_add, smul_smul, smul_smul, mul_comm, mul_smul, mul_comm, mul_smul],
λ s, by rw [D.map_algebra_map, smul_zero]⟩,
mul_smul := λ a1 a2 D, ext $λ b, mul_smul _ _ _, one_smul := λ D, ext$ λ b, one_smul A _,
smul_add := λ a D1 D2, ext $λ b, smul_add _ _ _, smul_zero := λ a, ext$ λ b, smul_zero _,
add_smul := λ a1 a2 D, ext $λ b, add_smul _ _ _, zero_smul := λ D, ext$ λ b, zero_smul A _ }

section
variables {R A M} (a : A) (D D1 D2 : derivation R A M) (b : A)
@[simp] lemma add_apply : (D1 + D2) b = D1 b + D2 b := rfl
@[simp] lemma zero_apply : (0 : derivation R A M) b = 0 := rfl
@[simp] lemma neg_apply : (-D) b = -(D b) := rfl
@[simp] lemma sub_apply : (D1 - D2) b = D1 b - D2 b := rfl
set_option class.instance_max_depth 41
@[simp] lemma smul_apply : (a • D) b = a • (D b) := rfl
end

variables {R A M}
def comp {N : Type u₁} [add_comm_group N] [module A N]
(D : derivation R A M) (f : M →ₗ[A] N) : derivation R A N :=
{ to_fun := λ a, f (D a),
mul := λ a1 a2, by rw [D.map_mul, f.map_add, f.map_smul, f.map_smul],
algebra := λ r, by rw [D.map_algebra_map, f.map_zero] }

end derivation

variables (R A)

def «Kähler».relators : set (free_abelian_group (A × A)) :=
{ x : free_abelian_group (A × A) |
(∃ a b c : A, free_abelian_group.of (a + b, c) - (free_abelian_group.of (a, c) + free_abelian_group.of (b, c)) = x) ∨
(∃ a b c : A, free_abelian_group.of (a, b + c) - (free_abelian_group.of (a, b) + free_abelian_group.of (a, c)) = x) ∨
(∃ a b c : A, free_abelian_group.of (a, b * c) - (free_abelian_group.of (a * b, c) + free_abelian_group.of (a * c, b)) = x) ∨
(∃ a : A, ∃ r : R, free_abelian_group.of (a, algebra_map A r) = x) }

def «Kähler» : Type v :=
quotient_add_group.quotient $add_group.closure$ «Kähler».relators R A

namespace «Kähler»

instance : normal_add_subgroup (add_group.closure (relators R A)) :=
{ normal := λ n hn g, by rwa add_sub_cancel' }

instance : has_scalar A («Kähler» R A) :=
begin
refine ⟨λ a, quotient_add_group.lift _
(free_abelian_group.lift $λ p : A × A, quotient_add_group.mk$ free_abelian_group.of (a * p.1, p.2)) _⟩,
intros x hx, refine add_group.in_closure.rec_on hx _ _ _ _,
{ intros y hy, rcases hy with ⟨b,c,d,rfl⟩ | ⟨b,c,d,rfl⟩ | ⟨b,c,d,rfl⟩ | ⟨b,r,rfl⟩,
{ rw [free_abelian_group.lift.sub, free_abelian_group.lift.add,
free_abelian_group.lift.of, free_abelian_group.lift.of, free_abelian_group.lift.of],
refine eq.symm (quotient.sound' _),
change _ ∈ _, rw [neg_zero, zero_add, mul_add],
exact add_group.subset_closure (or.inl ⟨_, _, _, rfl⟩) },
{ rw [free_abelian_group.lift.sub, free_abelian_group.lift.add,
free_abelian_group.lift.of, free_abelian_group.lift.of, free_abelian_group.lift.of],
refine eq.symm (quotient.sound' _),
change _ ∈ _, rw [neg_zero, zero_add],
exact add_group.subset_closure (or.inr $or.inl ⟨_, _, _, rfl⟩) }, { rw [free_abelian_group.lift.sub, free_abelian_group.lift.add, free_abelian_group.lift.of, free_abelian_group.lift.of, free_abelian_group.lift.of], refine eq.symm (quotient.sound' _), change _ ∈ _, rw [neg_zero, zero_add, ← mul_assoc, ← mul_assoc], exact add_group.subset_closure (or.inr$ or.inr $or.inl ⟨_, _, _, rfl⟩) }, { rw free_abelian_group.lift.of, refine eq.symm (quotient.sound' _), change _ ∈ _, rw [neg_zero, zero_add], exact add_group.subset_closure (or.inr$ or.inr $or.inr ⟨_, _, rfl⟩) } }, { exact free_abelian_group.lift.zero _ }, { intros x hx ih, rw [free_abelian_group.lift.neg, ih, neg_zero] }, { intros x y hx hy ihx ihy, rw [free_abelian_group.lift.add, ihx, ihy, add_zero] } end instance : module A («Kähler» R A) := begin refine { smul := (•), .. }, { intros x, refine quotient_add_group.induction_on x (λ p, _), dsimp only [(•)], rw quotient_add_group.lift_mk', refine free_abelian_group.induction_on p rfl _ _ _, { rintros ⟨p1, p2⟩, rw [free_abelian_group.lift.of, one_mul] }, { intros p ih, rw [free_abelian_group.lift.neg, ih], refl }, { intros p q ihp ihq, rw [free_abelian_group.lift.add, ihp, ihq], refl } }, { intros a1 a2 x, refine quotient_add_group.induction_on x (λ p, _), dsimp only [(•)], simp only [quotient_add_group.lift_mk'], refine free_abelian_group.induction_on p rfl _ _ _, { rintros ⟨p1, p2⟩, rw [free_abelian_group.lift.of, free_abelian_group.lift.of, quotient_add_group.lift_mk', free_abelian_group.lift.of, ← mul_assoc] }, { intros p ih, rw [free_abelian_group.lift.neg, free_abelian_group.lift.neg, ih], refl }, { intros p q ihp ihq, rw [free_abelian_group.lift.add, free_abelian_group.lift.add, ihp, ihq, is_add_group_hom.map_add (quotient_add_group.lift _ _ _)], apply_instance } }, { intros r x y, exact is_add_group_hom.map_add (quotient_add_group.lift _ _ _) _ _ }, { intros r, exact is_add_group_hom.map_zero (quotient_add_group.lift _ _ _) }, { intros r s x, refine quotient_add_group.induction_on x (λ p, _), dsimp only [(•)], simp only [quotient_add_group.lift_mk'], refine free_abelian_group.induction_on p rfl _ _ _, { rintros ⟨p1, p2⟩, rw [free_abelian_group.lift.of, free_abelian_group.lift.of, free_abelian_group.lift.of, add_mul], refine eq.symm (quotient.sound' (_ : _ ∈ _)), rw add_comm, exact add_group.subset_closure (or.inl ⟨_, _, _, rfl⟩) }, { intros p ih, rw [free_abelian_group.lift.neg, ih, neg_add], refl }, { intros p q ihp ihq, rw [free_abelian_group.lift.add, free_abelian_group.lift.add, free_abelian_group.lift.add, ihp, ihq, add_comm₄] } }, { intros x, refine quotient_add_group.induction_on x (λ p, _), dsimp only [(•)], simp only [quotient_add_group.lift_mk'], refine free_abelian_group.induction_on p rfl _ _ _, { rintros ⟨p1, p2⟩, rw [free_abelian_group.lift.of, zero_mul], refine quotient.sound' (_ : _ ∈ _), rw add_zero, refine add_group.subset_closure (or.inl ⟨0, 0, p2, _⟩), rw [← sub_sub, add_zero, sub_self, zero_sub] }, { intros p ih, rw [free_abelian_group.lift.neg, ih, neg_zero] }, { intros p q ihp ihq, rw [free_abelian_group.lift.add, ihp, ihq, add_zero] } } end  #### Kenny Lau (Jul 12 2019 at 15:22): def D : derivation R A («Kähler» R A) := { to_fun := λ a, quotient_add_group.mk$ free_abelian_group.of (1, a),
add := λ a b, eq.symm $quotient.sound'$ show _ ∈ _,
by rw add_comm; exact add_group.subset_closure (or.inr $or.inl ⟨_, _, _, rfl⟩), mul := λ a b, by dsimp only [(•)]; simp only [quotient_add_group.lift_mk', free_abelian_group.lift.of, mul_comm _ (1:A)]; exact eq.symm (quotient.sound'$ add_group.subset_closure $or.inr$ or.inr $or.inl ⟨1, a, b, by rw sub_eq_neg_add⟩), algebra := λ r, eq.symm$ quotient.sound' $add_group.subset_closure$ or.inr $or.inr$ or.inr ⟨1, r, by rw [neg_zero, zero_add]⟩ }

variables {R A}

theorem smul_D (a b : A) : a • D R A b = quotient_add_group.mk (free_abelian_group.of (a, b)) :=
by dsimp only [(•), D]; erw [quotient_add_group.lift_mk', free_abelian_group.lift.of, mul_one]

@[elab_as_eliminator] theorem induction_on {C : «Kähler» R A → Prop} (p : «Kähler» R A)
(hd : ∀ a b, C ((a : A) • D R A b)) (ha : ∀ a b, C a → C b → C (a+b)) : C p :=
quotient_add_group.induction_on p $λ p, free_abelian_group.induction_on p (by simpa only [zero_smul] using hd 0 0) (λ ⟨a, b⟩, by have := hd a b; rwa smul_D at this) (λ ⟨a, b⟩ ih, by have := hd (-a) b; rwa [neg_smul, smul_D] at this) (λ _ _, ha _ _) @[elab_as_eliminator] theorem induction_on' {C : «Kähler» R A → Prop} (p : «Kähler» R A) (hd : ∀ a b, C (quotient_add_group.mk$ free_abelian_group.of (a, b))) (ha : ∀ a b, C a → C b → C (a+b)) : C p :=
induction_on p (λ a b, by rw smul_D; apply hd) ha

end «Kähler»

namespace derivation

variables {R A M}

def factor (D : derivation R A M) : «Kähler» R A →ₗ[A] M :=
{ to_fun := quotient_add_group.lift _ (free_abelian_group.lift $λ p, p.1 • D p.2)$ λ x hx,
(λ p hp, or.cases_on hp
(by rintros ⟨a,b,c,rfl⟩; simp only [free_abelian_group.lift.add, free_abelian_group.lift.sub,
free_abelian_group.lift.of, add_smul, sub_self]) $λ hp, or.cases_on hp (by rintros ⟨a,b,c,rfl⟩; simp only [free_abelian_group.lift.add, free_abelian_group.lift.sub, free_abelian_group.lift.of, D.map_add, smul_add, sub_self])$ λ hp, or.cases_on hp
(by rintros ⟨a,b,c,rfl⟩; simp only [free_abelian_group.lift.add, free_abelian_group.lift.sub,
free_abelian_group.lift.of, D.map_mul, smul_add, mul_smul, sub_self])
(by rintros ⟨a,r,rfl⟩; simp only [free_abelian_group.lift.add, free_abelian_group.lift.sub,
free_abelian_group.lift.of, D.map_algebra_map, smul_zero, sub_self]))
(free_abelian_group.lift.zero _)
(λ p hp ih, by rw [free_abelian_group.lift.neg, ih, neg_zero])
(λ p q hp hq ihp ihq, by rw [free_abelian_group.lift.add, ihp, ihq, add_zero]),
smul := λ a p, «Kähler».induction_on p
(λ b c, by rw [smul_smul, «Kähler».smul_D, quotient_add_group.lift_mk', free_abelian_group.lift.of,
«Kähler».smul_D, quotient_add_group.lift_mk', free_abelian_group.lift.of, mul_smul])
(λ q r ihq ihr, by rw [smul_add, is_add_group_hom.map_add (quotient_add_group.lift _ _ _), ihq, ihr,

theorem factor_comp (D : derivation R A M) : («Kähler».D R A).comp D.factor = D :=
ext $λ a, by dsimp only [comp, factor, «Kähler».D, coe_fn, has_coe_to_fun.coe]; erw [quotient_add_group.lift_mk', free_abelian_group.lift.of, one_smul] theorem factor_D (D : derivation R A M) (a : A) : D.factor («Kähler».D R A a) = D a := by conv_rhs { rw ← D.factor_comp }; refl theorem comp_factor (f : «Kähler» R A →ₗ[A] M) : ((«Kähler».D R A).comp f).factor = f := linear_map.ext$ λ p, «Kähler».induction_on' p
(λ a b, by dsimp only [comp, factor, coe_fn, has_coe_to_fun.coe];
rw [quotient_add_group.lift_mk', free_abelian_group.lift.of, ← «Kähler».smul_D, f.smul]; refl)
(λ p q ihp ihq, by rw [f.map_add, linear_map.map_add, ihp, ihq])

def linear_equiv : derivation R A M ≃ₗ[A] («Kähler» R A →ₗ[A] M) :=
{ to_fun := factor,
inv_fun := comp («Kähler».D R A),
left_inv := λ D, D.factor_comp,
right_inv := λ f, comp_factor f,
add := λ D1 D2, linear_map.ext $λ p, «Kähler».induction_on p (λ a b, by rw [linear_map.map_smul, linear_map.map_smul, linear_map.add_apply, factor_D, factor_D, factor_D, derivation.add_apply]) (λ p q ihp ihq, by rw [linear_map.map_add, linear_map.map_add, ihp, ihq]), smul := λ a D, linear_map.ext$ λ p, «Kähler».induction_on p
(λ b c, by rw [linear_map.smul_apply, linear_map.map_smul, linear_map.map_smul,
factor_D, factor_D, derivation.smul_apply, smul_smul, smul_smul, mul_comm])
(λ p q ihp ihq, by rw [linear_map.map_add, linear_map.map_add, ihp, ihq]) }

end derivation

@[monotonicity] theorem multiset.to_finset_mono {α : Type u} [decidable_eq α]
{m₁ m₂ : multiset α} (h : m₁ ⊆ m₂) : m₁.to_finset ⊆ m₂.to_finset :=
λ i, by rw [multiset.mem_to_finset, multiset.mem_to_finset]; exact @h i

namespace finsupp

local attribute [instance] finsupp.to_has_scalar'
lemma sum_smul_index' {α : Type u} {β : Type v} {γ : Type w} [decidable_eq α] [decidable_eq β]
[semiring β] [add_comm_monoid γ] {g : α →₀ β} {b : β} {h : α → β → γ}
(h0 : ∀i, h i 0 = 0) : (b • g).sum h = g.sum (λi a, h i (b * a)) :=
sum_map_range_index h0

lemma single_eq_smul_one {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] [comm_semiring β]
(a : α) (b : β) :
single a b = b • single a 1 :=
by rw [smul_single, smul_eq_mul, mul_one]

end finsupp

namespace mv_polynomial

variables {σ : Type u} [decidable_eq σ]
variables {α : Type v} [comm_semiring α] [decidable_eq α]
variables (i j : σ) (p q : mv_polynomial σ α) (r : α)

def partial_deriv : mv_polynomial σ α :=
-- p.sum $λ v r, C r * (add_monoid.smul (v i) (X i ^ (v i - 1)) * v.prod (λ j n, if i = j then 1 else (mv_polynomial.X j)^n)) p.sum$ λ v r, finsupp.single (v.sum $λ j n, finsupp.single j (if i = j then n-1 else n)) (add_monoid.smul (v i) r) -- #exit theorem partial_deriv_add : (p + q).partial_deriv i = p.partial_deriv i + q.partial_deriv i := finsupp.sum_add_index (λ v, by rw [add_monoid.smul_zero, finsupp.single_zero]; refl)$

theorem partial_deriv_zero : (0 : mv_polynomial σ α).partial_deriv i = 0 :=
finsupp.sum_zero_index

theorem partial_deriv_C : (C r).partial_deriv i = 0 :=
(finsupp.sum_single_index $by rw [add_monoid.smul_zero, finsupp.single_zero]; refl).trans$
by rw [finsupp.zero_apply, add_monoid.zero_smul, finsupp.single_zero]; refl

theorem partial_deriv_X : (X i : mv_polynomial σ α).partial_deriv j = if i = j then 1 else 0 :=
begin
rw [partial_deriv, X, monomial, finsupp.sum_single_index, finsupp.sum_single_index, nat.sub_self, finsupp.single_apply],
{ split_ifs with hji hij hij,
{ rw [add_monoid.one_smul, finsupp.single_zero], refl },
{ exact absurd hji.symm hij },
{ exact absurd hij.symm hji },
{ rw [add_monoid.zero_smul, finsupp.single_zero], refl } },
{ split_ifs with hji,
{ rw [nat.zero_sub, finsupp.single_zero] },
{ rw finsupp.single_zero } },
{ rw [add_monoid.smul_zero, finsupp.single_zero], refl }
end

theorem partial_deriv_one : (1 : mv_polynomial σ α).partial_deriv i = 0 :=
by rw [← C_1, partial_deriv_C]

instance : semimodule α (mv_polynomial σ α) := finsupp.to_semimodule _ _

theorem C_mul'' : C r * p = r • p :=
begin
refine finsupp.induction p _ _,
{ exact (mul_zero _).trans (smul_zero _).symm },
{ intros v s f hfv hs ih,
rw [C, monomial, finsupp.mul_def, finsupp.sum_single_index, finsupp.sum_single_index, zero_add],
rw [finsupp.smul_single, smul_eq_mul],
{ rw [mul_zero, finsupp.single_zero] },
{ rw [finsupp.sum_single_index]; rw [zero_mul, finsupp.single_zero] } }
end

theorem partial_deriv_smul : (r • p).partial_deriv i = r • p.partial_deriv i :=
begin
rw [partial_deriv, finsupp.sum_smul_index', partial_deriv, ← C_mul'', finsupp.mul_sum], refine finset.sum_congr rfl _,
{ intros v hv, dsimp only, rw [add_monoid.smul_eq_mul, add_monoid.smul_eq_mul, mul_left_comm, ← smul_eq_mul, ← finsupp.smul_single, C_mul''] },
{ intros v, rw [add_monoid.smul_zero, finsupp.single_zero], refl }
end


#### Kenny Lau (Jul 12 2019 at 15:22):

theorem partial_deriv_mul : (p * q).partial_deriv i = p * q.partial_deriv i + q * p.partial_deriv i :=
begin
have : ∀ v w : σ →₀ ℕ, w i ≠ 0 → finsupp.sum (v + w) (λ (j : σ) (n : ℕ), finsupp.single j (ite (i = j) (n - 1) n)) =
v + finsupp.sum w (λ (j : σ) (n : ℕ), finsupp.single j (ite (i = j) (n - 1) n)),
{ intros v w hw, ext j,
rw [finsupp.sum_apply, finsupp.add_apply, finsupp.sum_apply, finsupp.sum, finset.sum_eq_single j, finsupp.sum, finset.sum_eq_single j],
{ rw [finsupp.single_apply, finsupp.single_apply, if_pos rfl, if_pos rfl], split_ifs with hij,
{ subst hij, rw [finsupp.add_apply, nat.add_sub_assoc], exact nat.one_le_of_lt (nat.pos_of_ne_zero hw) },
{ refl } },
{ intros k hk hkj, rw [finsupp.single_apply, if_neg hkj] },
{ intros hjw, rw [finsupp.single_apply, if_pos rfl], split_ifs; rw [finsupp.not_mem_support_iff.1 hjw] },
{ intros k hk hkj, rw [finsupp.single_apply, if_neg hkj] },
{ intros hjw, rw [finsupp.single_apply, if_pos rfl], split_ifs; rw [finsupp.not_mem_support_iff.1 hjw] } },
refine finsupp.induction p _ (λ v r p hpv hr ihp, _),
{ erw zero_mul, rw zero_add, erw partial_deriv_zero, rw mul_zero },
rw [add_mul, partial_deriv_add], refine eq.trans (congr_arg _ ihp) _,
refine finsupp.induction q _ (λ w s q hqw hs ihq, _),
{ erw mul_zero, rw zero_add, erw zero_mul, rw partial_deriv_zero },
rw [mul_add, partial_deriv_add], refine eq.trans (congr_arg _ ihq) _,
rw [finsupp.single_mul_single, finsupp.single_eq_smul_one v r, finsupp.single_eq_smul_one w s, finsupp.single_eq_smul_one (v+w) (r*s)],
rw [partial_deriv_smul, partial_deriv_smul, partial_deriv_smul, ← C_mul'', ← C_mul'', ← C_mul'', ← C_mul'', ← C_mul''],
rw [mul_comm₄, ← C_mul, mul_comm₄, ← C_mul, mul_comm s r, ← mul_add], congr' 1,
rw [partial_deriv, finsupp.sum_single_index], swap, { rw [add_monoid.smul_zero, finsupp.single_zero], refl },
rw [partial_deriv, finsupp.sum_single_index], swap, { rw [add_monoid.smul_zero, finsupp.single_zero], refl },
rw [partial_deriv, finsupp.sum_single_index], swap, { rw [add_monoid.smul_zero, finsupp.single_zero], refl },
rw [finsupp.add_apply, finsupp.single_mul_single, finsupp.single_mul_single, one_mul, one_mul],
by_cases hv : v i = 0,
by_cases hw : w i = 0,
{ rw [hw, add_monoid.zero_smul, finsupp.single_zero, finsupp.single_zero] },
{ rw [this v w hw] } },
by_cases hw : w i = 0,
{ rw [hw, add_monoid.zero_smul, finsupp.single_zero, add_zero], erw zero_add, rw [add_comm v w, this w v hv] },
{ rw this v w hw }, { rw [add_comm v w, this w v hv] }
end

theorem vars_add : (p + q).vars ⊆ p.vars ∪ q.vars :=
λ i, by unfold vars; simp only [finset.mem_union, multiset.mem_to_finset]; exact
λ hi, multiset.mem_add.1 (multiset.subset_of_le
(le_trans (degrees_add p q) $lattice.sup_le (multiset.le_add_right _ _) (multiset.le_add_left _ _)) hi) theorem vars_mul : (p * q).vars ⊆ p.vars ∪ q.vars := λ i, by unfold vars; simp only [finset.mem_union, multiset.mem_to_finset]; exact λ hi, multiset.mem_add.1 (multiset.subset_of_le (degrees_mul p q) hi) theorem vars_X_subset : vars (X i : mv_polynomial σ α) ⊆ {i} := λ j hj, multiset.subset_of_le (degrees_X i)$ multiset.mem_to_finset.1 hj

theorem of_not_mem_vars (h : i ∉ p.vars) (v : σ →₀ ℕ) (hv : v ∈ p.support) : v i = 0 :=
finsupp.not_mem_support_iff.1 $λ hiv, h$
have h1 : v.to_multiset ≤ p.degrees := finset.le_sup hv,
have h2 : _ ≤ v.to_multiset := finset.single_le_sum (λ _ _, multiset.zero_le _) hiv,
multiset.mem_to_finset.2 $multiset.subset_of_le h1$ multiset.subset_of_le h2 $by rw ← nat.succ_pred_eq_of_pos (nat.pos_of_ne_zero$ finsupp.mem_support_iff.1 hiv); exact
multiset.mem_cons_self _ _

theorem partial_deriv_of_not_mem_vars (h : i ∉ p.vars) : p.partial_deriv i = 0 :=
finset.sum_eq_zero \$ λ v hv, by dsimp only; rw [of_not_mem_vars i p h v hv, add_monoid.zero_smul, finsupp.single_zero]; refl

end mv_polynomial

namespace derivation

variables {σ : Type u} [decidable_eq σ]
variables {α : Type v} [comm_ring α] [decidable_eq α]
variables (i : σ) (p q : mv_polynomial σ α) (r : α)

/- protected def mv_polynomial : derivation α (mv_polynomial σ α) (mv_polynomial σ α) :=
{ to_fun := mv_polynomial.partial_deriv i,
mul := mv_polynomial.partial_deriv_mul i,
algebra := mv_polynomial.partial_deriv_C i } -/

theorem mv_polynomial_eval [decidable_eq R] {ι : Type v} [decidable_eq ι]
(D : derivation R A M) (p : mv_polynomial ι R) (f : ι → A) :
D (p.eval₂ (algebra_map A) f) = p.vars.sum (λ i, (p.partial_deriv i).eval₂ (algebra_map A) f • D (f i)) :=
begin
have : ∀ p : mv_polynomial ι R, ∀ q : finset ι, p.vars ⊆ q →
p.vars.sum (λ i, (p.partial_deriv i).eval₂ (algebra_map A) f • D (f i)) =
q.sum (λ i, (p.partial_deriv i).eval₂ (algebra_map A) f • D (f i)),
{ intros p q hpq, refine finset.sum_subset hpq (λ i hiq hip, _),
rw [mv_polynomial.partial_deriv_of_not_mem_vars i p hip, mv_polynomial.eval₂_zero, zero_smul] },
refine mv_polynomial.induction_on p _ _ _,
{ intros r, rw [mv_polynomial.eval₂_C, D.map_algebra_map, mv_polynomial.vars_C], refl },
{ intros p q ihp ihq,
rw [this p (p.vars ∪ q.vars) (finset.subset_union_left _ _)],
rw [this q (p.vars ∪ q.vars) (finset.subset_union_right _ _)],
rw [this (p+q) (p.vars ∪ q.vars) (mv_polynomial.vars_add p q)],
{ intros p i ih,
rw [mv_polynomial.eval₂_mul, mv_polynomial.eval₂_X, D.map_mul, ih],
rw [this (p * mv_polynomial.X i) (p.vars ∪ {i}) (finset.subset.trans (mv_polynomial.vars_mul p _)
(finset.union_subset (finset.subset_union_left _ _)
(finset.subset.trans (mv_polynomial.vars_X_subset _) (finset.subset_union_right _ _))))],
rw [finset.union_comm, ← finset.insert_eq],
simp only [mv_polynomial.eval₂_mul, mv_polynomial.partial_deriv_X, mv_polynomial.eval₂_X],
rw [finset.smul_sum], simp only [smul_smul],
by_cases hip : i ∈ p.vars,
{ rw finset.insert_eq_of_mem hip, congr' 1,
rw [finset.sum_eq_single i, if_pos rfl, mv_polynomial.eval₂_one, mul_one],
{ intros j hjp hji, rw [if_neg hji.symm, mv_polynomial.eval₂_zero, mul_zero, zero_smul] },
{ intros hnip, exact absurd hip hnip } },
{ rw [finset.sum_insert hip, finset.sum_insert hip],
rw [if_pos rfl, mv_polynomial.eval₂_one, mul_one, mv_polynomial.partial_deriv_of_not_mem_vars _ _ hip, ← add_assoc], congr' 1,
rw [mv_polynomial.eval₂_zero, mul_zero, zero_smul, add_zero, finset.sum_eq_zero, add_zero],
{ intros j hjp, rw [if_neg, mv_polynomial.eval₂_zero, mul_zero, zero_smul],
{ rintro rfl, exact hip hjp } } } }
end

end derivation


#### Kenny Lau (Jul 12 2019 at 15:37):

@Kevin Buzzard here's my progress regarding derivation

#### Kevin Buzzard (Jul 12 2019 at 15:37):

I'm looking at it right now

#### Kevin Buzzard (Jul 12 2019 at 16:08):

Should there be a stricklandization? If a module has these properties, then it satisfies the universal property of the Kähler differentials?

#### Kenny Lau (Jul 12 2019 at 16:09):

I'm not sure what the properties should be

#### Kevin Buzzard (Jul 12 2019 at 16:12):

More generally, every time a new mathematical structure is made from old structures, there should be an accompanying predicate to say "I am isomorphic to this construction", because this is what mathematicians need in practice.

#### Kevin Buzzard (Jul 12 2019 at 16:18):

Patrick was just talking about the following construction. Say you have an abelian group, and a filter on this group which you should think of as the filter of neighbourhoods of zero for a topology making this group into a topological group. This filter must then satisfy a couple of axioms (zero must be in all the elements, subtraction must be continuous at 0) and then you can define a topology on the abelian group by shifting the filter to every point using the group law and then defining the topology from the neighbourhood filters of every point using some standard trick in mathlib. This construction is all well and good, but the problem is what happens if you have a group which already has a topology and a filter of neighbourhoods of zero? The new topology you can make will probably not be defeq to the one you have. So you need a predicate "I am isomorphic to this thing you just made".

We have a technical problem in the perfectoid project because we defined a super-general valuation taking values in with_zero Gamma for Gamma a linearly ordered comm group. That with_zero Gamma is a construction. Now Rob's norm on the p-adic numbers takes values in the reals, and he proves that the values are always non-negative, so we easily get a norm taking values in the non-negative reals. Guess what. That's not equal to with_zero Gamma . So given that construction of with_zero Gamma we should have defined a predicate on totally ordered comm monoids with zero saying "I am isomorphic to with_zero G for some group G and we should have developed all of the theory for these monoids instead.

There is a general philosophy here, the extent of which I am only just understanding. But it seems to me that it applies to every time you make a new construction from an old one, e.g. a module of differentials from a morphism of rings, and you will find your object easier to use if you make this predicate now and then don't prove things about the construction but about objects satisfying the predicate.

#### Mario Carneiro (Jul 12 2019 at 16:21):

I also want to point out that this approach alleviates many of the requirements for transfer

#### Kevin Buzzard (Jul 12 2019 at 16:21):

Oh! I hadn't really internalised that part of it.

#### Andrew Ashworth (Jul 12 2019 at 16:30):

Yup. This is the problem that type classes are supposed to solve in the first place... which is why we have theories of distribs.

#### Andrew Ashworth (Jul 12 2019 at 16:31):

A type class is a universal property and you pick and choose only the ones you need.

#### Andrew Ashworth (Jul 12 2019 at 16:35):

At least, that's how I think of it. Opinionated programmers love saying things like "composition over inheritance" and such.

#### Kevin Buzzard (Jul 12 2019 at 16:35):

So if $A$ is an $R$-algebra and $M$ is an $A$-module and $d:A\to M$ is an $R$-derivation then we need to write down a list of necessary and sufficient conditions to ensure $M\cong\Omega^1_{A/R}$. We should firstly demand that the range of $d$ spans $M$. And then...hmm. I see your point.

#### Mario Carneiro (Jul 12 2019 at 16:37):

You can also see some similarities in category theory, where products are defined in this universal way but used as a binary operator by abuse of notation

#### Kevin Buzzard (Jul 12 2019 at 16:38):

The only way I think of how to do this is via some presentation of A as an R-algebra.

#### Kevin Buzzard (Jul 12 2019 at 16:41):

You write A as a quotient of a polynomial ring over R (e.g. the quotient of the polynomial ring over R generated by the set A) and then make sure that the formal derivative of everything in the kernel is zero.

#### Kevin Buzzard (Jul 12 2019 at 16:41):

This might be uncheckable in practice I guess.

why?

#### Andrew Ashworth (Jul 12 2019 at 16:44):

PS. In general the verb "to stricklandize" means "extract interface" in programming circles, if you want to waste an evening reading about the problem in computer languages...

#### Kevin Buzzard (Jul 12 2019 at 16:44):

Maybe it doesn't matter whether it's useful or not. If someone finds themself in a position where they have a maths proof that some module is isomorphic to the module of differentials then maybe they can tell us a better predicate

#### Johan Commelin (Jul 12 2019 at 16:45):

The problem is that by that time we won't have developed the API in terms of that predicate... and we'll have to port the entire interface.

#### Johan Commelin (Jul 12 2019 at 16:46):

Isn't there also the I^2/I description, where I is the ideal of the diagonal?

#### Mario Carneiro (Jul 12 2019 at 16:46):

The predicates are proofs, so you can exchange one for a provably equivalent one without breaking anything

#### Johan Commelin (Jul 12 2019 at 16:46):

So that already gives two useful def's

#### Mario Carneiro (Jul 12 2019 at 16:47):

As a first cut at this predicate making you can always use X ~= my_construction where ~= is isomorphism of the appropriate kind

#### Mario Carneiro (Jul 12 2019 at 16:48):

You can then try replacing this with a more concrete conjunction of properties, and as long as you are able to prove it's equivalent you can install the new definition without breaking anything

#### Kevin Buzzard (Jul 12 2019 at 17:25):

I haven't got the definition right yet. We need to check that everything in the kernel of the derivation is zero for the right reasons

#### Kevin Buzzard (Jul 13 2019 at 00:57):

How about this: If $A$ is an $R$-algebra then say that a pair $(M,d)$ consisting of an $A$-module $M$ and an $R$-linear derivation $A\to M$ "satisfies the Strickland predicate for $\Omega^1_{R/A}$" if the induced $A$-module map $A\otimes_R A \to M$ sending $a\otimes b$ to $a\cdot d(b)$ is surjective, and secondly, every element of the kernel of this map is in the image of a map to $A\otimes_R A$ from a certain set $J$. The set $J$ is an ideal in the polynomial ring $R[A]$ consisting of multivariate polynomials with coefficients in $R$ and variables in $A$, and the ideal is the kernel of the map from $R[A]$ to $A$ sending each variable to the corresponding element. The map from $J$ to $A\otimes_R A$ is the following. Take an element of $j$, considered as a finite $R$-linear sum of monomials. Now take "formal $D$" of this element, ending up with a finite R-linear sum of things of of the form $\prod_a x_a^{n_a} D(x_k)$ where the product is over a finite subset of $A$, the $n_a$ are non-negative integers, $D(x_k)$ is a formal differential (there's one for each $k\in A$) and the term hence depends on the finite subset and the choice of $k\in A$. The map from $J$ to $A\otimes_R A$ is defined by sending $\prod_a x_a^{n_a} D(x_k)$ to $(\prod_a a^{n_a})\otimes x_k$ and extending $R$-linearly. So can you prove that two pairs $(d,M)$ both satisfying this predicate for $R/A$ are uniquely isomorphic (i.e prove the universal property from the predicate), and then can you prove that your construction satisfies that predicate?

@Kenny Lau

#### Kevin Buzzard (Jul 13 2019 at 01:13):

This is my attempt to translate the standard exact sequence $J/J^2\to\Omega^1_{S/R}\otimes_S A\to \Omega^1_{A/R}\to 0$ into a predicate, where $S$ is the polynomial ring over $R$ with variables in $A$ (or more generally a polynomial ring over $R$ with coefficients corresponding to any subset of $A$ generating it as an $R$-algebra, so $S$ is a flat $R$-module and the canonical map $S\to A$ is surjective). Then I think $\Omega^1_{S/R}$ must just be the direct sum over $a\in A$ of $SD(x_a)$. And $J$ is the kernel of $S\to R$.

#### Johan Commelin (Jul 13 2019 at 05:16):

I guess such a predicate would work (in the sense that it is correct), but it looks quite complicated. We'll probably have to see in practice whether it's actually usable.

#### Johan Commelin (Jul 13 2019 at 05:16):

@Kenny Lau Is your next step the sheaf $\Omega^1$?

#### Kevin Buzzard (Jul 13 2019 at 09:54):

The point is that if you don't do it like this then you'll have trouble further down the line when you have a localisation of the one forms instead of the one forms of the localisation and you can't rewrite

#### Kevin Buzzard (Jul 13 2019 at 09:56):

You won't be able to glue one forms and thus define the one forms on a general scheme unless you do this now

Or am I wrong?

#### Johan Commelin (Jul 13 2019 at 09:58):

Right... I completely agree that such a predicate is what we need. I would hope that we somehow get better in managing them. Maybe those predicates should be turned into structures is_Kaehler_differentials : Prop or something like that...

#### Kevin Buzzard (Jul 13 2019 at 13:49):

is_the_same_as_Kaehler_differentials

#### Jesse Michael Han (Jul 14 2019 at 22:03):

PS. In general the verb "to stricklandize" means "extract interface" in programming circles, if you want to waste an evening reading about the problem in computer languages...

did kevin invent this word? what does it mean exactly? searching for it on google only brings me back to this chat...

#### Kenny Lau (Jul 15 2019 at 04:04):

@Jesse Michael Han it's the philosophy of classifying constructions concretely rather than using universal properties

#### Kevin Buzzard (Jul 15 2019 at 07:08):

I ran into an issue with the Schemes project where I had got Chris Hughes to prove a result about localisations $R[1/S]$, and I then realised I needed it for rings which were isomorphic to the localisations, and I couldn't rw h where h was equiv A B. I checked that all the diagrams that I needed to commute, commuted, and the code was awful. Then Neil Strickland came up with a predicate P R S A : Prop which was a list of criteria which were necessary and sufficient for the $R$-algebra $A$ to be isomorphic to $R[1/S]$. Ramon Mir was then faced with the challenge of reproving Chris' result about $R[1/S]$ in the "more general" case of rings $A$ satisfying this predicate -- but the miracle was that Chris' proof only used facts about $R[1/S]$ which were trivial consequences of the predicate (the predicate was of the form "this and this and this and this" and Chris used pretty much all of the "this"'s in his proof). There is hence some sort of underlying principle, which I think some of the computer scientists know about already, at least in some form, but I've still not really seen a precise formulation of what I need.

Here's an example of a question I'm still not clear about. Say I formulate a statement about all $R$-algebras satisfying Strickland's original predicate. Say now someone proves this statement for $R[1/S]$ (the concrete construction of the localisation). Can I deduce that statement is true in general? I think I can, but I don't know the details of the argument. The Cauchy/Dedekind question I'm asking is basically the same principle -- "I am a complete archimedean ordered field" is the "Stricklandization" of both the Cauchy reals and the Dedekind reals.

#### Koundinya Vajjha (Jul 15 2019 at 13:06):

How did you avoid having to transport any properties across any equivalence?

#### Koundinya Vajjha (Jul 15 2019 at 13:06):

I'm trying to understand what happened there: does "Stricklandization" roughly mean "coming up with isomorphism invariant properties of a Type"?

#### Chris Hughes (Jul 15 2019 at 13:07):

It means coming up with an easy to use set of criteria that imply isomorphism with a certain type, and proving things about types that meet those criteria instead.

#### Patrick Massot (Jul 15 2019 at 13:07):

Everybody, please, please ignore Kevin when he uses this word. It's an insult to generations of people who worked on formalized maths before (or even traditional maths really).

#### Patrick Massot (Jul 15 2019 at 13:08):

Kevin suddenly understood something when Neil used it, and Kevin associated Neil's name to it ever since.

#### Patrick Massot (Jul 15 2019 at 13:08):

But I'm sure Neil himself is uncomfortable with this crazyness.

#### Patrick Massot (Jul 15 2019 at 13:09):

I told Kevin countless time to stop doing that, but it won't help if other people start doing it.

#### Jesse Michael Han (Jul 15 2019 at 13:35):

oh, i see, so one sort of factors out general lemmas from their proof and prays that along the way they nail down the isomorphism class they want

#### Kevin Buzzard (Jul 15 2019 at 14:17):

I don't know a better word for it :-(

#### Kevin Buzzard (Jul 15 2019 at 14:46):

How did you avoid having to transport any properties across any equivalence?

The localisation $R[1/S]$ of a commutative ring $R$ at a submonoid $S$ can be explicitly constructed as pairs $(r,s)\in R \times S$ (thought of as $r/s$) modulo some appropriate equivalence relation. However what mathematicians do in practice is that they say "it's the thing satisfying this universal property". The universal property characterises the localisation up to unique isomorphism, and for a mathematician that is enough. When proving theorems about localisations, I used to prove them about the explicit construction. Then I ran into rewrite issues, when I had rings which were isomorphic to, but not equal to, localisations.

One fix for this would involve proving results not for $R[1/S]$ but for all rings satisfying the universal property. This is also hard to do in Lean because it involves quantifying over universes, at least if you want to be maximally universe polymorphic, which seems to be the fashion here (don't get me started).

Because introducing other universes can also cause problems, and rewrites won't work for isomorphisms, we need another method. The method is to find a predicate which is provably equivalent to "I am isomorphic to $R[1/S]$" and doesn't mention any universes and is convenient to use. There is an art to this. Strickland found what seems to be exactly the right predicate for localisations.

The abstract way of thinking about it is like this. We want to rewrite along isomorphisms, and we can't. Say T is the structure we're thinking about, and we have the notion of a T-isomorphism. We have some specific term t : T, some kind of universal object, which we want to prove things about . The problem is that we want to apply these theorems to other terms u : T which are T-isomorphic to t but not (provably) equal to t. The trick is not to ever prove anything about t, but only to prove things about terms isomorphic to t.

The missing piece of the puzzle is how to get from a proof of something which unfortunately does involve t (e.g. the proof that t has some property), to the more general proof that anything isomorphic to t satisfies the same property. This is not true in general, because the property could be "I am equal to t". But for properties mathematicians are interested in, it should be true.

However this is where the hornet's nest seems to lie, at least as far as I can see. This is why I have been asking questions about the Cauchy and Dedekind reals. All mathematicians know that it doesn't matter which one we choose. And yet in mathlib they chose Cauchy, and then they did prove a bunch of stuff about the Cauchy reals, rather than proving analogous results about an arbitrary complete archimedean ordered field (that's the canonical Stricklandization for the real numbers, because any complete archimedean ordered field is uniquely isomorphic to the Cauchy reals (and to the Dedekind reals)).

So far I have convinced myself that the following powerful principle stands a chance of being true. If P u is the predicate telling us if some term u : T is T-isomorphic to t, and we have a proposition Q u about all terms u of type T which satisfy P, and we have a proof of Q t, then we should be able to formally deduce that Q u is provable, even though it might be a pain trying to actually construct the proof. The key thing here is that we don't have to check that the proof can be reformulated so that it only talks about P and not about t, we only have to check that the statement only talks about P and not t. I am hoping that there is then some general result which says the proof can be translated into one which only talks about P and not t.

What is left is checking that the statements only talk about P. This is where the Bochner integral challenge comes in. The Bochner integral is some new function defined in mathlib which mentions the real numbers, and hence the Cauchy real numbers. I would be interested in seeing a Dedekind real version of this integral, or perhaps a version which applies to all complete ordered archimedean fields. I am wondering if there is a difference between what can be said in theory and what can be done in Lean in practice.

#### Kevin Buzzard (Jul 15 2019 at 14:46):

@Koundinya Vajjha

#### Jesse Michael Han (Jul 15 2019 at 15:18):

So far I have convinced myself that the following powerful principle stands a chance of being true. If P u is the predicate telling us if some term u : T is T-isomorphic to t, and we have a proposition Q u about all terms u of type T which satisfy P, and we have a proof of Q t, then we should be able to formally deduce that Q u is provable, even though it might be a pain trying to actually construct the proof.

do you mean something like this?

example
(T : Type*)
(t : T)
(u : T)
(eqv : T → T → Prop)
(H_equiv : is_equiv _ eqv)
(P : T → Prop)
(HP : ∀ u, P u → eqv t u)
(Q : T → Prop)
(HQ : ∀ u (Hu : P u), Q u)
(P_respect_iso : ∀ u (H : P u) t, eqv u t → P t)
(Q_respect_iso : ∀ u (H : Q u) t, eqv u t → Q t)
(Ht : Q t)
(Hu : P u)
: Q u :=
by simp*


#### Kevin Buzzard (Jul 15 2019 at 15:19):

I don't know HQ. I only know Q t

#### Kevin Buzzard (Jul 15 2019 at 15:20):

I don't think I know Q_respect_iso either.

#### Jesse Michael Han (Jul 15 2019 at 15:21):

oh, so you meant thatQ is a predicate on the subtype of P?

#### Kevin Buzzard (Jul 15 2019 at 15:21):

You can figure it out for yourself. In mathlib there's a proof that a non-empty bounded-above set of Cauchy reals has a supremum. I want to prove that for the Dedekind reals, say.

#### Kevin Buzzard (Jul 15 2019 at 15:22):

Yes, Q could be thought of as a predicate on the subtype of T corresponding to P.

#### Kevin Buzzard (Jul 15 2019 at 15:23):

So here are the two steps involved in proving that a non-empty bounded-above set of Dedekind reals has a supremum. Firstly, beef up the statement that a non-empty bounded-above set of Cauchy reals has a supremum to the statement that a non-empty bounded-above subset of any complete ordered archimedean field has a supremum, and then secondly show that if you have a proof of this for the Cauchy reals then you can deduce one for the Dedekind reals.

#### Jesse Michael Han (Jul 15 2019 at 15:52):

first-order transfer fails here since adjoining a predicate symbol easily spoils the completeness of first-order theories

but in this case you could just show that some second-order properties transfer across isomorphisms of ordered fields, like the supremum of a set or the property of being bounded

maybe the idiomatic way to do it would be to have a complete ordered archimedean field typeclass and then prove as many higher-order properties you want, and then specialize

#### Jesse Michael Han (Jul 15 2019 at 15:53):

(i'm sure this has all been said before)

#### Kevin Buzzard (Jul 15 2019 at 15:55):

maybe the idiomatic way to do it would be to have a complete ordered archimedean field typeclass and then prove as many higher-order properties you want, and then specialize

Right! But we don't! Mathematicians expect to be able to move between the Cauchy reals and the Dedekind reals immediately because they are "the same". On the other hand we are making lots and lots of constructions using only the Cauchy reals. This is not an issue for mathematicians though, because they know this general principle that one can rewrite anything sensible along a map saying that two things are the same, and it is perhaps not in anyone's interest to point out the subtleties here.

#### Nicolò Cavalleri (Jul 24 2020 at 13:42):

Is there any reason why derivations were formalized with this algebra field instead of extending linear maps (it seems the two are equivalent)?

#### Alex J. Best (Jul 24 2020 at 14:43):

Well that definition only allows derivations from A to itself? Whereas quite often you want derivations from A to any A-module M.

#### Kevin Buzzard (Jul 24 2020 at 15:33):

We could make do with the one to the universal module ;-)

#### Nicolò Cavalleri (Jul 31 2020 at 16:36):

Sorry if this is a stupid question but I've never really seen derivations in abstract algebra yet... is this not possible / is this a bad idea?

variables (R : Type*) (A : Type*) [comm_ring R] [ring A] [algebra R A]
variables (M : Type*) [add_comm_group M] [module A M]

instance transitive_scalar (R : Type*) (A : Type*) (M : Type*)
[comm_semiring R] [semiring A] [algebra R A]
[add_comm_monoid M] [semimodule A M] : has_scalar R M :=
{ smul := λ r m, (r • (1 : A)) • m, }

instance transitive_module (R : Type*) (A : Type*) (M : Type*)
[comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [semimodule A M] :
semimodule R M :=
{
smul_zero := sorry,
one_smul := sorry,
mul_smul := sorry,
zero_smul := sorry,
}

structure derivation extends A →ₗ[R] M :=
(Leibniz : ∀ x y, to_fun (x * y) = x • to_fun y + y • to_fun x)


#### Kenny Lau (Jul 31 2020 at 16:48):

oh right, you remind me to generalize is_algebra_tower

#### Kenny Lau (Jul 31 2020 at 16:49):

don't make transitive_module an instance

#### Kenny Lau (Jul 31 2020 at 16:49):

(make it a def)

#### Kenny Lau (Jul 31 2020 at 16:49):

are you asking about the Lean code or the maths content?

#### Nicolò Cavalleri (Jul 31 2020 at 17:14):

The maths content

#### Kevin Buzzard (Jul 31 2020 at 17:16):

Looks good at first glance

#### Nicolò Cavalleri (Jul 31 2020 at 17:17):

I need derivations for geometry and I need to write just a stab. I'd write derivations like in this last example because I am more comfortable with this definition, but the truth is that I really don't know anything of graduate level algebra (this will change next year but I need to do this now) and I have no idea if the definition you gave one year ago has advantages over mine or it is just a matter of preference

#### Nicolò Cavalleri (Jul 31 2020 at 17:18):

Sorry you is referring to Kenny

#### Kevin Buzzard (Jul 31 2020 at 17:22):

When I was just beginning in this area I used to ask this sort of question a lot ("here are three ways to do schemes, which is the best way?") and the answer I would get a lot was "nobody did schemes before in Lean, so why not just choose a way and do it, and see what happens?". Computer scientists don't have all the answers here. Even if there was a wonderful theory of derivations in Coq or Isabelle/HOL this doesn't mean that they way they set it up is the way it should be done in Lean.

#### Kevin Buzzard (Jul 31 2020 at 17:23):

Mathematicians all agree on the specification, but you are asking about the implementation. Probably all implementations give the same theorems but the question really is how easy is it to get to them. What do you want from derivations?

#### Nicolò Cavalleri (Jul 31 2020 at 17:30):

Well I just need to use them to create Lie brackets so I just need very basic stuff such that the commutator of derivations is a derivation, but my point is that I want them to be similar to how they will be implemented in mathlib later on so that I won't have to change my code afterwards. I also plan to PR my stab on derivations as I plan to PR Lie brackets so that's why I want to be sure my implementation is acceptable

#### Nicolò Cavalleri (Jul 31 2020 at 17:32):

If people are sure that derivations in the end will be implemented as Kenny did it in this topic one year ago, I will do it like that now

#### Nicolò Cavalleri (Jul 31 2020 at 17:33):

Kenny Lau said:

(make it a def)

But in order to write linear maps I need an instance! Should I write a def and a coercion?

#### Kenny Lau (Jul 31 2020 at 17:37):

@Nicolò Cavalleri to write linear maps just have an extra assumption semimodule R M

#### Kenny Lau (Jul 31 2020 at 17:37):

as well as transitive_scalar R A M

#### Kevin Buzzard (Jul 31 2020 at 17:38):

The idea is not to tell the typeclass system to solve problems, but tell it the answers yourself. Say "M is an R-module and an A-module, and the module structures are compatible", rather than telling Lean only some of the story and making it figure out the rest by itself.

#### Nicolò Cavalleri (Jul 31 2020 at 17:46):

Kenny Lau said:

as well as transitive_scalar R A M

You mean to make this a def as well?

#### Nicolò Cavalleri (Jul 31 2020 at 17:46):

But why? Why not an instance?

#### Nicolò Cavalleri (Jul 31 2020 at 17:47):

Kevin Buzzard said:

The idea is not to tell the typeclass system to solve problems, but tell it the answers yourself. Say "M is an R-module and an A-module, and the module structures are compatible", rather than telling Lean only some of the story and making it figure out the rest by itself.

I mean why this is the idea?

#### Reid Barton (Jul 31 2020 at 17:47):

It can't be an instance because it involves the variable A which doesn't appear in the result type.

#### Reid Barton (Jul 31 2020 at 17:47):

It means any time Lean wants to figure out why something is a module over some ring it will try to invent some intermediate algebra over the ring over which the thing is also a module.

#### Nicolò Cavalleri (Jul 31 2020 at 17:50):

Oh right it makes sense! Then I guess this is a reason to do it the way Kenny was doing it? Otherwise one always needs to go back to pick up this definition

#### Nicolò Cavalleri (Jul 31 2020 at 17:51):

I mean now the other definition looks more natural to me

#### Adam Topaz (Jul 31 2020 at 17:58):

Has anyone thought about introducing things like this?

variables (R : Type*) [comm_semiring R]
variables (A : Type*) [semiring A] [algebra R A]
variables (M : Type*) [add_comm_monoid M]

class has_compat_semimodule [semimodule A M] extends semimodule R M :=
(compat {r : R} {m : M} : r • m = ((algebra_map R A) r) • m)


#### Kenny Lau (Jul 31 2020 at 18:02):

Nicolò Cavalleri said:

Kenny Lau said:

as well as transitive_scalar R A M

You mean to make this a def as well?

no, I mean whenever you want to write linear maps, have extra assumptions semimoduel R M and transitive_scalar R A M

#### Kevin Buzzard (Jul 31 2020 at 18:24):

@Adam Topaz Kenny has made these classes for algebras but not modules

#### Kenny Lau (Jul 31 2020 at 18:29):

and my work can definitely be gerenalised thereto

#### Adam Topaz (Jul 31 2020 at 18:29):

Is this in mathlib?

#### Kenny Lau (Jul 31 2020 at 18:31):

docs#is_algebra_tower

Nice! Thanks.

#### Nicolò Cavalleri (Jul 31 2020 at 18:35):

In any case when did you write derivations that way instead of extending linear maps so to avoid dangerous instance problems? I mean is this thing of being forced to write a definition instead of an instance a disadvantage or is it something normal I should not care about?

#### Kevin Buzzard (Jul 31 2020 at 18:37):

Lean's typeclass inference system is pretty well understood by some people now, and some instances are dangerous. This has nothing to do with mathematics, we just have to do what we're told

#### Adam Topaz (Jul 31 2020 at 18:39):

I guess you can do this:

import ring_theory.algebra

variables (R : Type*) [comm_semiring R]
variables (A : Type*) [semiring A] [algebra R A]
variables (M : Type*) [add_comm_monoid M]

class has_compat_semimodule [semimodule A M] extends semimodule R M :=
(compat {r : R} {m : M} : r • m = ((algebra_map R A) r) • m)

structure derivation [semimodule A M] [has_compat_semimodule R A M]  extends A →ₗ[R] M :=
(leibniz {a b : A} : to_fun (a * b) = a • to_fun b + b • to_fun a)


#### Adam Topaz (Jul 31 2020 at 18:39):

With no dangerous instances.

#### Adam Topaz (Jul 31 2020 at 18:40):

At least I think it's not dangerous :) But like Kevin said, you have to ask someone who understands the typeclass inference system.

#### Nicolò Cavalleri (Jul 31 2020 at 18:41):

Well I guess that if lint does not say it is dangerous then it should be fine!

#### Adam Topaz (Jul 31 2020 at 18:42):

It was dangerous :(

#### Nicolò Cavalleri (Jul 31 2020 at 18:43):

Yes I actually see why

#### Adam Topaz (Jul 31 2020 at 18:43):

The linter is happy with this though:

import ring_theory.algebra

variables (R : Type*) [comm_semiring R]
variables (A : Type*) [semiring A] [algebra R A]
variables (M : Type*) [add_comm_monoid M]

class has_compat_semimodule [semimodule A M] [semimodule R M] :=
(compat {r : R} {m : M} : r • m = ((algebra_map R A) r) • m)

structure derivation [semimodule A M] [semimodule R M] [has_compat_semimodule R A M]  extends A →ₗ[R] M :=
(leibniz {a b : A} : to_fun (a * b) = a • to_fun b + b • to_fun a)


#### Adam Topaz (Jul 31 2020 at 18:43):

Which is closer to Kenny's is_algebra_tower.

#### Nicolò Cavalleri (Jul 31 2020 at 18:48):

Yeah even if this way one has to have three instances whereas with the definition Kenny had these instances where not required... Is this a disadvantage or will in practice these instances always be there? Who knows I'll just give it a try I guess if no one thinks these problem imply Kenny's definition was better

#### Nicolò Cavalleri (Jul 31 2020 at 18:51):

I guess it could also be a good idea to ask that derivation extends has_compat_semimodule instead that requiring it as an instance I guess

#### Nicolò Cavalleri (Jul 31 2020 at 18:51):

Looks no dangerous coercions would happen

#### Kenny Lau (Jul 31 2020 at 18:51):

algebra tower has been working perfectly so far for me

#### Nicolò Cavalleri (Jul 31 2020 at 18:54):

Kenny Lau said:

algebra tower has been working perfectly so far for me

So you'd also go for this last suggested implementation? I mean you have any further suggestion that could make things compatible with your future generalization of algebra towers?

#### Kenny Lau (Jul 31 2020 at 18:56):

well what is in my head is a complete generalization to only has_scalar when defining compatibility

#### Kenny Lau (Jul 31 2020 at 18:57):

but in terms of how you use it, yes that's how I use it

#### Kenny Lau (Jul 31 2020 at 18:57):

I mean you can look at how I use algebra tower in mathlib

#### Kenny Lau (Jul 31 2020 at 18:58):

(click the {...} to expand the assumptions)

#### Oliver Nash (Jul 31 2020 at 22:23):

Also relevant here is the following https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/extends.20has_scalar/near/201789261

#### Oliver Nash (Jul 31 2020 at 22:25):

So for example those definitions above that end up extending A →ₗ[R] M are fine because there are three carrier types on the class being extended but those that try to extend has_scalar are not.

#### Oliver Nash (Jul 31 2020 at 22:26):

I believe this limitation will go away in the promised land of Lean 4.

#### Mario Carneiro (Jul 31 2020 at 23:48):

derivation could indeed extend has_compat_semimodule, although that would mean that in proofs you have to get the compat theorem out of a derivation by d.compat rather than inferring it from the context. But that doesn't sound so bad

#### Nicolò Cavalleri (Aug 01 2020 at 11:49):

Alex J. Best said:

Well that definition only allows derivations from A to itself? Whereas quite often you want derivations from A to any A-module M.

Sorry another question about the maths content regarding this. Sincerely, not knowing algebra, I have no idea why it is interesting to consider derivations to a generic module A (when Alex says "often" I cannot really think of even one example), but I also realize just now that this theory can only be developed for commutative algebra, whereas the theory I am interested in is that of non-commutative algebra (for example in quantum mechanics one needs derivations on non commutative algebras), and it is the one of wikipedia: https://en.wikipedia.org/wiki/Derivation_(differential_algebra). As far as people know, is there an even more general theory that deals with both cases or should I just rechange my code (for like the 10th time haha) and just write the theory I need?

#### Nicolò Cavalleri (Aug 01 2020 at 11:51):

Actually I read that there is a theory for bimodules... Do we even have bimodules in mathlib?

#### Nicolò Cavalleri (Aug 01 2020 at 11:54):

I do not see them... Unless someone has some enlightning suggestion or wants to implement bimodules in little time I'll just write the theory for algebras and write TODO: generalize this to bimodules`

#### Julian Külshammer (Aug 01 2020 at 12:05):

This has been discussed recently, see e.g.: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Ideals.20over.20algebras/near/205492670

#### Adam Topaz (Aug 02 2020 at 00:39):

If you really want to go down the rabbit hole, look up Quillen's definition of a derivation :grinning_face_with_smiling_eyes:

#### Nicolò Cavalleri (Aug 02 2020 at 15:54):

In homotopical algebra? I don't really know his books

#### Adam Topaz (Aug 02 2020 at 15:56):

It's in his paper called "On the (co-)homology of commutative rings".

Last updated: May 18 2021 at 07:19 UTC