closedComplemented_ker_of_rightInverse

English

If f1: M →L[R] M2 and f2: M2 →L[R] M satisfy f2 ∘ f1 = id_M, then ker f1 is closed complemented.

Русский

Пусть f1: M →L[R] M2 и f2: M2 →L[R] M удовлетворяют f2 ∘ f1 = id_M; тогда ker f1 является замкнуто дополненным подпопространством.

LaTeX

$$$\text{If } f_1: M \to_L[R] M_2,\ f_2: M_2 \to_L[R] M\text{ satisfy } f_2 \circ f_1 = \mathrm{id}_M,\; \ker(f_1) \text{ is closed complemented.}$$$

Lean4

theorem closedComplemented_ker_of_rightInverse {R : Type*} [Ring R] {M : Type*} [TopologicalSpace M] [AddCommGroup M]
    {M₂ : Type*} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R M₂] [IsTopologicalAddGroup M]
    (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : Function.RightInverse f₂ f₁) : (ker f₁).ClosedComplemented :=
  ⟨f₁.projKerOfRightInverse f₂ h, f₁.projKerOfRightInverse_apply_idem f₂ h⟩

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