## Stream: new members

### Topic: Trouble with composition of maps for a functor over a preord

#### Rémi Bottinelli (Aug 03 2022 at 18:35):

I'm not sure how to describe my problem. I'm trying to construct, given an inverse system of types, the subsystem consisting of the "surjective" parts here and I'm having trouble showing what should be obvious, or so I thought. What am I doing wrong here?
To be a bit more precise, at some point I have the goal

F.map (op_hom_of_le _) (F.map (op_hom_of_le lk) y) = F.map (op_hom_of_le kj) (F.map (op_hom_of_le lk) y)


where I would swear the _ should be a shorthand for op_hom_of_le kj, thus making the goal trivial. I can't pinpoint the reason it isn't the case, and I didn't figure out how to ask lean to tell me what exactly should be at the _.
Ah, I might as well paste the whole goal context:

J : Type u,
_inst_1 : preorder J,
_inst_2 : is_directed J has_le.le,
F : Jᵒᵖ ⥤ Type v,
bigger : Jᵒᵖ → set Jᵒᵖ := λ (j : Jᵒᵖ), {i : Jᵒᵖ | opposite.unop j ≤ opposite.unop i},
Fsur_obj : Π (j : Jᵒᵖ), set (F.obj j) :=
λ (j : Jᵒᵖ), ⋂ (i : ↥(bigger j)), set.range (F.map (op_hom_of_le _)),
i j : Jᵒᵖ,
hij : i ⟶ j,
k : Jᵒᵖ,
kj : k ∈ bigger j,
kj : opposite.unop j ≤ opposite.unop k,
l' : J,
lk' : opposite.unop k ≤ l',
li' : opposite.unop i ≤ l',
l : Jᵒᵖ := opposite.op l',
lk : opposite.unop k ≤ opposite.unop l,
li : opposite.unop i ≤ opposite.unop l,
hlk : l ⟶ k := op_hom_of_le lk,
hli : l ⟶ i := op_hom_of_le li,
hkj : k ⟶ j := op_hom_of_le kj,
y : F.obj ↑⟨l, li⟩,
h : ∀ (i_1 : ↥(bigger i)), ∃ (y_1 : F.obj ↑i_1), F.map (op_hom_of_le _) y_1 = F.map (op_hom_of_le _) y
⊢ F.map (op_hom_of_le _) (F.map (op_hom_of_le lk) y) = F.map (op_hom_of_le kj) (F.map (op_hom_of_le lk) y)


#### Andrew Yang (Aug 03 2022 at 18:44):

rw [← functor_to_types.map_comp_apply, ← functor_to_types.map_comp_apply],
refl


solves the particular goal you described.

#### Andrew Yang (Aug 03 2022 at 18:44):

Or even a single refl suffices if I am not mistaken.

#### Rémi Bottinelli (Aug 03 2022 at 18:48):

Huh, it's very confusing, I tried things very close to that. So my intuition was correct? that is, the underscore really was op_hom_of_le kj?

#### Andrew Yang (Aug 03 2022 at 18:53):

You can click on the _ in the info view to see the hidden term. In this case it is subtype.prop ⟨k, kj⟩ which is definitionally equal to kj, but not syntactically equal, so dsimp did not close the goal for you.

In fact, due to proof irrelavence, two Props are defeq whenever they have the same type, so it doesn't even matter what the term is (and hence it is hidden in the infoview).

#### Rémi Bottinelli (Aug 03 2022 at 18:56):

OK, that does match my intuition, thanks a lot! So, what I did wrong was essentially to not try for refl early enough, since I _did_ have defeq terms?

#### Andrew Yang (Aug 03 2022 at 19:14):

Probably yes. It never hurts to try refl.
This is how I would approach subfunctor:

{ rintro i j hij,
rintro x h s ⟨⟨k, _⟩, rfl⟩,
obtain ⟨l,lk,li⟩ := directed_of (≤) k.unop i.unop,
rw set.mem_Inter at h,
obtain ⟨y,rfl⟩ := h ⟨opposite.op l, li⟩,
use F.map (hom_of_le lk).op y,
rw [← functor_to_types.map_comp_apply, ← functor_to_types.map_comp_apply],
refl },


#### Rémi Bottinelli (Aug 04 2022 at 06:25):

I'm also wondering: The following doesn't typecheck. That's because of the lifting involved in the instantiation of J as a category, am I right?

example {J : Type u} [preorder J] (i j : Jᵒᵖ) (m n : i ⟶ j) : m = n, by reflexivity


And the following does typecheck:

example {J : Type u} [preorder J] (i j : Jᵒᵖ) (m n : i ⟶ j) : m ≫ (𝟙 j) = n ≫ (𝟙 j) := rfl


becauses it forces the passage through a Prop. That's fun

Last updated: Dec 20 2023 at 11:08 UTC