English
A direct summand of a reflexive module is reflexive. More precisely, if M is reflexive and N with maps i:N→M and s:M→N satisfy s∘i = id_N, then N is reflexive.
Русский
Прямой суммируемый подмодуль рефлексивного модуля рефлексивен: если M рефлексивен и существует разложение N в M через i и s с s∘i = id_N, то N рефлексивен.
LaTeX
$$IsReflexive(R,M) \\wedge (\\exists i,N:\\ N \\to M, s:M \\to N, s \\circ i = \\mathrm{id}_N) \\Rightarrow IsReflexive(R,N).$$
Lean4
/-- A direct summand of a reflexive module is reflexive. -/
theorem of_split (i : N →ₗ[R] M) (s : M →ₗ[R] N) (H : s ∘ₗ i = .id) : IsReflexive R N where
bijective_dual_eval' :=
⟨.of_comp (f := i.dualMap.dualMap) <| (bijective_dual_eval R M).1.comp (injective_of_comp_eq_id i _ H),
.of_comp (g := s) <|
(surjective_of_comp_eq_id i.dualMap.dualMap s.dualMap.dualMap <| congr_arg (dualMap ∘ dualMap) H).comp
(bijective_dual_eval R M).2⟩
