Defining a (non-full) subcategory

Stream: new members

[Jakob Scholbach]

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]

@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]

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

[Johan Commelin]

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]

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]

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

[Jakob Scholbach]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Jakob Scholbach]

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]

I guess I would start with intros, ext, dsimp

[Jakob Scholbach]

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

[Adam Topaz]

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

[Adam Topaz]

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]

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]

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

[Jakob Scholbach]

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.