CDGAs

Stream: maths

[Reid Barton]

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]

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

[Reid Barton]

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

[Johan Commelin]

And who are you challenging :stuck_out_tongue_wink:?

[Reid Barton]

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

[Kevin Buzzard]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

The system needs fixing, not just another work around

[Neil Strickland]

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

[Floris van Doorn]

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]

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

[Kevin Buzzard]

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]

Oh my bad, I forgot some ints.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

That would be good.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I just want to say is_bilinear_map or something, right?

[Johan Commelin]

The output is a bilinear map

[Johan Commelin]

So you just want a term of such a type.

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[Reid Barton]

hmm, maybe you need to import something?

[Kevin Buzzard]

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

[Kevin Buzzard]

Oh! No I'm not! doh

[Kevin Buzzard]

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

[Kevin Buzzard]

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?

[Kevin Buzzard]

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?

[Reid Barton]

Well, ... oh

[Reid Barton]

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

[Kevin Buzzard]

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]

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]

Shall I remove all unnecessary spaces?

[Kevin Buzzard]

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.

[Reid Barton]

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

[Kevin Buzzard]

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]

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]

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]

The muls for some reason refused to coerce to functions.

[Johan Commelin]

@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]

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]

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]

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]

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]

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]

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]

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

[Reid Barton]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

See Reid's initial post for the maths

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kevin Buzzard]

I was using is_add_group_hom.map_zero IIRC

[Kevin Buzzard]

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]

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]

 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]

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

[Kenny Lau]

changing it to (1:ℕ) resolves the issue

[Mario Carneiro]

I want to see if an untyped formulation is easier

[Kenny Lau]

@Mario Carneiro what does that mean?

[Mario Carneiro]

stay tuned

[Mario Carneiro]

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]

why did you reverse my universes v u?

[Mario Carneiro]

I wrote it myself, didn't see that

[Kenny Lau]

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]

because untyped is awesome

[Kenny Lau]

I don't understand

[Kenny Lau]

oh wait nothing

[Mario Carneiro]

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

[Kenny Lau]

ok now how on earth does it work

[Mario Carneiro]

just like that...?

[Kenny Lau]

oh I understand now

[Mario Carneiro]

there are no add comm manipulations this way

[Kenny Lau]

ok this is interesting

[Kenny Lau]

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

[Mario Carneiro]

you have to hide the unfolding of mul and such

[Mario Carneiro]

you just rewrite with the equations

[Mario Carneiro]

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]

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]

I'm not convinced the option is necessary

[Mario Carneiro]

It's not

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

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]

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

[Mario Carneiro]

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

[Reid Barton]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

talk to the category theorists

[Mario Carneiro]

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]

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