Zulip Chat Archive

Stream: maths

Topic: derivation


view this post on Zulip 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 _ • _) = _,
--     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

view this post on Zulip 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,
    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

view this post on Zulip 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) _,
  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

view this post on Zulip Kenny Lau (Jul 12 2019 at 15:37):

@Kevin Buzzard here's my progress regarding derivation

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 15:37):

I'm looking at it right now

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jul 12 2019 at 16:09):

I'm not sure what the properties should be

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 12 2019 at 16:21):

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

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 16:21):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 16:35):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 16:41):

This might be uncheckable in practice I guess.

view this post on Zulip Mario Carneiro (Jul 12 2019 at 16:41):

why?

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 12 2019 at 16:46):

So that already gives two useful def's

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 13 2019 at 00:57):

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

view this post on Zulip Kevin Buzzard (Jul 13 2019 at 01:06):

@Kenny Lau

view this post on Zulip Kevin Buzzard (Jul 13 2019 at 01:13):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 13 2019 at 05:16):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 13 2019 at 09:57):

Or am I wrong?

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Jul 13 2019 at 13:49):

is_the_same_as_Kaehler_differentials

view this post on Zulip 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...

view this post on Zulip Kenny Lau (Jul 15 2019 at 04:04):

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

view this post on Zulip 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]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 RR-algebra AA to be isomorphic to R[1/S]R[1/S]. Ramon Mir was then faced with the challenge of reproving Chris' result about R[1/S]R[1/S] in the "more general" case of rings AA satisfying this predicate -- but the miracle was that Chris' proof only used facts about R[1/S]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 RR-algebras satisfying Strickland's original predicate. Say now someone proves this statement for R[1/S]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.

view this post on Zulip Koundinya Vajjha (Jul 15 2019 at 13:06):

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

view this post on Zulip 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"?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jul 15 2019 at 13:08):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 15 2019 at 14:17):

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

view this post on Zulip 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]R[1/S] of a commutative ring RR at a submonoid SS can be explicitly constructed as pairs (r,s)R×S(r,s)\in R \times S (thought of as r/sr/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]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]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.

view this post on Zulip Kevin Buzzard (Jul 15 2019 at 14:46):

@Koundinya Vajjha

view this post on Zulip 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*

view this post on Zulip Kevin Buzzard (Jul 15 2019 at 15:19):

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

view this post on Zulip Kevin Buzzard (Jul 15 2019 at 15:20):

I don't think I know Q_respect_iso either.

view this post on Zulip Jesse Michael Han (Jul 15 2019 at 15:21):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Jesse Michael Han (Jul 15 2019 at 15:53):

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

view this post on Zulip 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.

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 15:33):

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

view this post on Zulip 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_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)

view this post on Zulip Kenny Lau (Jul 31 2020 at 16:48):

oh right, you remind me to generalize is_algebra_tower

view this post on Zulip Kenny Lau (Jul 31 2020 at 16:49):

don't make transitive_module an instance

view this post on Zulip Kenny Lau (Jul 31 2020 at 16:49):

(make it a def)

view this post on Zulip Kenny Lau (Jul 31 2020 at 16:49):

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

view this post on Zulip Nicolò Cavalleri (Jul 31 2020 at 17:14):

The maths content

view this post on Zulip Kevin Buzzard (Jul 31 2020 at 17:16):

Looks good at first glance

view this post on Zulip 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

view this post on Zulip Nicolò Cavalleri (Jul 31 2020 at 17:18):

Sorry you is referring to Kenny

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jul 31 2020 at 17:37):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 17:37):

as well as transitive_scalar R A M

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Nicolò Cavalleri (Jul 31 2020 at 17:46):

But why? Why not an instance?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Nicolò Cavalleri (Jul 31 2020 at 17:51):

I mean now the other definition looks more natural to me

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 31 2020 at 18:24):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 18:29):

and my work can definitely be gerenalised thereto

view this post on Zulip Adam Topaz (Jul 31 2020 at 18:29):

Is this in mathlib?

view this post on Zulip Kenny Lau (Jul 31 2020 at 18:31):

docs#is_algebra_tower

view this post on Zulip Adam Topaz (Jul 31 2020 at 18:31):

Nice! Thanks.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Jul 31 2020 at 18:39):

With no dangerous instances.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Adam Topaz (Jul 31 2020 at 18:42):

It was dangerous :(

view this post on Zulip Nicolò Cavalleri (Jul 31 2020 at 18:43):

Yes I actually see why

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Jul 31 2020 at 18:43):

Which is closer to Kenny's is_algebra_tower.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Nicolò Cavalleri (Jul 31 2020 at 18:51):

Looks no dangerous coercions would happen

view this post on Zulip Kenny Lau (Jul 31 2020 at 18:51):

algebra tower has been working perfectly so far for me

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 31 2020 at 18:57):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 18:57):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 18:58):

e.g. docs#is_algebra_tower.aeval_apply

view this post on Zulip Kenny Lau (Jul 31 2020 at 18:58):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Oliver Nash (Jul 31 2020 at 22:26):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Nicolò Cavalleri (Aug 02 2020 at 15:54):

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

view this post on Zulip 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