diamond in CommAlgCat

Stream: mathlib4

[Michał Mrugała]

I'm trying to prove that a commutative Hopf algebra over R : CommRingCat defines an instance of a group object in (Under R)ᵒᵖ, but I consistently run into an issue with type class inference. To illustrate the issue let's try defining the multiplication morphism:

open CategoryTheory Opposite

variable {R : CommRingCat} {A : Type*} [CommRing A] [HopfAlgebra R A]

noncomputable instance : Grp_Class <| op <| CommRingCat.mkUnder R A where
  one := op <| (Bialgebra.counitAlgHom R A).toUnder
  mul := op <| by
    change R.mkUnder A ⟶ R.mkUnder _
    simp
    /-
    ⊢ R.mkUnder A ⟶ R.mkUnder (TensorProduct ↑R ↑(R.mkUnder A).right ↑(R.mkUnder A).right)
    -/
    refine (Bialgebra.comulAlgHom R A).toUnder
    sorry
  one_mul' := sorry
  mul_one' := sorry
  mul_assoc' := sorry
  inv := sorry
  left_inv' := sorry
  right_inv' := sorry

The refine fails due to a mismatch of the inferred typeclasses between Bialgebra.toAlgebra and (CommRingCat.instAlgebraCarrierRightDiscretePUnit (R.mkUnder A)). This can be solved by using the following:

noncomputable instance : Grp_Class <| op <| CommRingCat.mkUnder R A where
  one := op <| (Bialgebra.counitAlgHom R A).toUnder
  mul := op <| by
    refine (Bialgebra.comulAlgHom R A).toUnder ≫ (Algebra.TensorProduct.map ?_ ?_).toUnder <;>
      exact @AlgHom.mk _ _ _ _ _ _ _ (_) (.id _) fun _ ↦ rfl

However, this typeclass issue keeps consistently popping up in this context. Is there a way to prevent this mismatch from happening?

[Yaël Dillies]

For readers with less context than me, docs#CommRingCat.instAlgebraCarrierRightDiscretePUnit is constructed out of docs#RingHom.toAlgebra, which is known to cause non-defeq diamonds (because it makes up the redundant smul field)

[Yaël Dillies]

Michał and I know why this mismatch is happening, so the question rather is: Can we design the code so as to avoid running into this mismatch?

[Aaron Liu]

Yaël Dillies said:

For readers with less context than me, docs#CommRingCat.instAlgebraCarrierRightDiscretePUnit is constructed out of docs#RingHom.toAlgebra, which is known to cause non-defeq diamonds (because it makes up the redundant nsmul, zsmul, etc... fields)

I don't see those fields in docs#Algebra. Am I missing something?

[Yaël Dillies]

Sorry, I only mean docs#Algebra.smul. Edited. Same issue though ;-)

[Kevin Buzzard]

Is this a #mwe ? After import Mathlib I get

failed to synthesize
  ChosenFiniteProducts (Under R)ᵒᵖ

Is this what you're asking about? (I doubt it)

[Michał Mrugała]

This is not a mwe because of this instance not being in mathlib. I can post the code later.

[Kevin Buzzard]

Probably you can illustrate the diamond without posting the chosen finite products instance.

[Kevin Buzzard]

Is this your question:

import Mathlib

variable {R : CommRingCat} {A : Type*} [CommRing A] [Algebra R A]

example : A = ↑(CommRingCat.mkUnder R A) := rfl

def i1 : SMul R A := inferInstance
def i2 : SMul R ↑(CommRingCat.mkUnder R A) := inferInstance

example (r : R) (a : A) : @SMul.smul R A i1 r a =  @SMul.smul R A i2 r a := rfl -- fails

? Yeah this is a common story in category theory, unfortunately. This sort of thing was the bane of Amelia's life when doing group cohomology.

[Kevin Buzzard]

As you say,

import Mathlib

variable {R : CommRingCat} {A : Type*} [CommRing A] [ia : Algebra R A]

example : A = ↑(CommRingCat.mkUnder R A) := rfl

def i1 : SMul R A := inferInstance
def i2 : SMul R ↑(CommRingCat.mkUnder R A) := inferInstance

example (r : R) (a : A) : @SMul.smul R A i1 r a =  @SMul.smul R A i2 r a := by
  change ia.1.1 r a = (algebraMap (↑R) A) r * a
  sorry -- not rfl

[Michał Mrugała]

This looks like the same issue essentially, and it’s the bane of my existence because it makes simplifying and rewriting expressions a nightmare.

[Kevin Buzzard]

Yeah there is a fundamental problem with our set-up here. I still can't run your actual code to the see the problem because you still didn't post a #mwe so it's difficult to help. What happens if you remove the instance tag from CommRingCat.instAlgebraCarrierRightDiscretePUnit?

[Kevin Buzzard]

You could also add something like instance [Algebra R A] : Algebra R ↑(CommRingCat.mkUnder R A) := inferInstanceAs (Algebra R A) or whatever the syntax for that is.

[Michał Mrugała]

Here is the code for a working example:

import Mathlib

