def Matroid.CrossingBinary {α : Type u_1} (M : Matroid α) : Prop

A matroid is Crossing-Binary if all its finite crossings are even. This is the same as having no U₂,₄-minor; see crossingBinary_iff_no_U24_isMinor.

Equations

• M.CrossingBinary = ∀ ⦃X : Finset α⦄, M.IsCrossing ↑X → Even X.card

theorem Matroid.CrossingBinary.even_of_finite {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.CrossingBinary) (hX : M.IsCrossing X) (hfin : X.Finite) : Even hfin.toFinset.card

theorem Matroid.CrossingBinary.even_of_isCrossing {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.CrossingBinary) (hX : M.IsCrossing X) : Even X.encard

theorem Matroid.CrossingBinary.dual {α : Type u_1} {M : Matroid α} (hM : M.CrossingBinary) : M✶.CrossingBinary

theorem Matroid.CrossingBinary.of_dual {α : Type u_1} {M : Matroid α} (hM : M✶.CrossingBinary) : M.CrossingBinary

@[simp]

theorem Matroid.CrossingBinary_dual_iff {α : Type u_1} {M : Matroid α} : M✶.CrossingBinary ↔ M.CrossingBinary

theorem Matroid.CrossingBinary.of_isMinor {α : Type u_1} {N M : Matroid α} (hM : M.CrossingBinary) (hNM : N ≤m M) : N.CrossingBinary

theorem Matroid.CrossingBinary.iso {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (hM : M.CrossingBinary) (i : M ≂ N) : N.CrossingBinary

theorem Matroid.CrossingBinary.isoMinor {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (hM : M.CrossingBinary) (e : IsoMinor N M) : N.CrossingBinary

theorem Matroid.crossingBinary_of_eRank_le_one {α : Type u_1} {M : Matroid α} (hM : M.eRank ≤ 1) : M.CrossingBinary

theorem Matroid.crossingBinary_unif_iff {a b : ℕ} : (unif a b).CrossingBinary ↔ a ≤ 1 ∨ b ≤ a + 1

CrossingBinary uniform matroids have rank or corank at most one.

theorem Matroid.exist_isCocircuits_of_rank_two {α : Type u_1} {M : Matroid α} {e : α} (hr : M.eRank = 2) (hel : ¬M.IsColoop e) (he : M.IsPoint {e}) (hU : M.NoUniformMinor 2 4) : ∃ (C₁ : Set α) (C₂ : Set α), (M.delete {e}).IsCocircuit C₁ ∧ (M.delete {e}).IsCocircuit C₂ ∧ Disjoint C₁ C₂ ∧ C₁ ∪ C₂ = M.E \ {e}

If e is a non-coloop point in a rank-two matroid with no U₂,₄-minor, then M ＼ e is the disjoint union of two cocircuits.

theorem Matroid.exists_smaller_of_odd_isCircuit_isCocircuit {α : Type u_1} {M : Matroid α} {C : Set α} (hfin : C.Finite) (hCc : M.IsCircuit C) (hCk : M.IsCocircuit C) (hCs : M.Spanning C) (hCcs : M✶.Spanning C) (h_odd : Odd hfin.toFinset.card) (h_bin : M.NoUniformMinor 2 4) : ∃ (N : Matroid α), N ≤m M ∧ N.IsCircuit C ∧ ∃ (K : Finset α), N.IsCocircuit ↑K ∧ ↑K ⊂ C ∧ Odd K.card

If C is a spanning/cospanning circuit/cocircuit of finite odd cardinality in a matroid M with no U₂,₄-minor, then there is an odd proper subset of C that is a cocircuit/cocircuit in a minor of M.

theorem Matroid.IsCrossing.exists_isMinor_isCircuit_isCocircuit {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.IsCrossing X) (hXne : X.Nonempty) : ∃ (N : Matroid α), N ≤m M ∧ N.IsCircuit X ∧ N.IsCocircuit X ∧ N.Spanning X ∧ N✶.Spanning X

For any nonempty crossing X of M, we can find a minor of M in which X is a spanning/cospanning circuit/cocircuit.

theorem Matroid.exists_uniformMinor_of_odd_isCrossing {α : Type u_1} {M : Matroid α} {X : Finset α} (hX : M.IsCrossing ↑X) (h_odd : Odd X.card) : ¬M.NoUniformMinor 2 4

theorem Matroid.crossingBinary_iff_no_U24_isMinor {α : Type u_1} (M : Matroid α) : M.CrossingBinary ↔ M.NoUniformMinor 2 4

theorem Matroid.Even.add_even {α : Type u_1} [Semiring α] {a b : α} (ha : Even a) (hb : Even b) : Even (a + b)