## 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