English
Let f: M → M′ and g: M′ → M′′ be a left-exact sequence with f injective and range f = ker g. If r is regular on M and on M′′, then r is regular on M′.
Русский
Пусть существует левосторонняя точная последовательность 0 → M → M′ → M′′ с инъективным f и равенством range(f) = ker(g). Если r регулярен на M и на M′′, тогда r регулярен на M′.
LaTeX
$$$\text{If } f \text{ is injective and } \operatorname{range}(f) = \ker(g) \text{ and } IsSMulRegular(M,r) \text{ and } IsSMulRegular(M'',r) , \text{ then } IsSMulRegular(M',r).$$$
Lean4
/-- Given a left exact sequence `0 → M → M' → M''`, if `r` is regular on both
`M` and `M''` it's regular `M'` too. -/
theorem isSMulRegular_of_range_eq_ker {f : M →ₗ[R] M'} {g : M' →ₗ[R] M''} (hf : Function.Injective f)
(hfg : LinearMap.range f = LinearMap.ker g) (h1 : IsSMulRegular M r) (h2 : IsSMulRegular M'' r) :
IsSMulRegular M' r := by
refine IsSMulRegular.of_right_eq_zero_of_smul ?_
intro x hx
obtain ⟨y, ⟨⟩⟩ :=
(congrArg (x ∈ ·) hfg).mpr <|
h2.right_eq_zero_of_smul <| (g.map_smul r x).symm.trans <| (congrArg _ hx).trans g.map_zero
refine (congrArg f (h1.right_eq_zero_of_smul ?_)).trans f.map_zero
exact hf <| (f.map_smul r y).trans <| hx.trans f.map_zero.symm
