Stream: maths

Topic: flexible indices

Johan Commelin (Feb 20 2019 at 09:45):

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 (Feb 20 2019 at 09:45):

What I am after is a nice definition of delta

Johan Commelin (Feb 20 2019 at 09:47):

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 (Feb 20 2019 at 09:51):

Currently this fails:

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


Johan Commelin (Feb 20 2019 at 09:51):

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

Johan Commelin (Feb 20 2019 at 09:59):

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)


(never mind)

Kenny Lau (Feb 20 2019 at 10:03):

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

Johan Commelin (Feb 20 2019 at 10:38):

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

Johan Commelin (Feb 20 2019 at 11:04):

Here is category_theory/instances/groups.lean:

/- Copyright (c) 2018 Johan Commelin. All rights reserved.
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 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 (Feb 20 2019 at 12:23):

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 (Feb 20 2019 at 14:51):

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 (Feb 26 2019 at 12:13):

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 (Feb 26 2019 at 12:14):

Why not use +1 instead of -1?

Mario Carneiro (Feb 26 2019 at 12:14):

it's over all integers

Mario Carneiro (Feb 26 2019 at 12:15):

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 (Feb 26 2019 at 12:15):

But can we make it transparent?

Mario Carneiro (Feb 26 2019 at 12:15):

don't know what you intend to do with this

Johan Commelin (Feb 26 2019 at 12:16):

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 (Feb 26 2019 at 12:16):

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

Mario Carneiro (Feb 26 2019 at 12:17):

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

Mario Carneiro (Feb 26 2019 at 12:17):

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

Johan Commelin (Feb 26 2019 at 12:18):

Hmm, how do I use next?

Johan Commelin (Feb 26 2019 at 12:18):

Should I put that in my definition of delta?

Mario Carneiro (Feb 26 2019 at 12:18):

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


Mario Carneiro (Feb 26 2019 at 12:19):

or are you looking somewhere else?

Aah, ok

Johan Commelin (Feb 26 2019 at 12:23):

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

Johan Commelin (Feb 26 2019 at 12:24):

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

Mario Carneiro (Feb 26 2019 at 12:24):

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 (Feb 26 2019 at 12:25):

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 (Feb 26 2019 at 12:25):

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 (Feb 26 2019 at 12:26):

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

Mario Carneiro (Feb 26 2019 at 12:26):

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

Mario Carneiro (Feb 26 2019 at 12:27):

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


what is {{}}?

Mario Carneiro (Feb 26 2019 at 12:28):

half implicit, too lazy to unicode

Mario Carneiro (Feb 26 2019 at 12:28):

I think it is working ascii notation though

Kenny Lau (Feb 26 2019 at 12:28):

what is half implicit?

Mario Carneiro (Feb 26 2019 at 12:28):

not applied unless you apply an argument after them

Mario Carneiro (Feb 26 2019 at 12:29):

like in the definition of subset

:o

Johan Commelin (Feb 26 2019 at 12:32):

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

Johan Commelin (Feb 26 2019 at 12:33):

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

Mario Carneiro (Feb 26 2019 at 12:33):

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

Ooh, right. Ok.

Johan Commelin (Feb 26 2019 at 12:33):

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

Mario Carneiro (Feb 26 2019 at 12:33):

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

Mario Carneiro (Feb 26 2019 at 12:34):

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

Mario Carneiro (Feb 26 2019 at 12:35):

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 (Feb 26 2019 at 12:35):

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

Mario Carneiro (Feb 26 2019 at 12:35):

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

Johan Commelin (Feb 26 2019 at 12:37):

This will be hard to explain to mathematicians...

Johan Commelin (Feb 26 2019 at 12:37):

Why can't automation help us here?

Mario Carneiro (Feb 26 2019 at 12:38):

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

Johan Commelin (Feb 26 2019 at 12:38):

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

Mario Carneiro (Feb 26 2019 at 12:38):

You want all rewriting and stuff to happen in prop land

Mario Carneiro (Feb 26 2019 at 12:38):

but delta is data, so it needs a general type

Mario Carneiro (Feb 26 2019 at 12:39):

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

Johan Commelin (Feb 26 2019 at 12:44):

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

Patrick Massot (Feb 26 2019 at 12:46):

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 (Feb 26 2019 at 12:47):

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

Patrick Massot (Feb 26 2019 at 12:47):

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 (Feb 26 2019 at 12:47):

I am in favor of both of those

Patrick Massot (Feb 26 2019 at 12:48):

What a nice thesis topic!

Johan Commelin (Feb 26 2019 at 12:49):

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

Johan Commelin (Feb 26 2019 at 12:50):

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

Patrick Massot (Feb 26 2019 at 12:50):

You already have it: the tactic language

Mario Carneiro (Feb 26 2019 at 12:50):

DTT is a horrible assembly language

Mario Carneiro (Feb 26 2019 at 12:51):

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

Mario Carneiro (Feb 26 2019 at 12:51):

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

Johan Commelin (Feb 26 2019 at 12:52):

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

Johan Commelin (Feb 26 2019 at 12:52):

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

Mario Carneiro (Feb 26 2019 at 12:58):

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 (Feb 26 2019 at 13:00):

What do you mean with that last sentence?

Mario Carneiro (Feb 26 2019 at 13:02):

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

Johan Commelin (Feb 26 2019 at 13:22):

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 (Feb 26 2019 at 14:14):

it's an intrinsic DTT issue

Mario Carneiro (Feb 26 2019 at 14:14):

defeq matters, and tactics can't change that

Johan Commelin (Feb 26 2019 at 14:14):

Aah, so Lean will always be fighting its foundations.

Johan Commelin (Feb 26 2019 at 14:17):

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 (Feb 26 2019 at 14:17):

You are hitting surprisingly close to my current research areas

Johan Commelin (Feb 26 2019 at 14:18):

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 (Feb 26 2019 at 14:19):

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

Mario Carneiro (Feb 26 2019 at 14:20):

as you can see lean has 2 out of 3

Mario Carneiro (Feb 26 2019 at 14:21):

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

Johan Commelin (Feb 26 2019 at 14:21):

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

Mario Carneiro (Feb 26 2019 at 14:22):

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

Mario Carneiro (Feb 26 2019 at 14:22):

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

Johan Commelin (Feb 26 2019 at 17:56):

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 (Feb 26 2019 at 18:01):

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

Mario Carneiro (Feb 26 2019 at 18:02):

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

Johan Commelin (Feb 26 2019 at 18:05):

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?

you can

Mario Carneiro (Feb 26 2019 at 18:05):

but it generalizes to more complicated index structures

I see...

Mario Carneiro (Feb 26 2019 at 18:09):

I'm not saying you should necessarily use it here

Reid Barton (Feb 26 2019 at 18:12):

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 (Feb 26 2019 at 18:13):

@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 (Feb 26 2019 at 18:15):

@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 (Feb 26 2019 at 19:15):

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 (Feb 26 2019 at 19:23):

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

Last updated: May 12 2021 at 07:17 UTC