Zulip Chat Archive

Stream: new members

Topic: is_iso identity and composition, maximal groupoid


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Alena Gusakov (Jun 28 2020 at 16:50):

Gotcha, I'll change that

view this post on Zulip 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

view this post on Zulip Alena Gusakov (Jun 28 2020 at 16:52):

Does that also apply to the composition stuff?

view this post on Zulip Bhavik Mehta (Jun 28 2020 at 16:53):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Alena Gusakov (Jun 28 2020 at 21:16):

Oh, that makes a lot of sense, thanks

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 28 2020 at 21:19):

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

view this post on Zulip Alena Gusakov (Jun 28 2020 at 21:20):

Oh, oops. Thanks!


Last updated: May 15 2021 at 02:11 UTC