open CategoryTheory Limits Opposite

namespace CategoryTheory.Limits
variable {C : Type*} [Category C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}

@[simp]
def pushoutCocone.toBinaryCofan : PushoutCocone f g ⥤ BinaryCofan (Under.mk f) (.mk g) where
  obj c := BinaryCofan.mk (Under.homMk (U := Under.mk f) c.inl rfl)
      (Under.homMk (U := Under.mk g) (V := Under.mk (f ≫ c.inl)) c.inr c.condition.symm)
  map {c1 c2} a := {
    hom := Under.homMk a.hom
    w := by rintro (_|_) <;> aesop_cat
  }

@[simp]
def binaryCofanUnder.toPushoutCocone : BinaryCofan (Under.mk f) (.mk g) ⥤ PushoutCocone f g where
  obj c := PushoutCocone.mk c.inl.right c.inr.right (c.inl.w.symm.trans c.inr.w)
  map {c1 c2} a := {
    hom := a.hom.right
    w := by rintro (_|_|_) <;> simp [← Under.comp_right]
  }

def aux_unit :
    𝟭 (PushoutCocone f g) ≅ pushoutCocone.toBinaryCofan ⋙ binaryCofanUnder.toPushoutCocone :=
  NatIso.ofComponents (fun c ↦ c.eta) (by aesop_cat)

def aux_counit :
    binaryCofanUnder.toPushoutCocone ⋙ pushoutCocone.toBinaryCofan
    ≅ 𝟭 (BinaryCofan (Under.mk f) (Under.mk g)) :=
  NatIso.ofComponents (fun X ↦ Limits.BinaryCofan.ext (Under.isoMk (Iso.refl _)
    (by simpa using X.inl.w.symm)) (by aesop_cat) (by aesop_cat))
    (by intros; ext; simp [BinaryCofan.ext])

@[simp]
def pushoutCoconeEquivBinaryCofan : PushoutCocone f g ≌ BinaryCofan (Under.mk f) (Under.mk g) :=
  .mk pushoutCocone.toBinaryCofan binaryCofanUnder.toPushoutCocone aux_unit aux_counit

def pushoutCocone.IsColimit.toBinaryCofanIsColimit {c : PushoutCocone f g}  (hc : IsColimit c) :
    IsColimit <| pushoutCocone.toBinaryCofan.obj c :=
  (IsColimit.ofCoconeEquiv pushoutCoconeEquivBinaryCofan).symm hc

end CategoryTheory.Limits

namespace CategoryTheory.Limits
variable {C : Type*} [Category C] {X Y P : C}

@[simps!]
def BinaryCofan.op (c : BinaryCofan X Y) : BinaryFan (.op X : Cᵒᵖ) (.op Y) :=
  .mk (.op c.inl) (.op c.inr)

@[simps!]
def BinaryFan.unop (c : BinaryFan (.op X : Cᵒᵖ) (.op Y)) : BinaryCofan X Y :=
  BinaryCofan.mk c.fst.unop c.snd.unop

