Zulip Chat Archive

Stream: maths

Topic: CDGAs


view this post on Zulip Reid Barton (Jun 11 2019 at 13:19):

I thought the discussion related to definitional associativity of addition and so on might benefit from a concrete example. So, here is a mini-challenge. A commutative differential graded algebra (CDGA) over a commutative ring RR consists of
1. for each natural number nn, an RR-module AnA_n
2. for each ii and jj, an RR-bilinear multiplication map Ai×AjAi+jA_i \times A_j \to A_{i+j}
3. a unit 1A01 \in A_0
4. satisfying the obvious unitality and associativity conditions 1a=a1 \cdot a = a, a1=aa \cdot 1 = a, (ab)c=a(bc)(a \cdot b) \cdot c = a \cdot (b \cdot c) for aAia \in A_i, bAjb \in A_j, cAkc \in A_k
5. as well as the graded commutativity relation ba=(1)ijabb \cdot a = (-1)^{ij} a \cdot b for aAia \in A_i, bAjb \in A_j
6. along with an RR-linear differential d:AnAn+1d : A_n \to A_{n+1} for each nn
7. satisfying d2=0d^2 = 0
8. as well as the Leibniz rule d(ab)=dab+(1)iadbd(a\cdot b) = da \cdot b + (-1)^i a \cdot db for aAia \in A_i, bAjb \in A_j.
Note that the equations in 4, 5, 8 all involve reassociating and/or commuting i, j, k, 1 past one another.

If AA is a CDGA then its cohomology H(A)H^*(A) is a graded commutative algebra. Basically this amounts to checking that

  • if da=0da = 0 and db=0db = 0, then d(ab)=0d(a \cdot b) = 0
  • if da=0da = 0 and b=dbb = db', then aba \cdot b is dd of something (namely (1)iab(-1)^i a \cdot b' where aAia \in A_i),
  • similarly if a=daa = da' and db=0db = 0 then aba \cdot b is dd of something
    and therefore the multiplication Ai×AjAi+jA_i \times A_j \to A_{i+j} restricts/descends to the kernel of dd modulo the image of dd.

view this post on Zulip Johan Commelin (Jun 11 2019 at 13:29):

And the challenge is... I guess: Implement CDGAs and prove that the cohomology is a graded commutative algebra?

view this post on Zulip Reid Barton (Jun 11 2019 at 13:33):

Right. Or just check the last three bulleted points if it's easier.

view this post on Zulip Johan Commelin (Jun 11 2019 at 13:36):

And who are you challenging :stuck_out_tongue_wink:?

view this post on Zulip Reid Barton (Jun 11 2019 at 13:39):

Anyone who doesn't already believe that this will be a mess :upside_down:

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 13:41):

I am sufficiently naive to believe that this will not be a mess. Why am I wrong?

view this post on Zulip Reid Barton (Jun 11 2019 at 13:42):

None of the equations in 4, 5, 8 or the trivial computations that need to be done to check the bulleted points type check if you write them down directly.

view this post on Zulip Reid Barton (Jun 11 2019 at 13:42):

Well, maybe one of the unitality equations happens to type check. The issue with associativity for example is that one side is in A ((i + j) + k), while the other side is in A (i + (j + k)).

view this post on Zulip Reid Barton (Jun 11 2019 at 13:43):

The Leibniz rule involves three different types (I think, unless by chance two of them are defeq)

view this post on Zulip Reid Barton (Jun 11 2019 at 13:44):

To check da=db=0d(ab)=0da = db = 0 \implies d(a \cdot b) = 0 you need to know that "being 0" is preserved across a cast A ((i + 1) + j) \to A ((i + j) + 1)

view this post on Zulip Reid Barton (Jun 11 2019 at 13:45):

If defeq coincidences make it too easy, then change the degree of dd to -1.

view this post on Zulip Reid Barton (Jun 11 2019 at 13:48):

By the way, considering the signs in the Leibniz rule, it would really be more consistent to write dd as AnA1+nA_n \to A_{1+n}, but for some reason we don't do that.

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

