# Zulip Chat Archive

## Stream: new members

### Topic: rewriting and propositional equalities

#### Robin Carlier (Jun 26 2021 at 10:35):

Hey, so I have an hypothesis of the form `f : x \hom y`

, for some x y in a category, now I also have some equalities `h_x : x = foo`

and `h_y: y = bar`

, which are propositional equalities rather than definitional (if I understand that distinction well), so that when I try `rw h_x at f`

I end up with a duplicate of f, of the form `f : stuff \hom y`

, if I try to rewrite again it rewrite on that duplicate as well.

Now I also have an hypothesis `mono f`

, but this one don't get duplicated during my rewritings (if I `dedup`

after the rewritings, I have some `f_1: foo \hom bar`

, but still have `mono f`

but no `mono f_1`

. Is there a way to tell Lean to change hypotheses involving f when rewriting like this?

#### Eric Wieser (Jun 26 2021 at 10:39):

`subst h_x`

may work better

#### Eric Wieser (Jun 26 2021 at 10:40):

Which means roughly "replace x with foo everywhere"

#### Eric Wieser (Jun 26 2021 at 10:41):

Your problem is that there are other hypotheses or a goal whose type depends on f, and when you `rw ... at f`

these terms are not also rewritten

#### Robin Carlier (Jun 26 2021 at 10:45):

Mmh, now that's weird since lean tells me that h_x is not of the form `x = t`

or `t = x`

while it clearly is (at least in my example). Thanks for the command subst, which I did not know before, I think that this new issue has to do with my particular setup so I'll think about it a bit!

#### Robin Carlier (Jun 26 2021 at 10:46):

Mmh alright I see why Lean doesn't like subst in my case, it's because somehow foo depends on x itself

#### Robin Carlier (Jun 26 2021 at 10:47):

foo is basically of the form h^{-1}(h(x)) for some h, so it can't just replace x everywhere without troubles

#### Eric Rodriguez (Jun 26 2021 at 11:01):

may not work in this case, but `subst`

is an option you can sometimes try (and the related `rintro rfl`

, etc)

#### Robin Carlier (Jun 26 2021 at 11:03):

Yeah I'll remember `subst`

anyway, it's quite useful!

#### Robin Carlier (Jun 26 2021 at 11:11):

So, do you think there's a way out of my situation (where foo depends on x)? Basically I have this `f : x \hom y`

, with hyp `mono f`

, and the same theorem I want already proved for `f`

of the form `h(stuff) \hom h(other _stuff)`

, and I simply thought I could say "well just apply it to stuff = h^{-1}(x) and other _stuff = h^{-1}(y)", but runs into problems like this. Sounds like it' just me not really understanding how the lean rewriting works.

#### Eric Rodriguez (Jun 26 2021 at 11:11):

can you make a #mwe that shows an example of what's going on?

#### Robin Carlier (Jun 26 2021 at 11:12):

Yup, I'll try, it'll definitely be more clear.

#### Robin Carlier (Jun 26 2021 at 11:18):

```
import algebraic_topology.simplex_category
universe variables u
open category_theory
namespace simplex_category
namespace epi_mono
localized "notation `[`n`]` := simplex_category.mk n" in simplicial
lemma mono_le_card {n m : ℕ} {f : [n] ⟶ [m]} : (category_theory.mono f) → (n ≤ m) := begin
sorry,
end
lemma mono_le_length {x y : simplex_category} {f : x ⟶ y} : (category_theory.mono f) → (x.len ≤ y.len) := begin
set n := x.len with def_n,
set m := y.len with def_m,
intro h_f_mono,
have x_eq_n : x = [n] := by {rw def_n, exact (mk_len x).symm},
have y_eq_m : y = [m] := by {rw def_m, exact (mk_len y).symm},
-- subst x_eq_n <- does not work
-- type_check @mono_le_card n m f <-- Does not type check since f should be [n] ⟶ [m] rather than x ⟶ y
-- rw x_eq_n at f <- create a duplicate of f, but doesn't get that this dupe will be a mono from h_f_mono.
end
end epi_mono
end simplex_category
```

#### Kevin Buzzard (Jun 26 2021 at 11:33):

Maybe `mono_le_card`

is too weak because it you can only use for objects which are *equal* to `[n]`

and equality is evil in category theory. `mono_le_length`

is the correct thing to prove and probably it should not be deduced from `mono_le_card`

but done directly. It should follow from stuff which ideally would already be in the API, but who knows. You would want to prove that the category is concrete, that the mono is injective on the underlying types, and that the size of the underlying type of `x`

is equal to `x.len`

, and then it will be a fact from the library.

To deduce mono_le_length from mono_le_card I guess I would try to prove that every `x : simplex_category`

was *isomorphic* to some `[n]`

because that is not an evil statement.

Probably any comments from people who know more about category theory and this category in general should be taken more seriously than mine. @Scott Morrison @Reid Barton @Bhavik Mehta @Johan Commelin ?

#### Robin Carlier (Jun 26 2021 at 11:39):

Thanks for your insight. I've already proved that a mono induces an injection on the underlying type, but once again in the case `f`

is from some `[m]`

to some `[n]`

, I agree that the right statement is the one about length but somehow I thought going through the more concrete one first would ease the proof (since one of the nice point of the simplex category is there's no non-identity isos), but since the rewriting isn't that easy, I'll probably do as you suggest.

#### Robin Carlier (Jun 26 2021 at 11:46):

Proving that any `x : simplex_category`

is iso to some `[n]`

shouldn't be too hard from the fact they're equal, hopefully.

#### Kevin Buzzard (Jun 26 2021 at 11:53):

My mental model of category theory is that you should be aware that at any moment the developers might replace a category by an equivalent category, so we can't guarantee that any x is equal to an [n], and the result you want should probably be supplied for you in the simplicial set API. But I might be completely wrong about this

#### Mario Carneiro (Jun 26 2021 at 11:56):

rather than transferring across an equiv, it's usually easier to just modify the original proof to work in the desired generality

#### Mario Carneiro (Jun 26 2021 at 11:57):

that is, prove `mono_le_length`

first and deduce `mono_le_card`

as a consequence

#### Robin Carlier (Jun 26 2021 at 12:01):

I'll do that then!

#### Robin Carlier (Jun 26 2021 at 12:21):

Worked like a charm as you suggested, thanks a lot for the help!

Last updated: Dec 20 2023 at 11:08 UTC