flexible indices

Stream: maths

[Johan Commelin]

I'm fooling around with sequences of groups. Here is an extract of some code:

import algebra.group group_theory.subgroup
import category_theory.instances.groups
import category_theory.functor_category
import data.set.function

universes v v₁ v₂ v₃ u u₁ u₂ u₃ -- declare the `v`'s first; see `category_theory.category` for an explanation

namespace category_theory
open set instances
variables (C : Type u₁) [𝒞 : category.{v₁} C]
include 𝒞

def sequence := ℤ ⥤ C

namespace sequence

instance : category (sequence C) := functor.category _ _

variables {C} (X : sequence C)

def delta (i : ℤ) {j : ℤ} (h : i = j - 1 . obviously) :
  X.obj i ⟶ X.obj j :=
X.map $
begin
  rw auto_param_eq at h,
  rw h, tidy,
end

[Johan Commelin]

What I am after is a nice definition of delta

[Johan Commelin]

It is the map X.obj i \hom X.obj (i+1) but I want to use unification to replace i with (i-1+1) when necessary.

[Johan Commelin]

Currently this fails:

variable (i : ℤ)
#check X.delta (i-1) ≫ X.delta i

[Johan Commelin]

Because the second X.delta should be X.delta (i-1+1), which is ugly.

[Johan Commelin]

My goal is to make things like this typecheck:

variable (A : sequence Group)

def is_complex :=
∀ (i : ℤ), range (A.delta (i-1)) ⊆ ker (A.delta i)

[Kenny Lau]

(never mind)

[Kenny Lau]

also your code doesn't work because category_theory.instances.groups doesn't exist

[Johan Commelin]

Yes, I know. It exists on my machine. It's a pity it doesn't yet exist in mathlib.

[Johan Commelin]

Here is category_theory/instances/groups.lean:

/- Copyright (c) 2018 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin

Introduce Group -- the category of groups.

Currently only the basic setup.
Copied from monoids.lean.
-/

import category_theory.concrete_category
import category_theory.fully_faithful
import category_theory.adjunction
import data.finsupp

universes u v

open category_theory

namespace category_theory.instances

/-- The category of groups and group morphisms. -/
@[reducible] def Group : Type (u+1) := bundled group

instance (G : Group) : group G := G.str

instance concrete_is_group_hom :
  concrete_category @is_group_hom :=
⟨by introsI α ia; apply_instance,
  by introsI α β γ ia ib ic f g hf hg; apply_instance⟩

instance Group_hom_is_group_hom {G₁ G₂ : Group} (f : G₁ ⟶ G₂) :
  is_group_hom (f : G₁ → G₂) := f.2

instance : has_one Group := ⟨{ α := punit, str := by tidy }⟩

/-- The category of commutative groups and group morphisms. -/
@[reducible] def CommGroup : Type (u+1) := bundled comm_group

instance (x : CommGroup) : comm_group x := x.str

@[reducible] def is_comm_group_hom {α β} [comm_group α] [comm_group β] (f : α → β) : Prop :=
is_group_hom f

instance concrete_is_comm_group_hom : concrete_category @is_comm_group_hom :=
⟨by introsI α ia; apply_instance,
  by introsI α β γ ia ib ic f g hf hg; apply_instance⟩

instance CommGroup_hom_is_comm_group_hom {R S : CommGroup} (f : R ⟶ S) :
  is_comm_group_hom (f : R → S) := f.2

namespace CommGroup
/-- The forgetful functor from commutative groups to groups. -/
def forget_to_Group : CommGroup ⥤ Group :=
concrete_functor
  (by intros _ c; exact { ..c })
  (by introsI _ _ _ _ f i;  exact { ..i })

instance : faithful (forget_to_Group) := {}

instance : has_one CommGroup := ⟨{ α := punit, str := by tidy }⟩

end CommGroup

end category_theory.instances

[Kevin Buzzard]

What's the story as to why it's not in mathlib? My MSc student was going to use categories for doing schemes but we decided it wasn't a good idea because categories seemed to be happening too slowly

[Johan Commelin]

The story is that nobody copied the file about the category of monoids and did a search-replace s/monoid/group/. That's all.

[Johan Commelin]

My goal is to make things like this typecheck:

variable (A : sequence Group)

def is_complex :=
∀ (i : ℤ), range (A.delta (i-1)) ⊆ ker (A.delta i)

Does anyone have an idea how to make this work?
I think writing A.delta (i-1+1) is very very ugly.

[Mario Carneiro]

Why not use +1 instead of -1?

