derivation

Stream: maths

[Kenny Lau]

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 _ • _) = _,
--     by rw [algebra.map_add, add_smul]; refl,
--   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)

@[to_additive add_comm₄]
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_add, D2.map_add, add_comm₄],
    λ 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),
  add := λ a1 a2, by rw [D.map_add, f.map_add],
  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 : add_comm_group («Kähler» R A) := quotient_add_group.add_comm_group _

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]

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,
    add_group.in_closure.rec_on 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]),
  add := is_add_group_hom.map_add _,
  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,
        is_add_group_hom.map_add (quotient_add_group.lift _ _ _), smul_add]; apply_instance) }

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) $
λ v a1 a2, by rw [add_monoid.smul_add, finsupp.single_add]

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 [mul_add, smul_add, 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]

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) _,
  rw [add_mul, partial_deriv_add, mul_add, add_comm₄], congr' 1,
  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 [add_mul, partial_deriv_add, mul_add, add_comm₄], congr' 1,
  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,
  { rw [hv, zero_add, add_monoid.zero_smul, finsupp.single_zero], erw add_zero,
    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 [add_monoid.add_smul, finsupp.single_add, add_comm], congr' 1,
  { 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,
  add := mv_polynomial.partial_deriv_add 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 [mv_polynomial.eval₂_add, D.map_add, 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)],
    simp only [mv_polynomial.partial_deriv_add, mv_polynomial.eval₂_add, add_smul, finset.sum_add_distrib] },
  { 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.partial_deriv_mul, mv_polynomial.eval₂_add, add_smul, finset.sum_add_distrib],
    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]

@Kevin Buzzard here's my progress regarding derivation

[Kevin Buzzard]

I'm looking at it right now

[Kevin Buzzard]

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

[Kenny Lau]

I'm not sure what the properties should be

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Andrew Ashworth]

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]

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

[Andrew Ashworth]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

This might be uncheckable in practice I guess.

[Mario Carneiro]

why?

[Andrew Ashworth]

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]

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]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

So that already gives two useful def's

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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?

[Kevin Buzzard]

@Kenny Lau

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Or am I wrong?

[Johan Commelin]

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]

is_the_same_as_Kaehler_differentials

[Jesse Michael Han]

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]

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

[Kevin Buzzard]

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]

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

[Koundinya Vajjha]

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

[Chris Hughes]

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]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Jesse Michael Han]

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]

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

[Kevin Buzzard]

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]

@Koundinya Vajjha

[Jesse Michael Han]

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]

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

[Kevin Buzzard]

I don't think I know Q_respect_iso either.

[Jesse Michael Han]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Nicolò Cavalleri]

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_add := sorry,
  smul_zero := sorry,
  one_smul := sorry,
  mul_smul := sorry,
  add_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]

oh right, you remind me to generalize is_algebra_tower

[Kenny Lau]

don't make transitive_module an instance

[Kenny Lau]

(make it a def)

[Kenny Lau]

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

[Nicolò Cavalleri]

The maths content

[Kevin Buzzard]

Looks good at first glance

[Nicolò Cavalleri]

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]

Sorry you is referring to Kenny

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[Kenny Lau]

as well as transitive_scalar R A M

[Kevin Buzzard]

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]

Kenny Lau said:

as well as transitive_scalar R A M

You mean to make this a def as well?

[Nicolò Cavalleri]

But why? Why not an instance?

[Nicolò Cavalleri]

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]

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

[Reid Barton]

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]

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]

I mean now the other definition looks more natural to me

[Adam Topaz]

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]

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]

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

[Kenny Lau]

and my work can definitely be gerenalised thereto

[Adam Topaz]

Is this in mathlib?

[Kenny Lau]

docs#is_algebra_tower

[Adam Topaz]

Nice! Thanks.

[Nicolò Cavalleri]

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]

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]

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]

With no dangerous instances.

[Adam Topaz]

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]

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

[Adam Topaz]

It was dangerous :(

[Nicolò Cavalleri]

Yes I actually see why

[Adam Topaz]

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]

Which is closer to Kenny's is_algebra_tower.

[Nicolò Cavalleri]

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]

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]

Looks no dangerous coercions would happen

[Kenny Lau]

algebra tower has been working perfectly so far for me

[Nicolò Cavalleri]

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]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

e.g. docs#is_algebra_tower.aeval_apply

[Kenny Lau]

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

[Oliver Nash]

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

[Oliver Nash]

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]

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

[Mario Carneiro]

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]

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]

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

