How to coerce Quiver.Hom into FunLike in FullSubcategory

Stream: new members

[Javier Lopez-Contreras]

Halo!

I am working with FullSubcategory and I am not sure how to recover normal arrows from categorical arrows. I've condensed the doubt in the following minimal example, do you know how the "coe" in the FunLike should be filled?

Thanks!

import Mathlib

open CategoryTheory

def 𝓒 := FullSubcategory (fun (A : CommRingCat) ↦ True)

instance : Category 𝓒 := by unfold 𝓒; infer_instance
instance : CoeOut 𝓒 CommRingCat where coe A := A.obj

instance (A B : 𝓒) : FunLike (A ⟶ B) A B where
  coe := sorry
  coe_injective' := sorry

[Yaël Dillies]

coe f := (f : A.obj \hom B.obj) should work, see docs#CategoryTheory.InducedCategory.category

[Javier Lopez-Contreras]

Maybe I'm missing something, but I think this is not working for me : https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQOJgCmAdnAMIqEDm0AngCqqF14AmhAZnIKwbgSztwAuALxwAYgFd06AMrisAY0o0otOAAoO40moCCg8hBAgASsGJUKMAJRxAZYRx6UcYSt4zAZxhJi8wvsvUdDz8wnBYqlocEOiswQDccGYchFAA+h5ePoQ4Gd6+/hCEAPLi8HwGRqbmlnAA7kxQfvKFcHqhOgB0EFgAVm7Ennl+unAAQvp8NgJiWgAywADWw3qAb+RjNnrj9SnZcHDNflyhGvqd3T1wa6Ndva57B+nEPYTyMMAAboQA5IIi7tAqHBAA

[Javier Lopez-Contreras]

Oh, adding \u works now! https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQOJgCmAdnAMIqEDm0AngCqqF14AmhAZnIKwbgSztwAuALxwAYgFd06AMrisAY0o0otOAAoO40moCCg8hBAgASsGJUKMAJRxAZYRx6UcYSt4zAZxhJi8wvsvUdDz8wnBYqlocEOiswQDccGYchFAA+h5ePoQ4Gd6+/hCEAPLi8HwGRqbmlnAA7kxQfvKFcHqhOgB0EFgAVm7Ennl+unAAQvp8NgJiWgAywADWw3qAb+RjNnrj9SnZcHDNflyhGvqAiYSd3T1wa6ejXb2uewfpxD2E8jDAAG6EAOSCInc0BUOCAA

[Javier Lopez-Contreras]

Thank you @Yaël Dillies !

[Yaël Dillies]

Alternatively, provide the instance as inferInstanceAs <| FunLike (A.obj \hom B obj) _ _

[Javier Lopez-Contreras]

So it worked for the minimal example, but I am not being able to make it work for the real example (code bellow). I think it has to do with CategoryTheory Under having no instance of ConcreteCategory (the one I added is sorried)

import Mathlib

open CategoryTheory

universe u v

instance Under.instConcreteCategory {C : Type u} [CategoryTheory.Category.{v, u} C]
    {X : C} [ConcreteCategory C] :
    ConcreteCategory (CategoryTheory.Under X) := sorry

variable (𝓞 : Type*) [CommRing 𝓞]

def CommAlgCat := Under (CommRingCat.of 𝓞)

instance : Category (CommAlgCat 𝓞) := by unfold CommAlgCat; infer_instance

instance : ConcreteCategory (CommAlgCat 𝓞) := by unfold CommAlgCat; infer_instance

instance : CoeSort (CommAlgCat 𝓞) (Type _) where coe A := A.right

instance (A B : CommAlgCat 𝓞) : CoeFun (A ⟶ B) fun _ ↦ (A → B) :=
  sorry

variable (A : CommAlgCat 𝓞)

instance : Algebra 𝓞 A := A.hom.toAlgebra

instance (A B : CommAlgCat 𝓞) : FunLike (A ⟶ B) A B where
  coe f := sorry
  coe_injective' := sorry

instance (A B : CommAlgCat 𝓞) : AlgHomClass (A ⟶ B) 𝓞 A B where
  map_mul := sorry
  map_one := sorry
  map_add := sorry
  map_zero := sorry
  commutes := sorry

[Javier Lopez-Contreras]

#mathlib4 > Concrete category class redesign This seems relevant (reading it now)

[Javier Lopez-Contreras]

I am not sure how to solve this, but it's clear that it was just recently changed (and, depending on the version of mathlib you are on, somethings work or not). If someone knows how to complete the sorries above, it will be very appreciated!

[Anne Baanen]

Indeed, concrete categories are in a state of flux right now. Basically, we currently have a class HasForget that used to be the basis for the FunLike instances, but I want to switch it to a new ConcreteCategory class. Right now we still have lots of HasForget instances that should become ConcreteCategory in the future.

But right now I can't find a HasForget (CategoryTheory.Under X) instance either though, and I'm not sure how intentional that is.

[Anne Baanen]

I suppose a ConcreteCategory instance for Under would end up looking something like:

instance Subtype.instFunLike {F : Type*} {X Y} [DFunLike F X Y] (P : F → Prop) :
    DFunLike (Subtype P) X Y where
  coe f := f
  coe_injective' _ _ h := Subtype.coe_injective (DFunLike.coe_injective h)

instance Under.instConcreteCategory {C : Type u} [CategoryTheory.Category.{v, u} C]
    {FC : C → C → Type*} {CC : C → Type*} [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)]
    {X : C} [ConcreteCategory C FC] :
    ConcreteCategory (CategoryTheory.Under X) fun X Y => {f : FC X.right Y.right | ∀ x, f (X.hom x) = Y.hom x} where
  hom f := ⟨ConcreteCategory.hom f.right, sorry⟩
  ofHom f := Under.homMk (ConcreteCategory.ofHom f) (w := sorry)

[Javier Lopez-Contreras]

Sounds good, thanks! I think this is what I needed