English
A lemma about the congruence behavior of res on morphisms under equality of f and f'.
Русский
Лемма о поведении ограничения в отношении морфизмов при равенстве f и f'.
LaTeX
$$$\\forall f,f' : G \\to_{}^{} H\\ (h : f=f')\\;\\mathrm{ResCongr}\\ V f f' h : ContAction.res V f \\cong ContAction.res V f'$.$$
Lean4
/-- If `f = f'`, restriction of scalars along `f` and `f'` is the same. -/
@[simps! hom inv]
def resCongr (f f' : G →ₜ* H) (h : f = f') : ContAction.res V f ≅ ContAction.res V f' :=
NatIso.ofComponents (fun _ ↦ ObjectProperty.isoMk _ (Action.mkIso (Iso.refl _) (by subst h; simp))) fun f ↦
by
apply Action.Hom.ext
rw [ObjectProperty.FullSubcategory.comp_def, ObjectProperty.FullSubcategory.comp_def]
simp
