matroid_isBasis_iff_of_subsingleton

English

Let A be a subsingleton algebra over a commutative ring R. For any two subsets s and t of A, the matroidIsBasis relation holds between s and t precisely when s and t are equal; i.e., there is only one possible basis relation in this degenerate setting.

Русский

Пусть A является пододнородной алгеброй над кольцом R. Для любых подмножеств s, t пара матроида IsBasis(s, t) существует тогда и только тогда, когда s = t; т.е. в этой редуцированной ситуации базис уникален.

LaTeX

$$$ ( \\mathrm{matroid} \\, R\\, A ).\\mathrm{IsBasis}(s,t) \\;\\Longleftrightarrow\\; s = t $$$

Lean4

theorem matroid_isBasis_iff_of_subsingleton [Subsingleton A] {s t : Set A} : (matroid R A).IsBasis s t ↔ s = t :=
  by
  have := (FaithfulSMul.algebraMap_injective R A).subsingleton
  simp_rw [Matroid.IsBasis, matroid_indep_iff, of_subsingleton, true_and, matroid_e, subset_univ, and_true, ←
    le_iff_subset, maximal_le_iff]

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