English
The kernel of the composition g ∘ f has FG if ker f and ker g have FG and f is surjective.
Русский
Ядро композиции g ∘ f имеет FG, если ker f и ker g имеют FG и f является сюрьективным.
LaTeX
$$ker(g ∘ f) FG given FG ker f, FG ker g, and f surjective$$
Lean4
theorem fg_ker_comp {R S A : Type*} [CommRing R] [CommRing S] [CommRing A] (f : R →+* S) (g : S →+* A)
(hf : (RingHom.ker f).FG) (hg : (RingHom.ker g).FG) (hsur : Function.Surjective f) : (RingHom.ker (g.comp f)).FG :=
by
letI : Algebra R S := RingHom.toAlgebra f
letI : Algebra R A := RingHom.toAlgebra (g.comp f)
letI : Algebra S A := RingHom.toAlgebra g
letI : IsScalarTower R S A := IsScalarTower.of_algebraMap_eq fun _ => rfl
let f₁ := Algebra.linearMap R S
let g₁ := (IsScalarTower.toAlgHom R S A).toLinearMap
exact Submodule.fg_ker_comp f₁ g₁ hf (Submodule.fg_restrictScalars (RingHom.ker g) hg hsur) hsur