By the way, considering the signs in the Leibniz rule, it would really be more consistent to write dd as AnA1+nA_n \to A_{1+n}, but for some reason we don't do that.

That's because 1+n1+n and n+1n+1 are the same.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 14:10):

(and n+1n+1 is the canonical form. )

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 14:20):

def id' (A :   Type) (i j k : ) : A (i + (j + k))  A ((i + j) + k) :=
λ x, eq.mpr (by rw add_assoc) x

I don't really know what happens next. Does it get really horrible?

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 14:22):

Aah, and now the game is to prove that id' 0 = 0

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 14:24):

def id' (A :   Type) [ n, has_zero (A n)]
(i j k : ) : A (i + (j + k))  A ((i + j) + k) :=
λ x, eq.mpr (by rw add_assoc) x

example (A :   Type) [ n, has_zero (A n)] (i j k : ) :
id' A i j k 0 = 0 :=
begin
  sorry
end

view this post on Zulip Johan Commelin (Jun 11 2019 at 14:36):

Kevin, this is certainly not what formalisation should impose on us.

view this post on Zulip Johan Commelin (Jun 11 2019 at 14:37):

The system needs fixing, not just another work around

view this post on Zulip Neil Strickland (Jun 11 2019 at 14:39):

I think that this is the main thing that we need:

variables (A :   Type*) [ n, add_comm_group (A n)]

theorem mp_hom {n m : } (h : n = m) :
  is_add_group_hom ((congr_arg A h).mp : A n  A m) :=
begin
  rcases h,
  change is_add_group_hom id,
  exact {map_add := λ a b, rfl}
end

view this post on Zulip Floris van Doorn (Jun 12 2019 at 02:48):

I have worked with a sequence of types before, in the Lean 2 HoTT library (e.g. in the folder https://github.com/cmu-phil/Spectral/tree/master/colimit see sequence and seq_colimor https://github.com/cmu-phil/Spectral/blob/master/algebra/graded.hlean)
Here are some thoughts:

  • This is definitely doable over the ordinary natural numbers if you know what you are doing. It will be tricky if you're not used to dependent types.
  • Definitional associativity of addition will still be very useful.
  • For point 8, you also want (n+m)+1=(n+1)+m=n+(m+1) definitionally, which we probably won't get with any version of (d)nat. So we still have to reason with cast/heq/...
  • If we replace the indexing type by int instead of nat we have an additional problem that we want (n - 1) + 1 to be definitionally equal to n to define cohomology (there is no d which has AnA_n as codomain, only A(n1)+1A_{(n-1)+1}). See https://github.com/cmu-phil/Spectral/blob/master/algebra/graded.hlean#L17-L34 for some design considerations when I did graded morphisms and homology. For nat this will probably not be a problem, if we only define cohomology for n+1, since (n+1)-1+1=n+1 definitionally.
  • When doing this over nat, I would definitely use heq everywhere for every equation. heqs aren't that bad to work with, IMO (the pathovers I worked with in HoTT are worse). I would probably write point 8 as d(ab)+(1)i+1adb==dabd(a\cdot b)+(-1)^{i+1}a\cdot db==da\cdot b (otherwise you have to insert a cast on one side of the addition)

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 08:29):

theorem mp_hom {n m : } (h : n = m) :
  is_add_group_hom ((congr_arg A h).mp : A n  A m) :=
begin
  subst h,
  exact is_add_group_hom.id
end

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 08:30):

import algebra.group
import algebra.module

universe u

structure cdga (R : Type u) [comm_ring R] :=
(A :   Type u) -- universe monomorphism FTW
[hA :  n, add_comm_group (A n)]
[hRA :  n, module R (A n)]
(a2 :  i j , (A i)  (A j)  (A (i + j)))
(h21 :  i j,  r : R,  a : A i,  b : A j, a2 (r  a) b = r  (a2 a b))
(h22 :  i j,  r : R,  a : A i,  b : A j, a2 a (r  b) = r  (a2 a b))
(h23 :  i j,  r : R,  a₁ a₂ : A i,  b : A j, a2 (a₁ + a₂) b = a2 a₁ b + a2 a₂ b)
(h24 :  i j,  r : R,  a : A i,  b₁ b₂ : A j, a2 a (b₁ + b₂) = a2 a b₁ + a2 a b₂)

