naming

Stream: maths

[Robin Carlier]

What would be a meaningful name for this? I'm quite dissatisfied with this one but I feel like iso_of_whisker_left_L_counit would be way to long.

def iso_of_L_counit [is_iso (adjunction.unit h)] : (L ⋙ R ⋙ L) ≅ L :=
{ hom := ⟨(whisker_left L h.counit).app, (whisker_left L h.counit).naturality⟩,
  inv := ⟨(whisker_right h.unit L).app, (whisker_right h.unit L).naturality⟩,
  hom_inv_id' :=
  begin
    ext x, dsimp,
    rw [comp_hom_eq_id, ←hom_comp_eq_id],
    simpa [adjunction.right_triangle, functor.id_obj],
  end,
  inv_hom_id' :=
  begin
    ext x, dsimp,
    simp [adjunction.right_triangle, functor.id_obj],
  end}

[Robin Carlier]

Also lean does not accept whisker_left L h.counitdirectly for hom and similarly for invn since it expects some L ⋙ 𝟙 D instead of L, and does not accept a cast, but I feel weird having that being sort of redundant in the definition, is there a third way?

[Robin Carlier]

import category_theory.adjunction.basic

open category_theory

namespace category_theory
universes v₁ v₂ u₁ u₂

variables {C : Type u₁} [category.{v₁} C]
variables {D : Type u₂} [category.{v₂} D]
variables {L : C ⥤ D} {R : D ⥤ C} (h : L ⊣ R)


def iso_of_L_counit [is_iso (adjunction.unit h)] : (L ⋙ R ⋙ L) ≅ L :=
{ hom := ⟨(whisker_left L h.counit).app, (whisker_left L h.counit).naturality⟩,
  inv := ⟨(whisker_right h.unit L).app, (whisker_right h.unit L).naturality⟩,
  hom_inv_id' :=
  begin
    ext x, dsimp,
    rw [comp_hom_eq_id, ←hom_comp_eq_id],
    simpa [adjunction.right_triangle, functor.id_obj],
  end,
  inv_hom_id' :=
  begin
    ext x, dsimp,
    simp [adjunction.right_triangle, functor.id_obj],
  end }

end category_theory

for a MWE of it not accepting the right type, but I guess it's minor.

[Floris van Doorn]

Not sure about the name, but can you define it as something like (whisker_left L h.counit).trans L.comp_id?
And if it's that short, maybe it doesn't need a separate declaration? (But maybe it's still useful.)

[Floris van Doorn]

If you want it as a separate declaration, I would formulate it as something like

def comp_iso_of_iso_id (e : F ≅ 𝟙 D) : G ⋙ F ≅ G := ...

[Robin Carlier]

Mmh, Lean doesn't like (whisker_left L h.counit).trans L.comp_id, says invalid field notation, 'trans' is not a valid "field" because environment does not contain 'quiver.hom.trans
whisker_left L h.counit`

The def is (I think) useful to have since I use a few times this structure of iso and the explicit inverse given in this definition in other proofs, so I thought than rather reproving each times that the inverse is given by ... I'd just add a definition.
I feel like the comp_iso_of_iso_id would fit in category_theory/natural_isomorphism or something

[Robin Carlier]

But I see your idea using some trans, I'll try to see if there's a way to make something like this work

[Robin Carlier]

Mmh so (whisker_left L h.counit) ≫ (eq_to_iso L.comp_id).hom but I'm not sure this is a better solution, because eq_to_iso seems to add a lot of stuff

[Robin Carlier]

it turns some lemmas like lemma iso_of_L_counit_hom_app [is_iso (adjunction.unit h)] {X : C} : ((iso_of_L_counit h).hom.app X) = (whisker_left L h.counit).app X as stuff to prove, while it was just refl before the change, so I think I'll stick to the inelegant stuff in the definition so that this remains obvious

[Kevin Buzzard]

refl is not always the best proof

[Robin Carlier]

So you'd say it's better to have the (whisker_left L h.counit) ≫ (eq_to_iso L.comp_id).hom definition and have the simp lemmas, rather than going for the shorter variant where I just put the other definition, tag it as reducible so that I don't even have to put the simp lemmas?

[Kevin Buzzard]

Oh I don't have a clue :-) I'm just remarking that sometimes a refl proof can take 10 seconds or more in this part of the library

[Kevin Buzzard]

sometimes a refl proof is replaced by a longer quicker one

[Bhavik Mehta]

It looks to me like this should just be some composition of docs#category_theory.iso_whisker_left and docs#category_theory.functor.left_unitor, possibly with some left replaced with right

[Robin Carlier]

Alright I was missing the unitor part.
I agree that this should be this composite, but won't that produce just some abstract inverse for this iso? The point was kind of that the inverse is explicit, rather than given as inv h.unit.app L.obj X or stuff like this

[Robin Carlier]

I mean I guess I could define it as this composition and then prove the inverse is what I want

[Bhavik Mehta]

Robin Carlier said:

I mean I guess I could define it as this composition and then prove the inverse is what I want

Yeah this is the idea behind is_iso being a Prop: no applications of inv will be definitionally what you want

[Robin Carlier]

Mmh, so design-wise you'd say it'd be better to follow this route? Really I'm just putting this definition because I need twice in a row that the inverse is this, and wanted to have a record of it so that I have some simp available, I don't know if it's worth all the trouble of giving the "right definition" and putting this lemma afterward