ker_comp_eq_of_commute_of_disjoint_ker

English

If f and g commute and ker f is disjoint from ker g, then ker(f ∘ g) = ker f ⊔ ker g.

Русский

Если f и g commute и ker f дисjoint ker g, то ker(f ∘ g) = ker f ⊔ ker g.

LaTeX

$$$[\operatorname{FiniteDimensional}_K V] {f g: V \to V} (h: \operatorname{Commute} f g) (h': \operatorname{Disjoint}(\ker f)(\ker g)) : \ker(f \circ g) = \ker f \; \bigoplus\; \ker g$$$

Lean4

theorem ker_comp_eq_of_commute_of_disjoint_ker [FiniteDimensional K V] {f g : V →ₗ[K] V} (h : Commute f g)
    (h' : Disjoint (ker f) (ker g)) : ker (f ∘ₗ g) = ker f ⊔ ker g :=
  by
  suffices ∀ x, f x = 0 → f (g x) = 0 by rw [ker_comp, comap_eq_sup_ker_of_disjoint _ h']; simpa
  intro x hx
  rw [← comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_apply, hx, map_zero]

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