-- deterministic timeout :-(

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 08:37):

Oh my bad, I forgot some ints.

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 08:38):

import algebra.group
import algebra.module

universe u

structure cdga (R : Type u) [comm_ring R] :=
(A :   Type u) -- universe monomorphism FTW
[hA :  n, add_comm_group (A n)]
[hRA :  n, module R (A n)]
(a2 :  i j , (A i)  (A j)  (A (i + j)))
(h21 :  i j,  r : R,  a : A i,  b : A j, a2 i j (r  a) b = r  (a2 a b))
(h22 :  i j,  r : R,  a : A i,  b : A j, a2 i j a (r  b) = r  (a2 a b))
(h23 :  i j,  r : R,  a₁ a₂ : A i,  b : A j, a2 i j (a₁ + a₂) b = a2 a₁ b + a2 a₂ b)
(h24 :  i j,  r : R,  a : A i,  b₁ b₂ : A j, a2 i j a (b₁ + b₂) = a2 a b₁ + a2 a b₂)

Hmm, maybe the computer scientists would have chosen different names...

view this post on Zulip Johan Commelin (Jun 12 2019 at 08:40):

We have bilinear maps in mathlib, don't we?

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 08:40):

That would be good.

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 08:40):

Not least because it would tell me the correct names ;-)

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 08:41):

structure cdga (R : Type u) [comm_ring R] :=
(A :   Type u) -- universe monomorphism FTW
[hA :  n, add_comm_group (A n)]
[hRA :  n, module R (A n)]
(mul :  {i j} , (A i)  (A j)  (A (i + j)))
(lin_left :  i j,  r : R,  a : A i,  b : A j, mul (r  a) b = r  (mul a b))
(lin_right :  i j,  r : R,  a : A i,  b : A j, mul a (r  b) = r  (mul a b))
(add_left :  i j,  r : R,  a₁ a₂ : A i,  b : A j, mul (a₁ + a₂) b = mul a₁ b + mul a₂ b)
(add_right :  i j,  r : R,  a : A i,  b₁ b₂ : A j, mul a (b₁ + b₂) = mul a b₁ + mul a b₂)

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 18:31):

We have bilinear maps in mathlib, don't we?

I can't find them, and I sort-of don't know how to search for them.

view this post on Zulip Johan Commelin (Jun 12 2019 at 18:33):

https://github.com/leanprover-community/mathlib/blob/66a86ffe010ffc32ee92e2e92cbdaf83487af168/src/linear_algebra/tensor_product.lean#L24

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 18:34):

All the bilinearity hypotheses are _inputs_ to that function. Is that what I'm looking for?

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 18:34):

I just want to say is_bilinear_map or something, right?

view this post on Zulip Johan Commelin (Jun 12 2019 at 18:34):

The output is a bilinear map

view this post on Zulip Johan Commelin (Jun 12 2019 at 18:34):

So you just want a term of such a type.

view this post on Zulip Johan Commelin (Jun 12 2019 at 18:35):

I.e., add subscript l to your arrows, and you're done

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 18:38):

failed to synthesize type class instance for add_comm_group (A j →ₗ[R] A (i + j)) :-/ Maybe I need to turn up the heat.

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 18:40):

darn it, why is this error not in the mathlib file but I'm getting it :-/

view this post on Zulip Reid Barton (Jun 12 2019 at 18:42):

hmm, maybe you need to import something?

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 18:42):

I'm importing the file Johan linked to :-)

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 18:43):

Oh! No I'm not! doh

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 18:44):

Ha ha I'd already explictly checked to see if that was the problem :-) Thanks.

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 18:55):

