Documentation

Seymour.Sum1

This file contains everything about 1-sum of binary matroids.

source
@[reducible, inline]
abbrev Matrix_1sumComposition {α : Type u_1} {β : Type u_2} [Zero β] {X₁ : Set α} {Y₁ : Set α} {X₂ : Set α} {Y₂ : Set α} (A₁ : Matrix (↑X₁) (↑Y₁) β) (A₂ : Matrix (↑X₂) (↑Y₂) β) :
Matrix (↑X₁ ⊕ ↑X₂) (↑Y₁ ⊕ ↑Y₂) β

Matrix-level 1-sum for matroids defined by their standard representation matrices.

Equations
Instances For
    source
    def StandardRepresentation_1sum {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} (hXY : M₁.X ⫗ M₂.Y) (hYX : M₁.Y ⫗ M₂.X) :
    StandardRepresentation α × Prop

    StandardRepresentation-level 1-sum of two matroids. It checks that everything is disjoint (returned as .snd of the output).

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

      Binary matroid M is a result of 1-summing M₁ and M₂ (should be equivalent to disjoint sums).

      Equations
      Instances For
        source
        theorem StandardRepresentation_1sum_as_disjoint_sum {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {hXY : M₁.X ⫗ M₂.Y} {hYX : M₁.Y ⫗ M₂.X} (valid : (StandardRepresentation_1sum hXY hYX).2) :
        (StandardRepresentation_1sum hXY hYX).1.toMatroid = M₁.toMatroid.disjointSum M₂.toMatroid ⋯

        Matroid constructed from a valid 1-sum of binary matroids is the same as disjoint sum of matroids constructed from them.

        source
        theorem StandardRepresentation_1sum_comm {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {hXY : M₁.X ⫗ M₂.Y} {hYX : M₁.Y ⫗ M₂.X} (valid : (StandardRepresentation_1sum hXY hYX).2) :
        (StandardRepresentation_1sum hXY hYX).1.toMatroid = (StandardRepresentation_1sum ⋯ ⋯).1.toMatroid

        A valid 1-sum of binary matroids is commutative.

        source
        theorem StandardRepresentation_1sum_isRegular {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} [Fintype ↑M₁.X] [Fintype ↑M₁.Y] [Fintype ↑M₂.X] [Fintype ↑M₂.Y] (hXY : M₁.X ⫗ M₂.Y) (hYX : M₁.Y ⫗ M₂.X) (hM₁ : M₁.IsRegular) (hM₂ : M₂.IsRegular) :
        (StandardRepresentation_1sum hXY hYX).1.IsRegular
        source
        theorem StandardRepresentation.Is1sumOf.isRegular {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {M : StandardRepresentation α} [Fintype ↑M₁.X] [Fintype ↑M₁.Y] [Fintype ↑M₂.X] [Fintype ↑M₂.Y] (hM : M.Is1sumOf M₁ M₂) (hM₁ : M₁.IsRegular) (hM₂ : M₂.IsRegular) :
        M.IsRegular

        Any 1-sum of regular matroids is a regular matroid. This is the first of the three parts of the easy direction of the Seymour's theorem.

        source
        theorem StandardRepresentation.Is1sumOf.isRegular_left {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {M : StandardRepresentation α} (hMsum : M.Is1sumOf M₁ M₂) (hMreg : M.IsRegular) :
        M₁.IsRegular

        If a regular matroid is a 1-sum, then the left summand of the 1-sum is regular.

        source
        theorem StandardRepresentation.Is1sumOf.isRegular_right {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {M : StandardRepresentation α} (hMsum : M.Is1sumOf M₁ M₂) (hMreg : M.IsRegular) :
        M₂.IsRegular

        If a regular matroid is a 1-sum, then the right summand of the 1-sum is regular.