category theory tactics

Stream: maths

[Kevin Buzzard]

What is the tactic which solves goals like

⊢ 𝟙 X ≫ f = f

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

[Kevin Buzzard]

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,
φ : ℱ ⟶ 𝒢
⊢ 𝟙 ℱ ≫ φ = φ

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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 :-)

[Johan Commelin]

Does tidy help?

[Kevin Buzzard]

I could never get it to do anything

[Johan Commelin]

Weird

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

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).

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I'm going straight for sheaves now.

[Reid Barton]

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!

[Kevin Buzzard]

indeed it was!

[Reid Barton]

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

[Kevin Buzzard]

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

[Reid Barton]

Well, up to various sorts of extensionality, yes

[Kevin Buzzard]

yeah yeah yeah

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

You could also try dsimp, simp. Sometimes that helps

[Kevin Buzzard]

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

[Kevin Buzzard]

I live in a world where all exts are defeq.

[Reid Barton]

Oh, you rolled a lot of your own stuff

[Reid Barton]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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?

[Johan Commelin]

Yes, up to defining what a filtered diagram is.