## Stream: new members

### Topic: is_iso identity and composition, maximal groupoid

#### Alena Gusakov (Jun 28 2020 at 16:43):

So I'm trying to prove two things, namely the identity morphism is an isomorphism and composition of isomorphisms is an isomorphism. I'd like to use these proofs to show that the maximal groupoid of C is a subcategory of C.

For identity morphism, looking through isomorphism.lean, there is a statement that proves that identity morphisms are isomorphisms. I'm probably overcomplicating this, but is there a way to prove it in the way I've set it up? Is there even a point to proving it this way?

import category_theory.category -- this transitively imports
-- category_theory.category
-- category_theory.functor
-- category_theory.natural_transformation
import category_theory.isomorphism
import tactic

open category_theory

universes v u

variables (C : Type u) [category.{v} C]

def identity_is_iso {X : C} : is_iso (𝟙 X) :=
begin
have hcomp : 𝟙 X ≫ 𝟙 X = 𝟙 X :=
by {rw [category.id_comp]},
have hinv2 : (𝟙 X) = inv (𝟙 X) :=
by {sorry},
sorry,
end


When it comes to composition of morphisms, I pretty much have the same questions. What I have is really overcomplicating something I think is supposed to be really simple.

import category_theory.category -- this transitively imports
-- category_theory.category
-- category_theory.functor
-- category_theory.natural_transformation
import category_theory.isomorphism
import tactic

open category_theory

universes v u

variables (C : Type u) [category.{v} C]

-- need f.hom ≫ g.hom ≫ g.inv ≫ f.inv = 𝟙 X
def hom_comp_is_iso {X Y Z : C} (f : X ≅ Y) (g : Y ≅ Z) :
is_iso (f.hom ≫ g.hom) :=
begin
have hfx : 𝟙 X = f.hom ≫ f.inv :=
by {sorry},
have hfy : 𝟙 Y = f.inv ≫ f.hom :=
by {sorry},
have hgy : 𝟙 Y = g.hom ≫ g.inv :=
by {sorry},
have hgz : 𝟙 Z = g.inv ≫ g.hom :=
by {sorry},

have hfin1 : 𝟙 X = f.hom ≫ g.hom ≫ g.inv ≫ f.inv :=
calc 𝟙 X = f.hom ≫ f.inv :
by {sorry}
... = f.hom ≫ 𝟙 Y ≫ f.inv :
by {sorry}
... = f.hom ≫ g.hom ≫ g.inv ≫ f.inv :
by {sorry},
sorry,
end
-- incredibly inefficient. not even gonna bother with this.
-- figure out how to rephrase.


Also, are these definitions good to use in proving that the maximal groupoid is a subcategory? Is there another way I should be phrasing things? I want to be able to explicitly see what's going on because I'm still getting used to Lean syntax. It seems like there's a proof of Groupoid.{v u} being large_category.{max v u}, but I don't really see why a groupoid must necessarily be a large category. Unless I'm misunderstanding, should there be some way of proving groupoids are just categories, not necessarily large/small?

#### Alena Gusakov (Jun 28 2020 at 16:50):

Oops, looks like I was using out-of-date syntax for this stuff, don't know if that changes things much

#### Bhavik Mehta (Jun 28 2020 at 16:50):

There was a patch some time ago which means you don't need to explicitly name and include the category instance

#### Alena Gusakov (Jun 28 2020 at 16:50):

Gotcha, I'll change that

#### Bhavik Mehta (Jun 28 2020 at 16:51):

Also for the identity iso stuff, I think you are overcomplicating it a bit. In particular, notice that is_iso is a class with three fields, to construct the fact that it's an iso you just need to supply those three fields - you can get their names by doing {!!} (instead of begin/end) and the lightbulb will have an option about a skeleton

#### Alena Gusakov (Jun 28 2020 at 16:52):

Does that also apply to the composition stuff?

#### Bhavik Mehta (Jun 28 2020 at 16:53):

Yeah, it applies to basically anything where you want to prove is_iso directly

#### Alena Gusakov (Jun 28 2020 at 16:54):

Okay, good to know. Thanks! I might come back into this thread later once I rewrite stuff if things aren't working still

#### Bhavik Mehta (Jun 28 2020 at 17:28):

On your Groupoid thing, Groupoid is actually the category of groupoids, so it should be a large category. I think you want groupoid, which is the type of a groupoid

#### Alena Gusakov (Jun 28 2020 at 21:16):

Oh, that makes a lot of sense, thanks

#### Alena Gusakov (Jun 28 2020 at 21:18):

I figured out identity_is_iso but I can't seem to get the composition one - maybe my syntax is off?

import category_theory.category -- this transitively imports
-- category_theory.category
-- category_theory.functor
-- category_theory.natural_transformation
import category_theory.isomorphism
import tactic

open category_theory

universes v u

variables (C : Type u) [category.{v} C]

-- need f.hom ≫ g.hom ≫ g.inv ≫ f.inv = 𝟙 X and vice versa
def iso_comp_is_iso {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [is_iso f] [is_iso g] :
is_iso (f ≫ g) :=
{ inv := (inv g ≫ inv f),
hom_inv_id' := (f ≫ g) ≫ (inv g ≫ inv f) = 𝟙 X--by rw [category.assoc ] sorry,--is_iso.hom_inv_id' g],
inv_hom_id' := _}
end


#### Alena Gusakov (Jun 28 2020 at 21:18):

The error I'm getting is at the equals sign before 𝟙 X and it looks like

type mismatch at field 'hom_inv_id''
(f ≫ g) ≫ inv g ≫ inv f = ⁇
has type
Prop : Type
but is expected to have type
auto_param ((f ≫ g) ≫ inv g ≫ inv f = 𝟙 X) (name.mk_string "obviously" name.anonymous) : Prop


#### Reid Barton (Jun 28 2020 at 21:19):

You put what you need to prove where you were supposed to put a proof.

#### Alena Gusakov (Jun 28 2020 at 21:20):

Oh, oops. Thanks!

Last updated: May 15 2021 at 02:11 UTC