map_first_exact_on_four_term_exact_of_isSMulRegular_last

English

If f1, f2, f3 form a chain with exactness f1 ∘ f2 and f2 ∘ f3 and r is IsSMulRegular on the target, then the pair (map r f1, map r f2) is exact.

Русский

Если последовательность линейных отображений последовательна и точна на участках, и элемент r регулярен по действию, то пары (map r f1, map r f2) образуют точную пару.

LaTeX

$$$\\text{Exact}(f_1,f_2) \\wedge \\text{Exact}(f_2,f_3) \\wedge \\operatorname{IsSMulRegular}(M''', r) \\Rightarrow \\text{Exact}(\\mathrm{map}\, r\, f_1, \\mathrm{map}\, r\, f_2)$$$

Lean4

theorem map_first_exact_on_four_term_exact_of_isSMulRegular_last {M'''} [AddCommGroup M'''] [Module R M'''] {r : R}
    {f₁ : M →ₗ[R] M'} {f₂ : M' →ₗ[R] M''} {f₃ : M'' →ₗ[R] M'''} (h₁₂ : Exact f₁ f₂) (h₂₃ : Exact f₂ f₃)
    (h : IsSMulRegular M''' r) : Exact (map r f₁) (map r f₂) :=
  suffices IsSMulRegular (M'' ⧸ LinearMap.range f₂) r
    by
    dsimp [map, mapQLinear]
    rw [Exact.exact_mapQ_iff h₁₂, map_pointwise_smul, Submodule.map_top, inf_comm]
    exact smul_top_inf_eq_smul_of_isSMulRegular_on_quot this
  h.of_injective _ <| LinearMap.ker_eq_bot.mp <| ker_liftQ_eq_bot' _ _ h₂₃.linearMap_ker_eq.symm

Похожие утверждения