Documentation

Seymour.Matroid.Sum1

Matroid 1-sum #

Here we study the 1-sum of matroids (starting with the 1-sum of matrices).

Definition #

source
def matrixSum1 {R : Type u_1} [Zero R] {Xₗ : Type u_2} {Yₗ : Type u_3} {Xᵣ : Type u_4} {Yᵣ : Type u_5} (Aₗ : Matrix Xₗ Yₗ R) (Aᵣ : Matrix Xᵣ Yᵣ R) :
Matrix (Xₗ ⊕ Xᵣ) (Yₗ ⊕ Yᵣ) R

Matrix-level 1-sum for matroids defined by their standard representation matrices; does not check legitimacy.

Equations
Instances For
    source
    noncomputable def standardReprSum1 {α : Type u_1} [DecidableEq α] {Sₗ Sᵣ : StandardRepr α Z2} (hXY : Sₗ.X ⫗ Sᵣ.Y) (hYX : Sₗ.Y ⫗ Sᵣ.X) :
    Option (StandardRepr α Z2)

    StandardRepr-level 1-sum of two matroids. Returns the result only if valid.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Matroid.IsSum1of {α : Type u_1} [DecidableEq α] (M Mₗ Mᵣ : Matroid α) :
      Prop

      Binary matroid M is a result of 1-summing Mₗ and Mᵣ in some way.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        API #

        source
        theorem standardReprSum1_disjoint_X {α : Type u_1} [DecidableEq α] {Sₗ Sᵣ S : StandardRepr α Z2} {hXY : Sₗ.X ⫗ Sᵣ.Y} {hYX : Sₗ.Y ⫗ Sᵣ.X} (hS : standardReprSum1 hXY hYX = some S) :
        Sₗ.X ⫗ Sᵣ.X
        source
        theorem standardReprSum1_disjoint_Y {α : Type u_1} [DecidableEq α] {Sₗ Sᵣ S : StandardRepr α Z2} {hXY : Sₗ.X ⫗ Sᵣ.Y} {hYX : Sₗ.Y ⫗ Sᵣ.X} (hS : standardReprSum1 hXY hYX = some S) :
        Sₗ.Y ⫗ Sᵣ.Y
        source
        theorem standardReprSum1_X_eq {α : Type u_1} [DecidableEq α] {Sₗ Sᵣ S : StandardRepr α Z2} {hXY : Sₗ.X ⫗ Sᵣ.Y} {hYX : Sₗ.Y ⫗ Sᵣ.X} (hS : standardReprSum1 hXY hYX = some S) :
        S.X = Sₗ.X ∪ Sᵣ.X
        source
        theorem standardReprSum1_Y_eq {α : Type u_1} [DecidableEq α] {Sₗ Sᵣ S : StandardRepr α Z2} {hXY : Sₗ.X ⫗ Sᵣ.Y} {hYX : Sₗ.Y ⫗ Sᵣ.X} (hS : standardReprSum1 hXY hYX = some S) :
        S.Y = Sₗ.Y ∪ Sᵣ.Y
        source
        theorem Matroid.IsSum1of.E_eq {α : Type u_1} [DecidableEq α] {M Mₗ Mᵣ : Matroid α} (hMMM : M.IsSum1of Mₗ Mᵣ) :
        M.E = Mₗ.E ∪ Mᵣ.E
        source
        theorem standardReprSum1_disjoint_E {α : Type u_1} [DecidableEq α] {Sₗ Sᵣ S : StandardRepr α Z2} {hXY : Sₗ.X ⫗ Sᵣ.Y} {hYX : Sₗ.Y ⫗ Sᵣ.X} (hS : standardReprSum1 hXY hYX = some S) :
        Sₗ.toMatroid.E ⫗ Sᵣ.toMatroid.E
        source
        theorem Matroid.IsSum1of.disjoint_E {α : Type u_1} [DecidableEq α] {M Mₗ Mᵣ : Matroid α} (hMMM : M.IsSum1of Mₗ Mᵣ) :
        Mₗ.E ⫗ Mᵣ.E

        Results #

        source
        theorem standardReprSum1_eq_disjointSum {α : Type u_1} [DecidableEq α] {Sₗ Sᵣ S : StandardRepr α Z2} {hXY : Sₗ.X ⫗ Sᵣ.Y} {hYX : Sₗ.Y ⫗ Sᵣ.X} (hS : standardReprSum1 hXY hYX = some S) :
        S.toMatroid = ⋯.matroidSum
        source
        theorem Matroid.IsSum1of.eq_disjointSum {α : Type u_1} [DecidableEq α] {M Mₗ Mᵣ : Matroid α} (hMMM : M.IsSum1of Mₗ Mᵣ) :
        M = ⋯.matroidSum

        The 1-sum of matroids is a disjoint sum of those matroids.

        source
        theorem standardReprSum1_hasTuSigning {α : Type u_1} [DecidableEq α] {Sₗ Sᵣ S : StandardRepr α Z2} {hXY : Sₗ.X ⫗ Sᵣ.Y} {hYX : Sₗ.Y ⫗ Sᵣ.X} (hSₗ : Sₗ.B.HasTuSigning) (hSᵣ : Sᵣ.B.HasTuSigning) (hS : standardReprSum1 hXY hYX = some S) :
        S.B.HasTuSigning
        source
        theorem Matroid.IsSum1of.isRegular {α : Type u_1} [DecidableEq α] {M Mₗ Mᵣ : Matroid α} (hMMM : M.IsSum1of Mₗ Mᵣ) (hM : M.RankFinite) (hMₗ : Mₗ.IsRegular) (hMᵣ : Mᵣ.IsRegular) :
        M.IsRegular

        Any 1-sum of regular matroids is a regular matroid. This is part one (of three) of the easy direction of the Seymour's theorem.