import algebra.group
import linear_algebra.tensor_product

universe u

variables {R : Type u} [comm_ring R] {m n : } (h : m = n)
  {A :   Type u} [ n, add_comm_group (A n)] [ n, module R (A n)]

def canonical_map (h : m = n) : A m  A n := (congr_arg A h).mp

instance canonical_hom : is_add_group_hom (canonical_map h : A m  A n) :=
begin
  subst h,
  exact is_add_group_hom.id
end

def canonical_R_hom (h : m = n) : linear_map R (A m) (A n) :=
begin
  subst h,
  exact linear_map.id
end

structure cdga (R : Type u) [comm_ring R] :=
(A :   Type u) -- universe monomorphism FTW
[hA :  n, add_comm_group (A n)]
[hRA :  n, module R (A n)]
(mul :  i j , (A i) [R] (A j) [R] (A (i + j)))
(one : A 0)
(one_mul :  {j},  (a : A j), canonical_map (zero_add j) (mul 0 j one a) = a)
(mul_one :  {j},  (a : A j), canonical_map (add_zero j) (mul j 0 a one) = a)
(mul_assoc :  {i j k},  (a : A i) (b : A j) (c : A k),
   canonical_map (add_assoc i j k) (mul (i+j) k (mul i j a b) c) = mul i (j + k) a (mul j k b c))

Does this count as a "mess" so far?

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 18:56):

It's kind of annoying that M →ₗ[R] N has a coercion to M -> N but it doesn't seem to kick in if you leave i and j implicit. Am I missing a trick?

view this post on Zulip Reid Barton (Jun 12 2019 at 18:56):

Well, ... oh

view this post on Zulip Reid Barton (Jun 12 2019 at 18:56):

I was about to say you could make i and j implicit

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 18:58):

def cool_id {i : } : (A i) [R] (A i) := linear_map.id

variables (i : ) (a : A i)

#check cool_id a
/-
function expected at
  cool_id
term has type
  ?m_2 ?m_3 →ₗ[?m_1] ?m_2 ?m_3
-/

view this post on Zulip Reid Barton (Jun 12 2019 at 18:58):

Currently it took you 93 characters to say (ab)c=a(bc)(ab)c = a(bc), which doesn't seem ideal, but surely we can improve it

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 18:59):

Shall I remove all unnecessary spaces?

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 18:59):

There will be some way of using notation I guess; I just didn't see immediately how to do it once I switched to this R-linear stuff.

view this post on Zulip Reid Barton (Jun 12 2019 at 19:00):

How about we instead add some unnecessary spaces to the tex source

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 19:01):

If I'd left mul as the actual map with i and j implicit we'd save a few characters. Calling it m would save more though; but I don't know how to get the notation * working, even if I start splitting up the structure into smaller aux structures first

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 19:09):

Every 2 minutes Lean segfaults, for some reason, when I'm writing this structure. "There's something fishy about structures" someone once said on this chat, and I think they're right.

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 19:24):

structure cdga (R : Type u) [comm_ring R] :=
(A :   Type u) -- universe monomorphism FTW
[hA :  n, add_comm_group (A n)]
[hRA :  n, module R (A n)]
(mul :  i j , (A i) [R] (A j) [R] (A (i + j)))
(one : A 0)
(one_mul :  {j} (a : A j), canonical_map (zero_add j) (mul 0 j one a) = a)
(mul_one :  {j} (a : A j), canonical_map (add_zero j) (mul j 0 a one) = a)
(mul_assoc :  {i j k} (a : A i) (b : A j) (c : A k),
   canonical_map (add_assoc i j k) (mul (i+j) k (mul i j a b) c) = mul i (j + k) a (mul j k b c))
(graded_comm :  {i j} (a : A i) (b : A j),
  canonical_map (add_comm j i) (mul j i b a) = (-1 : R)^(i * j)  mul i j a b)
