morphism in `(topological_space.opens X)ᵒᵖ`

Stream: maths

[Kevin Buzzard]

I would have liked to think that I am experienced enough to figure out how to make progress with the following goal in marthlib3:

import tactic
import topology.sets.opens
import category_theory.category.preorder

example (X : Type) [topological_space X] (U V : (topological_space.opens X)ᵒᵖ) (h : V.unop ⊆ U.unop):
  U ⟶ V :=
begin
  -- apply ulift.up, -- fails
  -- change opposite.unop V ⟶ opposite.unop U, -- fails
  delta quiver.hom, --dreaded []
  sorry
end

Getting the system to unfold quiver.hom gives me the dreaded [quiver.hom quiver.opposite] U V and my rule of thumb is that when the []s start appearing you unfolded too much. By using widgets you can dig into what the definition should be and it's

/-- `Vᵒᵖ` reverses the direction of all arrows of `V`. -/
instance opposite {V} [quiver V] : quiver Vᵒᵖ :=
⟨λ a b, (unop b) ⟶ (unop a)⟩

so my change should work but this doesn't work either, I dunno if something was made irreducible or what, but anyway at the end of the day I'm stuck. This is for a lecture I'm giving today in 5 hours lol

[Andrew Yang]

Not tested, but exact (hom_of_le h).op should work?

[Kevin Buzzard]

ha ha I just replaced the goal with _ and clicked on every single lightbulb possibility, and library_search gave me category_theory.op_hom_of_le h

[Kevin Buzzard]

OK now to find out how I should be doing this. Thanks Andrew! Do you have any clue why my approaches didn't work?

[Andrew Yang]

I'm still looking into it, but dsimp [quiver.opposite] seems to leave you with opposite.unop V ⟶ opposite.unop U.

[Andrew Yang]

It seems like quiver.opposite is marked as irreducible to force users into using docs#category_theory.quiver.hom.op

[Joël Riou]

My first try would have been:

  let α : V.unop ⟶ U.unop := sorry,
  exact α.op,

[Adam Topaz]

I think we have docs#has_le.le.hom so you can use dot notation and write h.hom where h : A \le B.

[Adam Topaz]

similarly docs#quiver.hom.le

[Adam Topaz]

So altogether Kevin should be able to write h.hom.op :)

[Andrew Yang]

Not really. Kevin's h is in terms of subset and there isn't a has_subset.subset.hom. But to be fair, Kevin's example should use le to begin with.