[Nicolò Cavalleri]

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]

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]

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]

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

[Adam Topaz]

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

[Oliver Nash]

Our current definition of docs#Derivation requires a commutativity assumption because its Leibniz axiom is incorrect in the non-commutative case. The definition was a deliberate compromise pending a future refactor. Yesterday I experimented with such a refactor.

In the end I decided the refactor was too much of a distraction, especially as some of the relevant files have yet to be ported. However I did have some thoughts which I will share here in the hope that they may help somebody in the future.

[Oliver Nash]

The point is that we want a common generalisation of the following two situations:

1. Given a commutative ring A and a left A-module M, we want to consider maps D : A → M satisfying D (a * b) = a • D b + b • D a.
2. Given a not-necessarily-commutative ring A, we want to consider maps: D : A → A satisfying D (a * b) = a * D b + (D a) * b. The ordering is important because for any c : A, we want the map a ↦ c * a - a * c to be a derivation (when A is associative).

Actually everything is also linear over another set of coefficients R but this doesn't affect anything.

[Eric Rodriguez]

Could it be written in terms of the right action and have two definitional lemmas for either case?

[Oliver Nash]

@Eric Rodriguez I have a big post written off-line which I'm gradually pasting in which makes remarks along these lines ;-)

[Oliver Nash]

Informally all is clear: derivations are maps associated to an object M that is simultaneously a left and right A-module (though not necessarily a bimodule because I want to allow situation 2 above in the case when A is not associative).

The obvious formal definition based on the above would be something like:

structure Derivation  (R A M : Type _)
  [NonUnitalNonAssocSemiring A] [SMul A M] [SMul Aᵐᵒᵖ M]
  [AddCancelCommMonoid M] [CommSemiring R] [Module R A] [Module R M]
  extends A →ₗ[R] M where
  leibniz (a b : A) :
    toLinearMap (a * b) = a • toLinearMap b + MulOpposite.op b • toLinearMap a

[Oliver Nash]

I think this is a pretty good definition but it does have one awkwardness: when A is commutative the typeclass SMul Aᵐᵒᵖ M will usually not exist. The easiest solution would be to add:

instance (A M : Type _) [CommSemiring A] [AddCommMonoid M] [Module A M] : Module Aᵐᵒᵖ M :=

but I think this is probably bad because it would prevent us being able to discuss a situation where M is simultaneously a left and right A-module over a commutative ring when the actions are genuinely different (informally, modules over A ⊗ A).

I tried some other solutions (e.g., making the above a def to be locally enabled) but they all left the user at least slightly worse off than the current definition in the important case that A is commutative.

[Oliver Nash]

Thinking about this a bit more I came up with the following:

structure Derivation' (R A B C M : Type _)
  [NonAssocSemiring A] [NonAssocSemiring B] [NonAssocSemiring C] [SMul A M] [SMul B M] [SMul C M]
  [AddCancelCommMonoid M] [CommSemiring R] [Module R A] [Module R B] [Module R C] [Module R M]
  (iA : A →ₗ[R] C) (iB : B →ₗ[R] C) extends C →ₗ[R] M where -- Or even just `(iA : A → C) (iB : B → C)`
  leibniz (a : A) (b : B) :
    toLinearMap ((iA a) * (iB b)) = a • toLinearMap (iB b) + b • toLinearMap (iA a)

The idea is that when A is commutative we can take B = C = A and iA = iB to be the identity map and otherwise we can take B = Aᵐᵒᵖ, C = A, iA the identity, and iB to be MulOpposite.unop (or an R-linear version).

[Oliver Nash]

Actually the above is probably overkill and so I settled on the following candidate:

structure Derivation'' (R A B M : Type _)
  [NonAssocSemiring A] [NonAssocSemiring B] [SMul A M] [SMul B M]
  [AddCancelCommMonoid M] [CommSemiring R] [Module R A] [Module R B] [Module R M]
  (iB : B →ₗ[R] A) extends A →ₗ[R] M where
  leibniz (a : A) (b : B) :
    toLinearMap (a * iB b) = a • toLinearMap (iB b) + b • toLinearMap a

I'm not sure what would be the best definition. Since I've decided to shelve this I thought I'd dump these thoughts here.

[Oliver Nash]

Perhaps someone will have remarks / suggestions.

[Eric Wieser]

Checking my messages in some downtime: I have a mathlib3 PR with this refactor

[Oliver Nash]

Thanks for mentioning this. It looks like !3#18936 is the PR and it proposes what I called Derivation above, and thus depends on !3#10716 which we never really decided about.