English
Restriction is functorial with respect to composition: restricting along g ∘ f is the composition of restricting along f and g.
Русский
Ограничение по композиции гомоморфизмов удовлетворяет композиции: ограничение по g ∘ f эквивалентно композиции ограничений по f и по g.
LaTeX
$$def resComp {G H K} (f : G →* H) (g : H →* K) : res V g ⋙ res V f ≅ res V (g.comp f)$$
Lean4
/-- The natural isomorphism from the composition of restrictions along homomorphisms
to the restriction along the composition of homomorphism.
-/
@[simps!]
def resComp {G H K : Type*} [Monoid G] [Monoid H] [Monoid K] (f : G →* H) (g : H →* K) :
res V g ⋙ res V f ≅ res V (g.comp f) :=
NatIso.ofComponents fun M => mkIso (Iso.refl _)