@[simp] lemma BinaryCofan.op_mk (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : op (mk ι₁ ι₂) = .mk ι₁.op ι₂.op := rfl

@[simp] lemma BinaryFan.unop_mk (ι₁ : op P ⟶ op X) (ι₂ : op P ⟶ op Y) :
    unop (mk ι₁ ι₂) = .mk ι₁.unop ι₂.unop := rfl

lemma aux {D : Type*} [Category D] {F G : C ⥤ D} (α : F ⟶ G) :
    (NatTrans.op α).app (.op X) = (α.app X).op := rfl

def BinaryCofan.IsColimit.op {c : BinaryCofan X Y} (hc : IsColimit c) : IsLimit <| c.op where
  lift s := .op <| hc.desc (BinaryFan.unop s)
  fac s := by rintro (_|_) <;> simp [← CategoryTheory.op_comp, hc.fac]
  uniq s m h := by
    replace h j : c.ι.app j ≫ m.unop = (BinaryFan.unop s).ι.app j := by
      specialize h j; obtain ⟨_ | _⟩ := j <;> simpa using Quiver.Hom.op_inj h
    simpa using congr($(hc.uniq (BinaryFan.unop s) m.unop h).op)

end CategoryTheory.Limits

namespace CommRingCat.Under
variable {R : CommRingCat}

/-- A choice of finite products of `(Under R)ᵒᵖ` for `R : CommRingCat` given by the tensor product.
-/
noncomputable instance chosenFiniteProducts : ChosenFiniteProducts (Under R)ᵒᵖ where
  product X Y := {
    cone := BinaryCofan.op <| pushoutCocone.toBinaryCofan.obj <|
      pushoutCocone R (unop X).right (unop Y).right
    isLimit := BinaryCofan.IsColimit.op <| pushoutCocone.IsColimit.toBinaryCofanIsColimit <|
        CommRingCat.pushoutCoconeIsColimit R _ _
  }
  terminal := ⟨_, terminalOpOfInitial Under.mkIdInitial⟩

end CommRingCat.Under

variable {R : CommRingCat} {A : Type*} [CommRing A] [HopfAlgebra R A]


noncomputable instance : Grp_Class <| op <| CommRingCat.mkUnder R A where
  one := op <| (Bialgebra.counitAlgHom R A).toUnder
  mul := op <| by
    change R.mkUnder A ⟶ R.mkUnder _
    simp
    /-
    ⊢ R.mkUnder A ⟶ R.mkUnder (TensorProduct ↑R ↑(R.mkUnder A).right ↑(R.mkUnder A).right)
    -/
    --refine (Bialgebra.comulAlgHom R A).toUnder
    sorry
  one_mul' := sorry
  mul_one' := sorry
  mul_assoc' := sorry
  inv := sorry
  left_inv' := sorry
  right_inv' := sorry

[Kevin Buzzard]

Thanks. So just to summarise the issue:

If you remove the problematic instance with attribute [-instance] CommRingCat.instAlgebraCarrierRightDiscretePUnit then the first thing that breaks is the instance for ChosenFiniteProducts (Under R)ᵒᵖ, because given X : (Under R)ᵒᵖ Lean needs to find an instance of Algebra ↑R ↑(unop X).right and it can't do so. If you make this instance with docs#CommRingCat.instAlgebraCarrierRightDiscretePUnit then you'll get a diamond if you ever apply it with X = op (R.mkUnder A) for some [Algebra R A] because then ↑(unop X).right is defeq to A but the typeclass inference system finds different (i.e. definitionally different, but propeq) algebra instances on the two types. However if you try to avoid such As and just work with Xs of type (Under R)ᵒᵖ then there is no way to say "I am actually a Hopf algebra" because HopfAlgebra extends Algebra.

In simple terms, if you start with [Algebra R A] and then turn A into a term of type Under R and then back into a type, you end up with a definitionally different algebra instance on a definitionally equal type. This means that it's extremely annoying to do mathematics which relies on both constructions made in type-land (e.g. HopfAlgebra) and in category-land (e.g. ChosenFiniteProducts). A key example of such mathemtics is the theory of group schemes, which is absolutely essential for FLT. So we have a very interesting problem here!

[Kevin Buzzard]

Here's the diamond, as noted above, plus the proof that it's propeq:

import Mathlib

variable {R : CommRingCat} {A : Type*} [CommRing A] [Algebra R A]

example : A = ↑(CommRingCat.mkUnder R A) := rfl

def i1 : SMul R A := inferInstance
def i2 : SMul R ↑(CommRingCat.mkUnder R A) := inferInstance

example (r : R) (a : A) : @SMul.smul R A i1 r a = @SMul.smul R A i2 r a := by
  change r • a = (algebraMap (↑R) A) r * a
  exact Algebra.smul_def r a -- but not `rfl`

[Michał Mrugała]

Yeah this summary is pretty much what we've concluded as well. One idea that's been floated is to just define CommAlgCat and work with that instead of Under R. We've managed to deal with the diamonds for proofs of one_mul' and mul_one' but mul_comm' seems extremely painful because this diamond happens internally in the triple tensor product.

[Kevin Buzzard]

This discussion needs to move to #mathlib4 so some expert eyes will see it (many of the people who might be able to say something helpful are not subscribed to this channel). I'll start a new thread.

[Yaël Dillies]

Can't you move the existing one? EDIT: I guess the point is that you get to write a better summary of the situation

[Notification Bot]

This topic was moved here from #new members > Algebra type class inference by Kevin Buzzard.

[Eric Wieser]

Fundamentally the issue here is that docs#CommRingCat.instAlgebraCarrierRightDiscretePUnit uses RingHom.toAlgebra, which almost always creates diamonds

[Eric Wieser]

But in this case it has no other choice, because the SMul instance which is carried by Algebra to avoid the diamond cannot be carried by CategoryTheory.Under R

[Kevin Buzzard]

I wonder whether a way of fixing the issue is defining CommAlgCat R so that the objects are (edit: types A equipped with) terms of type Algebra R A

[Eric Wieser]

Yes, I think this is an argument for not defining CommAlgCat in terms of Under

[Eric Wieser]

@Kyle Miller, do you have any idea where DiscretePUnit is being inserted in the name from? nevermind, it's from expanding Under

[Kevin Buzzard]

Is there another highly disruptive but possible approach, involving redefining Algebra R A as a ring morphism and defining the SMul to be f(r) * a? Or is this impossible for other reasons?

[Eric Wieser]

That's impossible for other reasons, consider A := Matrix n n R and the natural module structure on matrices: diagonal (algebraMap _ _ r) * M is not possible to make defeq to r • M

[Eric Wieser]

Maybe CategoryTheory.Under could take some extra [UnderData R] assumption, which for CommRingCat carries the smul action?

[Michał Mrugała]

CommAlgCat seems to be working well

[Kim Morrison]

Can someone remind me why we wanted to avoid a hand-rolled CommAlgCat in favour of using Under? Just avoiding having two ways to say the same thing?

[Andrew Yang]

Yes. And to apply the general category theoretic machinery about Over categories.