(d :  n, (A n) [R] (A (n + 1)))
(d_squared :  {n} (a : A n), (d (n + 1) : A (n + 1)  A (n + 2)) (d n a) = 0)
(Leibniz :  i j (a : A i) (b : A j), d (i + j) (mul i j a b) =
   canonical_map (show i + 1 + j = i + j + 1, by simp)
     ((mul (i + 1) j : A (i + 1)  (A j [R] A (i + 1 + j))) (d i a) b) +
   (-1 : R) ^ i  canonical_map (show i + (j + 1) = i + j + 1, by simp)
     ((mul i (j + 1) : A i  (A (j + 1) [R] A (i + (j + 1)))) a (d j b)))

Leibniz didn't go too well.

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 19:25):

The muls for some reason refused to coerce to functions.

view this post on Zulip Johan Commelin (Jun 12 2019 at 19:37):

@Reid Barton Seems like you picked a good topic for the challenge. @Patrick Massot posted about this formalization "olympiad" kind of thing. Maybe this would make a nice exercise (-; And maybe @Mario Carneiro could give us some hints how to solve it...

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 19:39):

I'm about to start the challenge; I have just got enough time to try d(ab)=0 before I need to go and do other things. The file is getting long so I'll post a gist when I finish / give up / have to go

view this post on Zulip Reid Barton (Jun 12 2019 at 19:42):

Can you replace all the proof arguments to canonical_map by by ring or similar? Or does the elaborator not yet know what types it's trying to prove equal?

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 19:46):

It has worked for the two examples I've tried. There's some way of getting it to do it automatically isn't there. Some dot notation thing.

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 19:48):

It looks something like def canonical_R_hom (h : m = n . ring) : linear_map R (A m) (A n) := but I need to create something of type tactic unit which does ring

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 19:50):

Yeah, it doesn't always work :-( The elaborator makes the wrong guess sometimes, ring proves it (rfl would probably also prove it) and then I run into trouble later.

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 20:05):

https://gist.github.com/kbuzzard/f5ee35457c5d257ceec58c66d7da0c38

I didn't quite finish :-( I have to prove 0 = 0. I was hoping rw is_add_group_hom.zero would work but it didn't, and now I have to go for a while.

view this post on Zulip Reid Barton (Jun 12 2019 at 20:06):

I wonder whether it matters which side you put the canonical_map on

view this post on Zulip Reid Barton (Jun 12 2019 at 20:07):

If the elaborator could figure out the types involved at the right time, the entire canonical_map (by ring) could become a bit of notation

view this post on Zulip Reid Barton (Jun 12 2019 at 20:09):

Maybe a = canonical_map (_) b is easier than canonical_map (_) a = b

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 21:10):

It's not going to be a simp lemma that way around ;-)

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

--set_option pp.proofs true
lemma ker_d_prod (A : cdga R) {i j : } (a : A.A i) (b : A.A j) (ha : ((A.d i) : A.A i  A.A (i + 1)) a = 0) (hb : A.d j b = 0) :
  A.d (i + j) (A.mul i j a b) = 0 :=
begin
  rw [A.Leibniz, ha, hb, zero_mul, mul_zero],
  rw @is_add_group_hom.map_zero (A.A (i + 1 + j)) (A.A (i + j + 1)) _ _ (canonical_map (show i + 1 + j = i + j + 1, by ring)),
  rw @is_add_group_hom.map_zero (A.A (i + (j + 1))) (A.A (i + j + 1)) _ _ (canonical_map (show i + (j + 1) = i + j + 1, by ring)),
  rw [zero_add, smul_zero],
end

What was that about "messy"?

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 21:23):

I updated the gist and now I'm back to cleaning the kitchen. @Kenny Lau @Mario Carneiro I'm sure both of you will see ways to tidy this up.

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 21:23):

https://gist.github.com/kbuzzard/f5ee35457c5d257ceec58c66d7da0c38

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 21:27):

See Reid's initial post for the maths

view this post on Zulip Kenny Lau (Jun 12 2019 at 21:42):

import algebra.group
import linear_algebra.tensor_product
import tactic.ring

universes v u

section canonical

