∀ {A : Type u} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  (self : Algebra.Smooth.DescentAux✝ A B) (j : Algebra.Smooth.DescentAux.rels✝ self),
  (Algebra.Smooth.DescentAux.p✝ self j).IsHomogeneous 2