Zulip Chat Archive

Stream: maths

Topic: category theory tactics


view this post on Zulip Kevin Buzzard (Dec 16 2019 at 14:24):

What is the tactic which solves goals like

⊢ 𝟙 X ≫ f = f

or the assertion that composition of morphisms in a category is associative?

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 14:31):

Oh it's more universe issues :-/

type mismatch at application
  category.id_comp C φ
term
  φ
has type
  ℱ ⟶ 𝒢 : Type (max v w)
but is expected to have type
  ?m_1 ⟶ ?m_2 : Type v
state:
C : Type u,
𝒞 : category C,
X : Type w,
_inst_1 : topological_space X,
ℱ 𝒢 : presheaf X C,
φ : ℱ ⟶ 𝒢
⊢ 𝟙 ℱ ≫ φ = φ

view this post on Zulip Johan Commelin (Dec 16 2019 at 14:47):

@Kevin Buzzard φ is not a morphism in C, right? So shouldn't that be category.id_comp _ φ, where _ = presheaf X C?

view this post on Zulip Johan Commelin (Dec 16 2019 at 14:47):

Also, usually simp will solve this, and hence so does tidy.

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 15:00):

I've had a great day so far slowly but surely doing this. I haven't got anywhere yet, but the notation is coming out well at least. I don't understand how to get automation to work, it's like when I was a beginner and I'd just try simp and then cc and then I'd ask Mario or Kenny and get a direct answer in ten seconds flat :-)

view this post on Zulip Johan Commelin (Dec 16 2019 at 15:06):

Does tidy help?

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 15:06):

I could never get it to do anything

view this post on Zulip Johan Commelin (Dec 16 2019 at 15:06):

Weird

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 15:06):

it would just take all the terms apart; I was trying to be really strict with notation, using notation natural for a mathematician.

view this post on Zulip Johan Commelin (Dec 16 2019 at 15:07):

This looks very tidyable to me: https://github.com/ramonfmir/lean-scheme/commit/5f5072a8c050dd3f4ca71841cbb69c66e60b2e77#diff-62dda0355159ecad2596c2c93999a2b8R137-R151

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 15:10):

tidy just turns the goal from

𝟙 U ≫ f = f

into

⊢ (𝟙 U ≫ f).map ⟨x_val, x_property⟩ = f.map ⟨x_val, x_property⟩

I am at the point where I am still proving the axioms for a category (presheaf X C), but there is another category kicking around (namely C).

view this post on Zulip Johan Commelin (Dec 16 2019 at 15:15):

Right, but 𝟙 U ≫ f lives in this other category, doesn't it?

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 15:20):

No, f is a morphism in the presheaf category, so we do need to take it apart I guess.

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 15:21):

I'd like to hear some automation tips before I embark on presheaves on a basis!

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 15:21):

I'm going straight for sheaves now.

view this post on Zulip Reid Barton (Dec 16 2019 at 16:17):

I am at the point where I am still proving the axioms for a category (presheaf X C), but there is another category kicking around (namely C).

aha, a trick question!

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 16:20):

indeed it was!

view this post on Zulip Reid Barton (Dec 16 2019 at 16:20):

simp can fail on a goal like 𝟙 X ≫ f for various reasons, but "because we're in the middle of defining the category instance" was not one I had considered

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 16:21):

but when you unravel it all it's just an instance of the same theorem one level down

view this post on Zulip Reid Barton (Dec 16 2019 at 16:22):

Well, up to various sorts of extensionality, yes

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 16:22):

yeah yeah yeah

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 16:22):

simp couldn't do ⊢ ⇑(𝟙 X_1 ≫ f) x = ⇑f x

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 16:23):

but apply category.id_comp, does it fine. That's one of my favourite uses of the apply tactic.

view this post on Zulip Reid Barton (Dec 16 2019 at 16:23):

You could also try dsimp, simp. Sometimes that helps

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 16:24):

I'm just not sure if I'm supposed to be happy with getting my hands dirty like this.

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 16:24):

I live in a world where all exts are defeq.

view this post on Zulip Reid Barton (Dec 16 2019 at 16:26):

Oh, you rolled a lot of your own stuff

view this post on Zulip Reid Barton (Dec 16 2019 at 16:31):

If you replace the whole proof of id_comp' by begin tidy, end how does it get stuck?

view this post on Zulip Kevin Buzzard (Dec 17 2019 at 01:30):

⊢ (𝟙 X_1 ≫ f).map ⟨x_val, x_property⟩ = f.map ⟨x_val, x_property⟩

view this post on Zulip Kevin Buzzard (Dec 17 2019 at 01:31):

I want to assume that my category has all filtered colimits (but not necessarily all colimits). Can this be done easily given the current state of mathlib?

view this post on Zulip Johan Commelin (Dec 17 2019 at 05:30):

Yes, up to defining what a filtered diagram is.


Last updated: May 14 2021 at 19:21 UTC