delate lambda in tatic state

Stream: general

[orlando]

Hello, i have a tatic state of the form :

((Y < π1> | Y < π2>) ≫ λ (g : (Y ⟶ A) ⨯ (Y ⟶ B)), π1 g | π2 g) g = 𝟙 Y⟦(A ⨯ B)⟧ g

Is it possible to remove the lambda ? To have something like :

(Y < π1> | Y < π2>) ≫ (π1 g | π2 g) =  𝟙 Y⟦(A ⨯ B)⟧ g

i.e reduce the \lambda , i thinck it's the name of the operation ?
Thx

[Patrick Massot]

dsimp only

[Patrick Massot]

But really we should have a beta_reduce tactic.

[Kevin Buzzard]

I usually just type dsimp to do this. dsimp only what?

[orlando]

Ok so the operation that i want is named beta reduction :
with dsimp,
(π1 ((Y < π1> | Y < π2>) g) | π2 ((Y < π1> | Y < π2>) g)) = g

nice !

[Reid Barton]

dsimp only []

[orlando]

no dsimp only and dsimp only [], fail but dsimp transform my expression !

[orlando]

my code is a little too long to put here

[Kevin Buzzard]

Maybe you could find out what's going on with squeeze_simp

[Kevin Buzzard]

dsimp means something like "use only the simp lemmas whose proof is rfl"

[Reid Barton]

But you don't actually have a lambda applied to something, do you?

[Reid Barton]

The reverse category composition order makes everything hard to read :frown:

[Kevin Buzzard]

Scott thinks exactly the opposite.

[Kevin Buzzard]

Users may like to add `f ⊚ g` for composition in the standard convention, using
```lean
local notation f ` ⊚ `:80 g:80 := category.comp g f    -- type as \oo
```

[Reid Barton]

Yeah but Scott doesn't actually write any proofs...?

[Reid Barton]

because everything is supposed to be by obviously

[Patrick Massot]

He worked hard on tidy to avoid that.

[Kevin Buzzard]

he writes things which mathematicians would call proofs, but which turn out to be definitions.

[Reid Barton]

but in the real world, it's hard

[orlando]

The first expression is :
((Y < π1> | Y < π2>) ≫ λ (g : (Y ⟶ A) ⨯ (Y ⟶ B)), π1 g | π2 g) g = 𝟙 Y⟦(A ⨯ B)⟧ g

so it's the left hand, a ≫ (\lambda b, f b) b i thinck it's equal a ≫ f b

[Reid Barton]

I still don't understand Scott's position on the order of composition really

[Patrick Massot]

This is category theory, homs are not meant to be applied.

[Kevin Buzzard]

@orlando just imagine maps on the right :-)

[Kevin Buzzard]

$(x)f$

[Kevin Buzzard]

then it all makes sense

[Reid Barton]

It's really (a ≫ (\lambda b, f b)) b = (\lambda b, f b) (a b) = f (a b)

[Reid Barton]

and this is awful

[Patrick Massot]

This is because you are applying homs to elements of the object, which is utterly bad taste for category theory minded people.

[Reid Barton]

Not really, because everything is really a set by Yoneda.

[Kevin Buzzard]

(a ≫ (\lambda b, f b)) b = (a ≫ f) b

[Kenny Lau]

sad CCC noises

[Reid Barton]

I think I've only seen one category theory paper ever that uses the ≫ direction

[orlando]

hum ok @Kevin Buzzard !

[orlando]

@Reid Barton : i thinck it's not too bad notation, when you make diagram that clear !

[Reid Barton]

I wonder whether it's feasible now to move ∘ to a class

[Johan Commelin]

Sounds like a nice idea

[Reid Barton]

or, it might be a disaster :slight_smile:

[Scott Morrison]

I'm sorry about ≫! I was converted when I wanted to think about categories enriched in braided categories (for modelling domain walls of 3d topological phases), and composition really is a map hom(a,b) \otimes hom(b,c) \to hom(a,c), and unless you assume your braiding is symmetric, thus throwing out the nice examples, you just can't write it the other way. But this is absolutely no excuse for inflicting it on anyone else --- just the story of how I got there...

[Reid Barton]

but I don't think ∘ is used that frequently elsewhere anyways

[Kevin Buzzard]