variables (R : Type u) [comm_ring R]
variables (A :   Type v) {m n : } (h : m = n)
include h

def canonical_map : A m  A n := (congr_arg A h).mp

instance canonical_hom [ n, add_comm_group (A n)] : is_add_group_hom (canonical_map A h : A m  A n) :=
begin
  subst h,
  exact is_add_group_hom.id
end

def canonical_R_hom [ n, add_comm_group (A n)] [ n, module R (A n)] : (A m) [R] (A n) :=
begin
  subst h,
  exact linear_map.id
end

end canonical

structure cdga (R : Type u) [comm_ring R] :=
(A :   Type v) -- universe polymorphism FTW
[hA :  n, add_comm_group (A n)]
[hRA :  n, module R (A n)]
(mul :  i j , (A i) [R] (A j) [R] (A (i + j)))
(one : A 0)
(one_mul :  {j} (a : A j), canonical_R_hom R A (zero_add j) (mul 0 j one a) = a)
(mul_one :  {j} (a : A j), canonical_R_hom R A (add_zero j) (mul j 0 a one) = a)
(mul_assoc :  {i j k} (a : A i) (b : A j) (c : A k),
   canonical_R_hom R A (add_assoc i j k) (mul (i+j) k (mul i j a b) c) = mul i (j + k) a (mul j k b c))
(graded_comm :  {i j} (a : A i) (b : A j),
  canonical_R_hom R A (add_comm j i) (mul j i b a) = (-1 : R)^(i * j)  mul i j a b)
(d :  n, (A n) [R] (A (n + 1)))
(d_squared :  {n} (a : A n), (d (n + 1) : A (n + 1)  A (n + 2)) (d n a) = 0)
(Leibniz :  i j (a : A i) (b : A j), d (i + j) (mul i j a b) =
   canonical_R_hom R A (add_right_comm i (1:) j) (mul (i+(1:)) j (d i a) b) +
   (-1 : R) ^ i  canonical_R_hom R A (add_assoc i j (1:)).symm (mul i (j+(1:)) a (d j b)))
attribute [instance] cdga.hA cdga.hRA

/-
If AAA is a CDGA then its cohomology H∗(A)H^*(A)H∗(A) is a graded commutative algebra. Basically this amounts to checking that

    if da=0da = 0da=0 and db=0db = 0db=0, then d(a⋅b)=0d(a \cdot b) = 0d(a⋅b)=0
    if da=0da = 0da=0 and b=db′b = db'b=db′, then a⋅ba \cdot ba⋅b is ddd of something (namely (−1)ia⋅b′(-1)^i a \cdot b'(−1)ia⋅b′ where a∈Aia \in A_ia∈Ai​),
    similarly if a=da′a = da'a=da′ and db=0db = 0db=0 then a⋅ba \cdot ba⋅b is ddd of something
    and therefore the multiplication Ai×Aj→Ai+jA_i \times A_j \to A_{i+j}Ai​×Aj​→Ai+j​ restricts/descends to the kernel of ddd modulo the image of ddd.

-/
namespace cdga

variables (R : Type u) [comm_ring R] (A : cdga R)

lemma zero_mul {i j : } (b : A.A j) : A.mul i j (0 : A.A i) b = 0 :=
by rw [linear_map.map_zero, linear_map.zero_apply]

lemma mul_zero {i j : } (a : A.A i) : A.mul i j a (0 : A.A j) = 0 :=
linear_map.map_zero _

--set_option pp.proofs true
lemma ker_d_prod (A : cdga R) {i j : } (a : A.A i) (b : A.A j) (ha : A.d i a = 0) (hb : A.d j b = 0) :
  A.d (i + j) (A.mul i j a b) = 0 :=
by rw [A.Leibniz, ha, hb, zero_mul, mul_zero, linear_map.map_zero, linear_map.map_zero, zero_add, smul_zero]

end cdga

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 22:18):

I couldn't get map_zero to work with unbundled homs. You have changed to bundled homs and now it works?

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 22:18):

