is_iso identity and composition, maximal groupoid

Stream: new members

[Alena Gusakov]

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]

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

[Bhavik Mehta]

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

[Alena Gusakov]

Gotcha, I'll change that

[Bhavik Mehta]

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]

Does that also apply to the composition stuff?

[Bhavik Mehta]

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

[Alena Gusakov]

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]

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]

Oh, that makes a lot of sense, thanks

[Alena Gusakov]

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]

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]

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

[Alena Gusakov]

Oh, oops. Thanks!