Stream: new members

Topic: Defining a (non-full) subcategory

Jakob Scholbach (Mar 23 2021 at 21:29):

Another category theoretic question: I am trying to construct a (non-full) subcategory whose morphisms have the lifting property with respect to some other subcategory (see around here https://ncatlab.org/nlab/show/lift). What is a convenient syntax to phrase such things? A not-quite-minimal example is posted below, but the question makes sense for any property of morphisms in a category that is stable under composition and holds for the identity morphisms.

import category_theory.category
import category_theory.arrow
import category_theory.functor

namespace category_theory

universes v₁ u₁ u₂ u v
variables {C : Type u₁} [category.{v₁} C]
variables {D : Type u₁} [category.{v₁} D]
variable X : C

/- The left lifting property of a morphism i vs. a morphism p. -/
def llp (i p : arrow C) : Prop := ∀ (sq : i ⟶ p), nonempty (arrow.lift_struct sq)

/- The subcategory of C consisting of those morphisms having the right lifting property with respect to any
morphism in the range of a functor. -/

/- Any identity has the right lifting property with respect to any map. -/
lemma id_has_rlp (i : arrow C) : llp i (arrow.mk (𝟙 X)) :=
begin
sorry
end

def rlp_of_range (I : D ⥤ C) : category.{v₁} C :=
{
hom := λ X Y, { p : X ⟶ Y // ∀ i : arrow D, llp ((functor.map_arrow I).obj i) (arrow.mk p)},
id := λ X, {
sorry, -- want to use id_has_rlp here
},
comp := sorry -- will use a similar stability of the lifting
id_comp' := _,
comp_id' := _,
assoc' := _
}



Johan Commelin (Mar 23 2021 at 21:32):

@Jakob Scholbach you might be interested in https://github.com/rwbarton/lean-homotopy-theory where @Reid Barton develops a whole lot of homotopy theory. However that repo is quite old, and not compatible with current mathlib.

Adam Topaz (Mar 23 2021 at 21:35):

Note that because C already has a category structure in your code, you would want to introduce an alias for C.

Johan Commelin (Mar 23 2021 at 21:36):

To answer question, I would break rlp_of_range into pieces. So

namespace rlp_of_range

def hom ...

def id ...

def comp ...

end rlp_of_range

def rlp_of_range (I : D ⥤ C) : category.{v₁} C :=
{ hom := rlp_of_range.hom,
id := rlp_of_range.id,
comp := rlp_of_range.comp,
id_comp' := _,
comp_id' := _,
assoc' := _ }


Johan Commelin (Mar 23 2021 at 21:36):

At first, this seems very tedious. But in practice it is a lot faster to work this way, because you can take more advantage of the previous steps

Jakob Scholbach (Mar 23 2021 at 21:41):

OK, good - is there some example somewhere in mathlib that has applied this skeleton in this way?

Jakob Scholbach (Mar 23 2021 at 21:42):

It always takes me lots of time to hunt down the syntax to the place where it is actually defined.

Adam Topaz (Mar 23 2021 at 21:44):

import category_theory.isomorphism
import category_theory.functor

namespace category_theory
variables {C D : Type*}
variables [category C] [category D]

def liftable (F : D ⥤ C) := C

variable {F : D ⥤ C}

def liftable.X (x : liftable F) : C := x

instance : category (liftable F) :=
{ hom := λ X Y, { f : X.X ⟶ Y.X // ∀ {a b : D} {g : a ⟶ b} {i : F.obj b ≅ Y.X},
∃ h : F.obj a ⟶ X.X, h ≫ f = F.map g ≫ i.hom},
id := _,
comp := _,
id_comp' := _,
comp_id' := _,
assoc' := _ }

end category_theory


Adam Topaz (Mar 23 2021 at 21:44):

I haven't thought about whether the definition is actually correct, but it typechecks

Adam Topaz (Mar 23 2021 at 21:45):

Note that one should not talk about equality of objects in the category, hence the isomorphism i in the condition

Adam Topaz (Mar 23 2021 at 21:45):

And I agree with Johan's comments that it's probably better to split off the hom, id, comp, etc.

Jakob Scholbach (Mar 24 2021 at 13:10):

A follow up question: given the definition of the hom-sets, identity and composition as below, how do I unwind the definition of the composition that I just made in order to show id_comp' (near the end of the post)?

import category_theory.category
import category_theory.arrow
import category_theory.functor

namespace category_theory

universes v₁ u₁ u₂ u v
variables {C : Type u₁} [category.{v₁} C]
variables {D : Type u₁} [category.{v₁} D]

variables {A B X Y Z : C}

/- The left lifting property of a morphism i vs. a morphism p. -/
def has_lifting_property (i p : arrow C) : Prop := ∀ (sq : i ⟶ p), nonempty (arrow.lift_struct sq)

def liftable (F : D ⥤ arrow C) := C

variable {F : D ⥤ arrow C}

def liftable.X (x : liftable F) : C := x

lemma has_lifting_property_id' (X : C) :  ∀ i : D, has_lifting_property ((F.obj) i) (arrow.mk (𝟙 X)) :=
begin
sorry
end

lemma has_lifting_property_comp' {f : X ⟶ Y} (hf : ∀ i : D, has_lifting_property ((F.obj) i) (arrow.mk f))
{g : Y ⟶ Z} (hg : ∀ i : D, has_lifting_property ((F.obj) i) (arrow.mk g)) :
∀ i : D,  has_lifting_property ((F.obj) i) (arrow.mk (f ≫ g)) :=
begin
sorry
end

/- Given a functor F : D ⥤ arrow C, we construct the (non-full) subcategory of C
spanned by those morphisms that have the right lifting property relative to all maps
of the form F(i), where i is any object in D. -/
instance : category (liftable F) :=
{ hom := λ X Y, { p : X.X ⟶ Y.X // ∀ {i : D},
has_lifting_property ((F.obj) i) (arrow.mk p)},
id := λ X, ⟨ 𝟙 X, has_lifting_property_id' X, ⟩, --λ X, llp_to_id' X,
comp := λ X Y Z f g, ⟨f.val ≫ g.val, has_lifting_property_comp' f.property g.property ⟩,
id_comp' := _, -- how do I unwind the definition of comp with f.val ≫ g.val that I previously made?
comp_id' := _,
assoc' := _ }

end category_theory


Johan Commelin (Mar 24 2021 at 13:11):

I guess I would start with intros, ext, dsimp

Jakob Scholbach (Mar 24 2021 at 13:14):

Thanks! -- Can I get a copy of your lean brain, please?! :)

Adam Topaz (Mar 24 2021 at 13:32):

Tidy should be able to handle that goal, I hope?!

Adam Topaz (Mar 24 2021 at 13:54):

Here's tidy doing all the work :)

import category_theory.category
import category_theory.arrow
import category_theory.functor

namespace category_theory

universes v₁ u₁ u₂ u v
variables {C : Type u₁} [category.{v₁} C]
variables {D : Type u₁} [category.{v₁} D]

variables {A B X Y Z : C}

/- The left lifting property of a morphism i vs. a morphism p. -/
def has_lifting_property (i p : arrow C) : Prop := ∀ (sq : i ⟶ p), nonempty (arrow.lift_struct sq)

structure liftable (F : D ⥤ arrow C) := mk :: (X : C) -- :-)

variable {F : D ⥤ arrow C}

lemma has_lifting_property_id' (X : C) :  ∀ i : D, has_lifting_property ((F.obj) i) (arrow.mk (𝟙 X)) :=
begin
sorry
end

lemma has_lifting_property_comp' {f : X ⟶ Y} (hf : ∀ i : D, has_lifting_property ((F.obj) i) (arrow.mk f))
{g : Y ⟶ Z} (hg : ∀ i : D, has_lifting_property ((F.obj) i) (arrow.mk g)) :
∀ i : D,  has_lifting_property ((F.obj) i) (arrow.mk (f ≫ g)) :=
begin
sorry
end

/- Given a functor F : D ⥤ arrow C, we construct the (non-full) subcategory of C
spanned by those morphisms that have the right lifting property relative to all maps
of the form F(i), where i is any object in D. -/
instance : category (liftable F) :=
{ hom := λ X Y, { p : X.X ⟶ Y.X // ∀ (i : D),
has_lifting_property ((F.obj) i) (arrow.mk p)},
id := λ X, ⟨𝟙 _, has_lifting_property_id' _⟩,
comp := λ X Y Z f g, ⟨f.1 ≫ g.1, has_lifting_property_comp' f.2 g.2⟩ }

end category_theory


Adam Topaz (Mar 24 2021 at 13:56):

When you omit the fields like I did in this code, lean uses what's called the auto_param which is essentially a tactic that it tries in order to close the goal automatically. In this case, it applies tidy, which is able to close the three omitted goals all by itself.

Adam Topaz (Mar 24 2021 at 14:00):

The key trick was to replace the definition of liftable with a structure, so that tidy is able to use cases X

Jakob Scholbach (Mar 24 2021 at 20:46):

Thanks again @Adam Topaz and @Johan Commelin . I somehow did not see this last message and used a slightly more verbose way (but also includingtidy`). I will integrate your simplification there soon. If you are interested, have a look here #6852. I'm sure there will again be many stylistic shortcomings...
My mid-term goal is to define the notion of a model category.

Last updated: May 14 2021 at 04:22 UTC