Or was it the change to universe polymorphism which was decisive? ;-)

view this post on Zulip Kenny Lau (Jun 12 2019 at 22:36):

well you didn't use the linear map, so of course you couldn't access map_zero

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 22:37):

I was using is_add_group_hom.map_zero IIRC

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 22:37):

and I made that an instance. I'm looking at your changes. I made the bundled and unbundled maps and you have completely switched to bundled maps.

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 22:38):

I had problems with coercions to functions not kicking in but you seem to have solved them. Is this because of the bundling?

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 22:38):

 rw @is_add_group_hom.map_zero (A.A (i + 1 + j)) (A.A (i + j + 1)) _ _ (canonical_map (show i + 1 + j = i + j + 1, by ring)),

view this post on Zulip Kenny Lau (Jun 12 2019 at 22:40):

I turned on pp.all and it turns out that 1 was the problem

view this post on Zulip Kenny Lau (Jun 12 2019 at 22:40):

changing it to (1:ℕ) resolves the issue

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:04):

I want to see if an untyped formulation is easier

view this post on Zulip Kenny Lau (Jun 12 2019 at 23:22):

@Mario Carneiro what does that mean?

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:23):

stay tuned

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:43):

import linear_algebra.basic
universes v u
def env (A :   Type v) := option (Σ n, A n)

def env.as {A :   Type v} (e : env A) (n) : option (A n) :=
do m, (a:A m)  e,
  if h : m = n then some (by rw  h; exact a) else none

instance (A :   Type v) (n) : has_coe (A n) (env A) := ⟨λ x, some n, x⟩⟩

instance (A :   Type v) [ n, has_add (A n)] : has_add (env A) :=
⟨λ x y, do n, a  x, b  y.as n, some n, a + b⟩⟩

instance (R : Type u) (A :   Type v) [ n, has_scalar R (A n)] : has_scalar R (env A) :=
⟨λ r x, x.map (λ n, a, n, r  a)

def env.mul {A :   Type v} (f :  i j, A i  A j   A (i + j))
  (x y : env A) : env A :=
do i, a  x, j, b  y, some i + j, f i j a b

def cdga_mul {R : Type u} [comm_ring R] {A :   Type v}
  [ n, add_comm_group (A n)] [ n, module R (A n)]
  (f :  i j, A i [R] A j [R] A (i + j)) :
  env A  env A  env A :=
env.mul (λ i j x y, f i j x y)

def cdga_d {R : Type u} [comm_ring R] {A :   Type v}
  [ n, add_comm_group (A n)] [ n, module R (A n)]
  (f :  n, A n [R] A (n + 1))
  (x : env A) : env A :=
x.map (λ n, a, n+1, f n a)

structure cdga (R : Type u) [comm_ring R] :=
(A :   Type v) -- universe polymorphism FTW
[hA :  n, add_comm_group (A n)]
[hRA :  n, module R (A n)]
(mul :  i j, (A i) [R] (A j) [R] (A (i + j)))
(infix ` * ` := cdga_mul mul)
(one : A 0) (notation `𝟙` := (one : env A))
(one_mul :  {j} (a : A j), 𝟙 * a = a)
(mul_one :  {j} (a : A j), a * 𝟙 = a)
(mul_assoc :  {i j k} (a : A i) (b : A j) (c : A k), (a * b) * c = a * (b * c))
(graded_comm :  {i j} (a : A i) (b : A j),
  b * a = ((-1 : R)^(has_mul.mul i j))  a * b)
(d :  n, A n [R] A (n + 1))
(notation `D` := cdga_d d)
(d_squared :  {n} (a : A n), D (D a) = (0 : A (n+2)))
(Leibniz :  i j (a : A i) (b : A j), D (a * b) = D a * b + (-1:R)^i  a * D b)

view this post on Zulip Kenny Lau (Jun 12 2019 at 23:44):

why did you reverse my universes v u?

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:44):

I wrote it myself, didn't see that

view this post on Zulip Kenny Lau (Jun 12 2019 at 23:45):

