theorems about compositions of `RingHomClass` elements

Stream: mathlib4

[Christian Merten]

Is there a good way to generalize statements about ring homs where compositions are involved (e.g. docs#RingHom.comap_ker) to elements of types satisfying some RingHomClass F R S? Or do we have to copy such lemmas for e.g. AlgHoms?

[Edward van de Meent]

i think it's possible, but non-trivial, because there is no typeclass which tells you how to compose these "general maps which happen to be a ring-hom". There is only "cast them to RingHom, then compose", or "assume some third RingHomClass-value exists, and assume RingHomCompTriple" (from the top of my head). both ways don't seem ideal to me, but that's what we've got, as far as i can tell.

[Edward van de Meent]

i'd say the best alternative is to lift your statements via docs#RingHomClass.toRingHom

[Christian Merten]

Thanks! I think I'll stick to copying to the AlgHom case then, because e.g. this

import Mathlib

variable {R A B C F G : Type} [CommRing R] [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B]
  [Algebra R C] [FunLike F A B] [FunLike G B C] [RingHomClass F A B] [RingHomClass G B C]

lemma RingHom.comap_ker' (f : F) (g : G) : (RingHom.ker g).comap f =
    RingHom.ker ((RingHomClass.toRingHom g).comp <| RingHomClass.toRingHom f) :=
  RingHom.comap_ker (RingHomClass.toRingHom g) (RingHomClass.toRingHom f)

example (f : A →ₐ[R] B) (g : B →ₐ[R] C) : RingHom.ker (g.comp f) = ⊥ := by
  rw [← RingHom.comap_ker' f g]

does not work (while erw unsurprisingly does).