I got used to it. For me it's helpful having it Scott's way around because when I'm staring at a commutative diagram and wanting to translate the assertion that it commutes into Lean I don't have to read everything backwards.

[David Wärn]

Do we have notation for reversed function application? Something like x £ f := f x

[Kevin Buzzard]

\mapsfrom

[Kevin Buzzard]

no that's something slightly different I guess. How about \gg again?

[Andrew Ashworth]

isn't it $<?

[Andrew Ashworth]

but we actually want |> in the future, but it's in core

[Robin Carlier]

I think McLane writes stuff in the >> direction in Sheaves in Geometry and Logic

[Kevin Buzzard]

Or geology and logic, as it's called in the topos repo

[Reid Barton]

I had amazon show me a random page from this book and it happened to give the definition of category, and there it's clear that composition is written in the usual order.

[Reid Barton]

p. 10

[Reid Barton]

I think in this subject in particular it's nearly impossible to use the reverse order consistently, because all the objects being considered are closely related to sets and categories and one wants to write $(FG)X = FGX = F(GX)$.

[Reid Barton]

That is, impossible unless one also writes function application on the other side, which is what the one paper I've seen use this convention also tries to do, but then it gets a bit weird to write things like Sub(X) or Hom(X, Y) which look like function applications with the usual order

[Robin Carlier]

So I just checked, and yeah, my bad on this one. I had that mistaken with some other weird convention the book has about applying a contravariant on a morphism. Anyway, it's not important.

@Kevin Buzzard You're mentioning a topos repo, I'm quite new to lean and I wanted to do some toposy-category-y stuff for fun with it, do you have a link to the repo or is it private at this point?

[Reid Barton]

https://github.com/b-mehta/topos

[Robin Carlier]

Thank you!

[Bhavik Mehta]

@Robin Carlier I'm currently taking a little break from adding stuff to that repo and making a bunch of PRs to mathlib instead - if there's anything in particular you'd like to work on in there (especially from the issues and coming soon list) let me know, or if you have any questions about it! :)

[Robin Carlier]

Ok! for now I think I will just play around with what have been done so far. However I see that the fact that any presheaf is a colimit of representable is an open issue on the repo, I might be interested in doing that later on, when I'm confident enough with lean ;)
(actually, I installed lean because I thought "hey proving co-yoneda might be a cool challenge", so it's quite a nice coincidence)

[orlando]

there is a version of co / Yoneda in mathlib inthe repertory "category_theory" perhaps it can help you !

[Bhavik Mehta]

Yes, that's a great idea! I really like the proof given in Geology and Logic (I.5, Proposition 1) in particular using the result in Theorem 2 which is useful in other contexts so I'd like to have it in the repo (and eventually in mathlib) - but of course I'd be more than happy with an alternate proof too!

[Bhavik Mehta]

Robin Carlier said:

I think McLane writes stuff in the >> direction in Sheaves in Geometry and Logic

I don't think so - at least not in the edition I have

[Robin Carlier]

Yeah no I had that mistaken for its notation $x \cdot f$ for $P(f)(x)$ where $P$ is a presheaf

I agree with you that Th 2 is the good stuff (and to me it's the really important point, the fact that you get an adjoint pair gives sooo many nice constructions), and I was intending to do it this way.
For now I'll read a bit how things are proved in the category_theory package and in the repo to get a grasp of how things are done (I'm just fresh out of reading "Theorem Proving in Lean" and playing the natural numbers game, so I still have to get a bit more used to lean syntax/all the nice tactics around)

[Bhavik Mehta]

Robin Carlier said:

all the nice tactics around

On this note, if there's any tactics you think would be useful for category theory, definitely start a thread for it!

[orlando]

@Bhavik Mehta @Robin Carlier

A question i do a little exercice : Traduction of group structure on objet of a category with product and terminal objet. And Show that this give a structure of group on Yoneda functor. There is 3 files : here group_objet.lean sugar_yoneda.lean
to_product.lean

1. My proof is horrible cause i don't know good theorem on category perhaps.
2. Do you have a cool proof of this fact : see here for definition ? Without big calculus like me :sweat_smile:
3. Yesterday i try to make, group action of group object on a objet. And I asked myself the question: is there an automatic translation of the axioms of algebraics structure, For example, how to write the ring object axioms in a category ?

Is it topos theory behind ?

[orlando]

I don't make functoriality for the moment !