English
The zero map is invertible if and only if the domain and codomain are both subsingletons.
Русский
Нулевое отображение обратимо тогда и только тогда, когда обе области — одноэлементные.
LaTeX
$$$ IsInvertible(0: M \to M_2) \iff (Subsingleton M) \land (Subsingleton M_2) $$$
Lean4
@[simp]
theorem isInvertible_zero_iff : IsInvertible (0 : M →L[R] M₂) ↔ Subsingleton M ∧ Subsingleton M₂ :=
by
refine ⟨fun ⟨e, he⟩ ↦ ?_, ?_⟩
· have A : Subsingleton M := by
refine ⟨fun x y ↦ e.injective ?_⟩
simp [he, ← ContinuousLinearEquiv.coe_coe]
exact ⟨A, e.toEquiv.symm.subsingleton⟩
· rintro ⟨hM, hM₂⟩
let e : M ≃L[R] M₂ :=
{ toFun := 0
invFun := 0
left_inv x := Subsingleton.elim _ _
right_inv x := Subsingleton.elim _ _
map_add' x y := Subsingleton.elim _ _
map_smul' c x := Subsingleton.elim _ _ }
refine ⟨e, ?_⟩
ext x
exact Subsingleton.elim _ _
