## Stream: maths

### Topic: CDGAs

#### 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 $R$ consists of
1. for each natural number $n$, an $R$-module $A_n$
2. for each $i$ and $j$, an $R$-bilinear multiplication map $A_i \times A_j \to A_{i+j}$
3. a unit $1 \in A_0$
4. satisfying the obvious unitality and associativity conditions $1 \cdot a = a$, $a \cdot 1 = a$, $(a \cdot b) \cdot c = a \cdot (b \cdot c)$ for $a \in A_i$, $b \in A_j$, $c \in A_k$
5. as well as the graded commutativity relation $b \cdot a = (-1)^{ij} a \cdot b$ for $a \in A_i$, $b \in A_j$
6. along with an $R$-linear differential $d : A_n \to A_{n+1}$ for each $n$
7. satisfying $d^2 = 0$
8. as well as the Leibniz rule $d(a\cdot b) = da \cdot b + (-1)^i a \cdot db$ for $a \in A_i$, $b \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 $A$ is a CDGA then its cohomology $H^*(A)$ is a graded commutative algebra. Basically this amounts to checking that

• if $da = 0$ and $db = 0$, then $d(a \cdot b) = 0$
• if $da = 0$ and $b = db'$, then $a \cdot b$ is $d$ of something (namely $(-1)^i a \cdot b'$ where $a \in A_i$),
• similarly if $a = da'$ and $db = 0$ then $a \cdot b$ is $d$ of something
and therefore the multiplication $A_i \times A_j \to A_{i+j}$ restricts/descends to the kernel of $d$ modulo the image of $d$.

#### 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?

#### Reid Barton (Jun 11 2019 at 13:33):

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

#### Johan Commelin (Jun 11 2019 at 13:36):

And who are you challenging :stuck_out_tongue_wink:?

#### Reid Barton (Jun 11 2019 at 13:39):

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

#### 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?

#### 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.

#### 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)).

#### 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)

#### Reid Barton (Jun 11 2019 at 13:44):

To check $da = 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)

#### Reid Barton (Jun 11 2019 at 13:45):

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

#### 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 $d$ as $A_n \to A_{1+n}$, but for some reason we don't do that.

#### 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 $d$ as $A_n \to A_{1+n}$, but for some reason we don't do that.

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

#### Kevin Buzzard (Jun 11 2019 at 14:10):

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

#### 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?

#### Kevin Buzzard (Jun 11 2019 at 14:22):

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

#### 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


#### Johan Commelin (Jun 11 2019 at 14:36):

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

#### Johan Commelin (Jun 11 2019 at 14:37):

The system needs fixing, not just another work around

#### 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,
exact {map_add := λ a b, rfl}
end


#### 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 $A_n$ as codomain, only $A_{(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(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)

#### 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,
end


#### 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 :-(


#### Kevin Buzzard (Jun 12 2019 at 08:37):

Oh my bad, I forgot some ints.

#### 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...

#### Johan Commelin (Jun 12 2019 at 08:40):

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

#### Kevin Buzzard (Jun 12 2019 at 08:40):

That would be good.

#### Kevin Buzzard (Jun 12 2019 at 08:40):

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

#### 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₂)


#### 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.

#### Johan Commelin (Jun 12 2019 at 18:33):

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

#### Kevin Buzzard (Jun 12 2019 at 18:34):

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

#### Kevin Buzzard (Jun 12 2019 at 18:34):

I just want to say is_bilinear_map or something, right?

#### Johan Commelin (Jun 12 2019 at 18:34):

The output is a bilinear map

#### Johan Commelin (Jun 12 2019 at 18:34):

So you just want a term of such a type.

#### Johan Commelin (Jun 12 2019 at 18:35):

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

#### 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.

#### Kevin Buzzard (Jun 12 2019 at 18:40):

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

#### Reid Barton (Jun 12 2019 at 18:42):

hmm, maybe you need to import something?

