# Zulip Chat Archive

## 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