[Mario Carneiro]

it's over all integers

[Mario Carneiro]

Another way to flexify the indices for dependent types is to have an equality argument i+1 = j and have i on the left and j on the right

[Johan Commelin]

But can we make it transparent?

[Mario Carneiro]

don't know what you intend to do with this

[Johan Commelin]

Why not use +1 instead of -1?

I could do that here. But I think this issue will show up elsewhere as soon as we start looking in a broader range of indices.

[Johan Commelin]

don't know what you intend to do with this
For starters we could try to prove the snake lemma (-;

[Mario Carneiro]

More generally, you want an inductive family describing the allowable index combinations

[Mario Carneiro]

In this case it is just inductive next : nat -> nat -> Prop | mk (i) : next i (i+1)

[Johan Commelin]

Hmm, how do I use next?

[Johan Commelin]

Should I put that in my definition of delta?

[Mario Carneiro]

def is_complex :=
∀ (i j : ℤ), next i j -> range (A.delta i) ⊆ ker (A.delta j)

[Mario Carneiro]

or are you looking somewhere else?

[Johan Commelin]

Aah, ok

[Johan Commelin]

But that means I have 3 explicit arguments. So I can't just write A.delta i

[Johan Commelin]

I would like to tell Lean: "If unification knows what j should be, use that. Otherwise, default to (i+1)."

[Mario Carneiro]

Yeah, I think so... it's just like with categories, you want the objects to be there before the morphisms, rather than extracting objects as the dom/cod of morphisms

[Johan Commelin]

And after that I say to Lean: "Hey, 95% of the time you can prove next i j by mk i. Otherwise, simplify the expression for j before doing that."

[Johan Commelin]

And so in 99% of the cases I can get away with just writing A.delta i. And in 1% of the cases I might to actually work on the proof obligation...

[Johan Commelin]

If something like that can work, that would be cool.

[Mario Carneiro]

So is_complex is actually talking about three objects....

[Mario Carneiro]

def is_complex :=
∀ {{i j k : ℤ}} (n1: next i j) (n2 : next j k), range (A.delta n1) ⊆ ker (A.delta n2)

[Kenny Lau]

what is {{}}?

[Mario Carneiro]

half implicit, too lazy to unicode

[Mario Carneiro]

I think it is working ascii notation though

[Kenny Lau]

what is half implicit?

[Mario Carneiro]

not applied unless you apply an argument after them

[Mario Carneiro]

like in the definition of subset

[Kenny Lau]

:o

[Johan Commelin]

Hmm, but I think you are working on the wrong part. The definition of delta has to change.

[Johan Commelin]

is_complex is just an example of something that doesn't typecheck with the current definition of delta.

[Mario Carneiro]

I did that... A.delta {i j} n1

[Johan Commelin]

Ooh, right. Ok.

[Johan Commelin]

But that means I can't write A.delta i, can I?

[Mario Carneiro]

although possibly i and j shouldn't be implicit - this will print a bit weird if n1 is not a simple term

[Mario Carneiro]

No, I'm claiming that's a bad idea

[Mario Carneiro]

If you don't have the objects lying around already, you can use +1 and -1 to access next elements, but if you ever want to link two of them together you need a variable for the common object

[Mario Carneiro]

is_complex is a good example of this - j is mediating the connection between i and k

[Mario Carneiro]

I know this looks silly but it's a DTT thing

[Johan Commelin]

This will be hard to explain to mathematicians...

[Johan Commelin]

Why can't automation help us here?

[Mario Carneiro]

because DTT doesn't like it when you try to prove defeqs

[Johan Commelin]

If Lean figures out j by unification, that's cool. If it didn't: use i+1.

[Mario Carneiro]

You want all rewriting and stuff to happen in prop land

[Mario Carneiro]

but delta is data, so it needs a general type

[Mario Carneiro]

it's not a question of figuring out the expressions, it's about making i+1-1 defeq to i

[Johan Commelin]

Hmmm, I think that I wouldn't mind if automation could also help us with providing data, and not only proofs.

[Patrick Massot]

I don't know if automation is the right word here, but it's pretty clear that proof assistants that require using this next trick are not ready for use by mathematicians

[Mario Carneiro]

It's about wrangling DTT issues

[Mario Carneiro]

You are causing equality of integers to propagate to equality of types, which is bad

[Patrick Massot]

I understand. It means we need either better wrangling tools or a better foundational framework. I'm not saying this is an easy question

[Mario Carneiro]

I am in favor of both of those

[Patrick Massot]

What a nice thesis topic!

[Johan Commelin]

Mario, I agree with Patrick. I understand the issues. But the issues are non-mathematical, so they should be hidden. Somehow...

[Johan Commelin]

In the end, DTT should be our assembly language. We want a Python on top of that.

[Patrick Massot]

You already have it: the tactic language

[Mario Carneiro]

DTT is a horrible assembly language

[Mario Carneiro]

it's like javascript - high level ish but used for low level things

[Mario Carneiro]

I know a much better proof assembly language, and it starts with M

[Johan Commelin]

Sure, but is there a Python on top of your M?

[Johan Commelin]

One that will let me define functors on objects and morphisms, and check that they are lawful in a completely transparent way?

[Mario Carneiro]

Proof automation is hard, and no one has a perfect solution. Lean could have the stuff you are talking about if it didn't have to fight its own foundation

[Johan Commelin]

What do you mean with that last sentence?

[Mario Carneiro]

You could just rewrite i+1-1 = i with the simplifier and we would all be happy

[Johan Commelin]

Sure, that's exactly what I would want. But what do you mean with:

Lean could have the stuff you are talking about if it didn't have to fight its own foundation
Is that an issue that can be solved, or is this fight some intrinsic DTT issue?

[Mario Carneiro]

it's an intrinsic DTT issue

[Mario Carneiro]

defeq matters, and tactics can't change that

[Johan Commelin]

Aah, so Lean will always be fighting its foundations.

[Johan Commelin]

So, why don't we write a Python-like on top of your assembly M? Do you think we would get further into state-of-the-art research level maths with a Python-like on top of M? Or is Lean just the best there is, and are we stuck with a system that fights its own foundations?

[Mario Carneiro]

You are hitting surprisingly close to my current research areas

[Johan Commelin]

That only means that I've been paying attention to what you've been saying on Zulip over the last couple of months (-;

[Mario Carneiro]

I think that the killer combo is untyped foundations (ZFC like) + good tactic language + metaprogramming

[Mario Carneiro]

as you can see lean has 2 out of 3

[Mario Carneiro]

Isabelle gets pretty close, but it's not quite untyped foundations and as a result they are stuck with some things

[Johan Commelin]

Hmmm, so why again did you give my colleagues that nlab blogpost on why type theory p0wns set theory?

[Mario Carneiro]

I didn't write it, and I don't really endorse most of nLab philosophy

[Mario Carneiro]

but it's a good place to find the philosophy when you want it

[Johan Commelin]

Why not use +1 instead of -1?

So, for is_complex I could do this. But for is_exact_at (i : int) you need to reference A.obj (i-1) at some point. You can't avoid the subtraction. (Unless you want to break with the indexing conventions, but that will just move the pain to the next page, where it will hit you twice as hard.)

[Mario Carneiro]

with the next thing, you can say \ex j, next i j /\ ...

[Mario Carneiro]

but depending on what you want to say just plain A.obj (i-1) might be best

[Johan Commelin]

So what is actually the benefit of next? Why can't I just write a condition (h : j = i+1) in the definition of delta?

[Mario Carneiro]

you can

[Mario Carneiro]

but it generalizes to more complicated index structures

[Johan Commelin]

I see...

[Mario Carneiro]

I'm not saying you should necessarily use it here

[Reid Barton]

Another example of this index business is (commutative / graded commutative) graded algebras

[Reid Barton]

where multiplication is a family of operations $m : A_i \times A_j \to A_{i+j}$ and $m$ is supposed to be, say, associative, but stating that depends on the associativity of addition of indices

[Johan Commelin]

@Mario Carneiro Do you know how mathematicians write the predicate is_complex?
They just write A.delta \circ A.delta = 0
Now, I thought I should write \forall i, A.delta i \circ A.delta (i-1) = 0. But you are telling me I need 3 explicit arguments... it will probably take my psyche some time to adjust.

[Johan Commelin]

@Reid Barton Yeah, I was thinking about those a bit. (Because you can of course also do sequences as graded modules with a differential of degree 1.) I really don't know if the A_i should be an indexed family of types or an indexed family of subsets... We will probably need both...

[Sebastien Gouezel]

Mario Carneiro Do you know how mathematicians write the predicate is_complex?
They just write A.delta \circ A.delta = 0

You can also write it in this way in Lean if you think of the total space of your complex as a group/module/whatever (with an additional filtered structure), and A.deltaas a group/module/whatever morphism that, incidentally, happens to respect the filtration.

[Johan Commelin]

Yes, but I fear that will make talking about homogeneous elements a lot more awkward...