how on earth does (mul_assoc : ∀ {i j k} (a : A i) (b : A j) (c : A k), (a * b) * c = a * (b * c)) work?

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:45):

because untyped is awesome

view this post on Zulip Kenny Lau (Jun 12 2019 at 23:46):

I don't understand

view this post on Zulip Kenny Lau (Jun 12 2019 at 23:46):

oh wait nothing

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:46):

a,b,c are coerced to env A, and env A is closed under multiplication

view this post on Zulip Kenny Lau (Jun 12 2019 at 23:47):

ok now how on earth does it work

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:47):

just like that...?

view this post on Zulip Kenny Lau (Jun 12 2019 at 23:47):

oh I understand now

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:47):

there are no add comm manipulations this way

view this post on Zulip Kenny Lau (Jun 12 2019 at 23:47):

ok this is interesting

view this post on Zulip Kenny Lau (Jun 12 2019 at 23:48):

but I'm not very convinced that it will be easy to use

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:48):

you have to hide the unfolding of mul and such

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:48):

you just rewrite with the equations

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:50):

You can use a typeclass predicate has_type : env A -> out_param nat -> Prop to find that an expression is well defined, and extract the value from there

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:52):

Obviously this is very different from the usual way of doing stuff in lean, but it totally works; this is how ZFC formalization goes

view this post on Zulip Kenny Lau (Jun 12 2019 at 23:53):

I'm not convinced the option is necessary

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:53):

It's not

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:54):

it's slightly better hygiene, but you could use <0,0> instead

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:54):

it doesn't really matter as long as you promise not to write bad expressions

view this post on Zulip Reid Barton (Jun 12 2019 at 23:55):

BTW in math we often just add together things in different A ns and work in the direct sum or direct product as appropriate

view this post on Zulip Reid Barton (Jun 12 2019 at 23:55):

however I intentionally didn't mention this to avoid biasing the approaches that people came up with

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:55):

ah, that might be the better choice since then you get some saner closure conditions

view this post on Zulip Reid Barton (Jun 12 2019 at 23:56):

In fact the stacks project defines one of these as an algebra A=iAiA = \bigoplus_i A_i (direct sum of modules) with the property that AiAjAi+jA_i \cdot A_j \subset A_{i+j} etc.

view this post on Zulip Reid Barton (Jun 12 2019 at 23:57):

but it's more common to see a definition of the sort that I gave originally

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:57):

the major downside of my approach is that env isn't any reasonable kind of algebraic class

view this post on Zulip Mario Carneiro (Jun 12 2019 at 23:59):

I have long been of the opinion that doing anything nontrivial with expressions in a type dependency is possible but inadvisable in DTT

view this post on Zulip Kenny Lau (Jun 13 2019 at 01:02):

@Johan Commelin now I understand why you want i+1-1 = i = i-1+1 to be defeq

view this post on Zulip Johan Commelin (Jun 13 2019 at 03:49):

Just wait till we seriously start doing complexes and long exact sequences etc...

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

I have long been of the opinion that doing anything nontrivial with expressions in a type dependency is possible but inadvisable in DTT

Yeah but the thing is that we're going to make all of mathematics in DTT so we'd better come up with some coherent way of approaching these issues.

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

structure cdga (R : Type u) [comm_ring R] :=
(A :   Type v) -- universe polymorphism FTW

@Kenny Lau I thought it was bad to randomly mention extra universes in a structure, when they couldn't be inferred from the input.

view this post on Zulip Kenny Lau (Jun 13 2019 at 14:32):

talk to the category theorists

view this post on Zulip Mario Carneiro (Jun 13 2019 at 15:36):

I wasn't touching that aspect. More likely A and stuff would be a parameter, but I don't know all that goes into the math surrounding this

view this post on Zulip Reid Barton (Jun 13 2019 at 17:00):

From a math perspective it doesn't make much sense to have just the underlying types A a parameter, but then the same is true about unbundled rings and so on


Last updated: May 12 2021 at 08:14 UTC