#### Kevin Buzzard (Jun 12 2019 at 18:42):

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

#### Kevin Buzzard (Jun 12 2019 at 18:43):

Oh! No I'm not! doh

#### Kevin Buzzard (Jun 12 2019 at 18:44):

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

#### 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,
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?

#### 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?

Well, ... oh

#### Reid Barton (Jun 12 2019 at 18:56):

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

#### 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
-/


#### Reid Barton (Jun 12 2019 at 18:58):

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

#### Kevin Buzzard (Jun 12 2019 at 18:59):

Shall I remove all unnecessary spaces?

#### 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.

#### 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

#### 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.

#### 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.

#### Kevin Buzzard (Jun 12 2019 at 19:25):

The muls for some reason refused to coerce to functions.

#### 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...

#### 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

#### 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?

#### 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.

#### 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

#### 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.

#### 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.

#### Reid Barton (Jun 12 2019 at 20:06):

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

#### 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

#### Reid Barton (Jun 12 2019 at 20:09):

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

#### Kevin Buzzard (Jun 12 2019 at 21:10):

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

#### 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)),
end


#### 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.

#### Kevin Buzzard (Jun 12 2019 at 21:23):

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

#### Kevin Buzzard (Jun 12 2019 at 21:27):

See Reid's initial post for the maths

#### 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,
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


#### 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?

#### Kevin Buzzard (Jun 12 2019 at 22:18):

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

#### 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

#### 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.

#### 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?

#### 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)),


#### Kenny Lau (Jun 12 2019 at 22:40):

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

#### Kenny Lau (Jun 12 2019 at 22:40):

changing it to (1:ℕ) resolves the issue

#### Mario Carneiro (Jun 12 2019 at 23:04):

I want to see if an untyped formulation is easier

#### Kenny Lau (Jun 12 2019 at 23:22):

@Mario Carneiro what does that mean?

stay tuned

#### 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)


#### Kenny Lau (Jun 12 2019 at 23:44):

why did you reverse my universes v u?

#### Mario Carneiro (Jun 12 2019 at 23:44):

I wrote it myself, didn't see that

#### 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?

#### Mario Carneiro (Jun 12 2019 at 23:45):

because untyped is awesome

#### Kenny Lau (Jun 12 2019 at 23:46):

I don't understand

oh wait nothing

#### Mario Carneiro (Jun 12 2019 at 23:46):

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

#### Kenny Lau (Jun 12 2019 at 23:47):

ok now how on earth does it work

#### Mario Carneiro (Jun 12 2019 at 23:47):

just like that...?

#### Kenny Lau (Jun 12 2019 at 23:47):

oh I understand now

#### Mario Carneiro (Jun 12 2019 at 23:47):

there are no add comm manipulations this way

#### Kenny Lau (Jun 12 2019 at 23:47):

ok this is interesting

#### Kenny Lau (Jun 12 2019 at 23:48):

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

#### Mario Carneiro (Jun 12 2019 at 23:48):

you have to hide the unfolding of mul and such

#### Mario Carneiro (Jun 12 2019 at 23:48):

you just rewrite with the equations

#### 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

#### 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

#### Kenny Lau (Jun 12 2019 at 23:53):

I'm not convinced the option is necessary

It's not

#### Mario Carneiro (Jun 12 2019 at 23:54):

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

#### Mario Carneiro (Jun 12 2019 at 23:54):

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

#### 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

#### 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

#### Mario Carneiro (Jun 12 2019 at 23:55):

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

#### Reid Barton (Jun 12 2019 at 23:56):

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

#### Reid Barton (Jun 12 2019 at 23:57):

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

#### 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

#### 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

#### 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

#### Johan Commelin (Jun 13 2019 at 03:49):

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

#### 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.

#### 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.

#### Kenny Lau (Jun 13 2019 at 14:32):

talk to the category theorists

#### 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

#### 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: Jan 31 2023 at 21:29 UTC