Documentation

Mathlib.Data.Matroid.Minor.Contract

Matroid Contraction #

Instead of deleting the the elements of X : Set α from M : Matroid α, we can contract them. The contraction of X from M, denoted M / X, is the matroid on ground set M.E \ X in which a set I is independent if and only if I ∪ J is independent in M, where J is an arbitrarily chosen basis for X. Contraction corresponds to contracting edges in graphic matroids (hence the name) and corresponds to projecting to a quotient space in the case of linearly representable matroids. It is an important notion in both these settings.

We can also define contraction much more tersely in terms of deletion and duality with M / X = (M✶ \ X)✶: that is, contraction is the dual operation of deletion. While this is perhaps less intuitive, we use this very concise expression as the definition, and prove with the lemma Matroid.IsBasis.contract_indep_iff that this is equivalent to the more verbose definition above.

Main Declarations #

Naming conventions #

Mirroring the convention for deletion, we use the abbreviation contractElem in lemma names to refer to the contraction M / {e} of a single element e : α from M : Matroid α.

def Matroid.contract {α : Type u_1} (M : Matroid α) (C : Set α) :

The contraction M / C is the matroid on M.E \ C in which a set I ⊆ M.E \ C is independent if and only if I ∪ J is independent, where J is an arbitrarily chosen basis for C. It is also equal by definition to (M✶ \ C)✶; see Matroid.IsBasis.contract_indep_iff for a proof that its independent sets are the claimed ones.

Equations
Instances For

    M / C refers to the contraction of a set C from the matroid M.

    Equations
    Instances For
      @[simp]
      theorem Matroid.contract_ground {α : Type u_1} (M : Matroid α) (C : Set α) :
      (M.contract C).E = M.E \ C
      theorem Matroid.dual_delete_dual {α : Type u_1} (M : Matroid α) (X : Set α) :
      @[simp]
      theorem Matroid.dual_delete {α : Type u_1} (M : Matroid α) (X : Set α) :
      @[simp]
      theorem Matroid.dual_contract {α : Type u_1} (M : Matroid α) (X : Set α) :
      theorem Matroid.dual_contract_dual {α : Type u_1} (M : Matroid α) (X : Set α) :
      @[simp]
      theorem Matroid.contract_contract {α : Type u_1} (M : Matroid α) (C₁ C₂ : Set α) :
      (M.contract C₁).contract C₂ = M.contract (C₁ C₂)
      theorem Matroid.contract_comm {α : Type u_1} (M : Matroid α) (C₁ C₂ : Set α) :
      (M.contract C₁).contract C₂ = (M.contract C₂).contract C₁
      theorem Matroid.dual_contract_delete {α : Type u_1} (M : Matroid α) (X Y : Set α) :
      theorem Matroid.dual_delete_contract {α : Type u_1} (M : Matroid α) (X Y : Set α) :
      theorem Matroid.contract_eq_self_iff {α : Type u_1} {M : Matroid α} {C : Set α} :
      M.contract C = M Disjoint C M.E
      theorem Matroid.contractElem_eq_self {α : Type u_1} {M : Matroid α} {e : α} (he : eM.E) :
      @[simp]
      theorem Matroid.contract_empty {α : Type u_1} (M : Matroid α) :
      theorem Matroid.contract_contract_eq_contract_diff {α : Type u_1} (M : Matroid α) (C₁ C₂ : Set α) :
      (M.contract C₁).contract C₂ = (M.contract C₁).contract (C₂ \ C₁)
      theorem Matroid.contract_eq_contract_iff {α : Type u_1} {M : Matroid α} {C₁ C₂ : Set α} :
      M.contract C₁ = M.contract C₂ C₁ M.E = C₂ M.E
      @[simp]
      theorem Matroid.contract_inter_ground_eq {α : Type u_1} (M : Matroid α) (C : Set α) :
      M.contract (C M.E) = M.contract C
      theorem Matroid.contract_ground_subset_ground {α : Type u_1} (M : Matroid α) (C : Set α) :
      (M.contract C).E M.E

      Independence and Coindependence #

      theorem Matroid.coindep_contract_iff {α : Type u_1} {M : Matroid α} {X C : Set α} :
      theorem Matroid.Coindep.coindep_contract_of_disjoint {α : Type u_1} {M : Matroid α} {X C : Set α} (hX : M.Coindep X) (hXC : Disjoint X C) :
      @[simp]
      theorem Matroid.contract_isCocircuit_iff {α : Type u_1} {M : Matroid α} {K C : Set α} :
      theorem Matroid.Indep.contract_isBase_iff {α : Type u_1} {M : Matroid α} {I B : Set α} (hI : M.Indep I) :
      (M.contract I).IsBase B M.IsBase (B I) Disjoint B I
      theorem Matroid.Indep.contract_indep_iff {α : Type u_1} {M : Matroid α} {I J : Set α} (hI : M.Indep I) :
      (M.contract I).Indep J Disjoint J I M.Indep (J I)
      theorem Matroid.IsNonloop.contractElem_indep_iff {α : Type u_1} {M : Matroid α} {e : α} {I : Set α} (he : M.IsNonloop e) :
      (M.contract {e}).Indep I eI M.Indep (insert e I)
      theorem Matroid.Indep.union_indep_iff_contract_indep {α : Type u_1} {M : Matroid α} {I J : Set α} (hI : M.Indep I) :
      M.Indep (I J) (M.contract I).Indep (J \ I)
      theorem Matroid.Indep.diff_indep_contract_of_subset {α : Type u_1} {M : Matroid α} {I J : Set α} (hJ : M.Indep J) (hIJ : I J) :
      (M.contract I).Indep (J \ I)
      theorem Matroid.Indep.contract_dep_iff {α : Type u_1} {M : Matroid α} {I J : Set α} (hI : M.Indep I) :
      (M.contract I).Dep J Disjoint J I M.Dep (J I)

      Bases #

      theorem Matroid.IsBasis.contract_eq_contract_delete {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis I X) :
      M.contract X = (M.contract I).delete (X \ I)

      Contracting a set is the same as contracting a basis for the set, and deleting the rest.

      theorem Matroid.Indep.union_isBasis_union_of_contract_isBasis {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.Indep I) (hB : (M.contract I).IsBasis J X) :
      M.IsBasis (J I) (X I)
      theorem Matroid.IsBasis'.contract_isBasis'_diff_diff_of_subset {α : Type u_1} {M : Matroid α} {I J X : Set α} (hIX : M.IsBasis' I X) (hJI : J I) :
      (M.contract J).IsBasis' (I \ J) (X \ J)
      theorem Matroid.IsBasis'.contract_isBasis'_diff_of_subset {α : Type u_1} {M : Matroid α} {I J X : Set α} (hIX : M.IsBasis' I X) (hJI : J I) :
      (M.contract J).IsBasis' (I \ J) X
      theorem Matroid.IsBasis.contract_isBasis_diff_diff_of_subset {α : Type u_1} {M : Matroid α} {I J X : Set α} (hIX : M.IsBasis I X) (hJI : J I) :
      (M.contract J).IsBasis (I \ J) (X \ J)
      theorem Matroid.IsBasis.contract_diff_isBasis_diff {α : Type u_1} {M : Matroid α} {I J X Y : Set α} (hIX : M.IsBasis I X) (hJY : M.IsBasis J Y) (hIJ : I J) :
      (M.contract I).IsBasis (J \ I) (Y \ X)
      theorem Matroid.IsBasis'.contract_isBasis_union_union {α : Type u_1} {M : Matroid α} {I J X : Set α} (h : M.IsBasis' (J I) (X I)) (hJI : Disjoint J I) (hXI : Disjoint X I) :
      (M.contract I).IsBasis' J X
      theorem Matroid.IsBasis.contract_isBasis_union_union {α : Type u_1} {M : Matroid α} {I J X : Set α} (h : M.IsBasis (J I) (X I)) (hJI : Disjoint J I) (hXI : Disjoint X I) :
      (M.contract I).IsBasis J X
      theorem Matroid.IsBasis'.contract_eq_contract_delete {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis' I X) :
      M.contract X = (M.contract I).delete (X \ I)
      theorem Matroid.IsBasis'.contract_indep_iff {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.IsBasis' I X) :
      (M.contract X).Indep J M.Indep (J I) Disjoint X J
      theorem Matroid.IsBasis.contract_indep_iff {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.IsBasis I X) :
      (M.contract X).Indep J M.Indep (J I) Disjoint X J
      theorem Matroid.IsBasis'.contract_dep_iff {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis' I X) {D : Set α} :
      (M.contract X).Dep D M.Dep (D I) Disjoint X D
      theorem Matroid.IsBasis.contract_dep_iff {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis I X) {D : Set α} :
      (M.contract X).Dep D M.Dep (D I) Disjoint X D
      theorem Matroid.IsBasis.contract_indep_iff_of_disjoint {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.IsBasis I X) (hdj : Disjoint X J) :
      (M.contract X).Indep J M.Indep (J I)
      theorem Matroid.IsBasis.contract_indep_diff_iff {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.IsBasis I X) :
      (M.contract X).Indep (J \ X) M.Indep (J \ X I)
      theorem Matroid.IsBasis'.contract_indep_diff_iff {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.IsBasis' I X) :
      (M.contract X).Indep (J \ X) M.Indep (J \ X I)
      theorem Matroid.IsBasis.contract_isBasis_of_isBasis' {α : Type u_1} {M : Matroid α} {I J X C : Set α} (h : M.IsBasis I X) (hJC : M.IsBasis' J C) (h_ind : M.Indep (I \ C J)) :
      (M.contract C).IsBasis (I \ C) (X \ C)
      theorem Matroid.IsBasis'.contract_isBasis' {α : Type u_1} {M : Matroid α} {I J X C : Set α} (h : M.IsBasis' I X) (hJC : M.IsBasis' J C) (h_ind : M.Indep (I \ C J)) :
      (M.contract C).IsBasis' (I \ C) (X \ C)
      theorem Matroid.IsBasis.contract_isBasis {α : Type u_1} {M : Matroid α} {I J X C : Set α} (h : M.IsBasis I X) (hJC : M.IsBasis J C) (h_ind : M.Indep (I \ C J)) :
      (M.contract C).IsBasis (I \ C) (X \ C)
      theorem Matroid.IsBasis.contract_isBasis_of_disjoint {α : Type u_1} {M : Matroid α} {I J X C : Set α} (h : M.IsBasis I X) (hJC : M.IsBasis J C) (hdj : Disjoint C X) (h_ind : M.Indep (I J)) :
      (M.contract C).IsBasis I X
      theorem Matroid.IsBasis'.contract_isBasis_of_indep {α : Type u_1} {M : Matroid α} {I J X : Set α} (h : M.IsBasis' I X) (h_ind : M.Indep (I J)) :
      (M.contract J).IsBasis' (I \ J) (X \ J)
      theorem Matroid.IsBasis.contract_isBasis_of_indep {α : Type u_1} {M : Matroid α} {I J X : Set α} (h : M.IsBasis I X) (h_ind : M.Indep (I J)) :
      (M.contract J).IsBasis (I \ J) (X \ J)
      theorem Matroid.IsBasis.contract_isBasis_of_disjoint_indep {α : Type u_1} {M : Matroid α} {I J X : Set α} (h : M.IsBasis I X) (hdj : Disjoint J X) (h_ind : M.Indep (I J)) :
      (M.contract J).IsBasis I X
      theorem Matroid.Indep.of_contract {α : Type u_1} {M : Matroid α} {I C : Set α} (hI : (M.contract C).Indep I) :
      M.Indep I
      theorem Matroid.Dep.of_contract {α : Type u_1} {M : Matroid α} {X C : Set α} (h : (M.contract C).Dep X) (hC : C M.E := by aesop_mat) :
      M.Dep (C X)

      Finiteness #

      instance Matroid.contract_finite {α : Type u_1} {M : Matroid α} {C : Set α} [M.Finite] :
      instance Matroid.contract_rankFinite {α : Type u_1} {M : Matroid α} {C : Set α} [M.RankFinite] :
      instance Matroid.contract_finitary {α : Type u_1} {M : Matroid α} {C : Set α} [M.Finitary] :

      Loops and Coloops #

      theorem Matroid.contract_eq_delete_of_subset_loops {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X M.loops) :
      M.contract X = M.delete X
      theorem Matroid.contract_eq_delete_of_subset_coloops {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X M.coloops) :
      M.contract X = M.delete X
      @[simp]
      theorem Matroid.contract_isLoop_iff_mem_closure {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} :
      (M.contract C).IsLoop e e M.closure C eC
      @[simp]
      theorem Matroid.contract_loops_eq {α : Type u_1} (M : Matroid α) (C : Set α) :
      (M.contract C).loops = M.closure C \ C
      @[simp]
      theorem Matroid.contract_coloops_eq {α : Type u_1} (M : Matroid α) (C : Set α) :
      @[simp]
      theorem Matroid.contract_isColoop_iff {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} :
      (M.contract C).IsColoop e M.IsColoop e eC
      theorem Matroid.IsNonloop.of_contract {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (h : (M.contract C).IsNonloop e) :
      @[simp]
      theorem Matroid.contract_isNonloop_iff {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} :
      (M.contract C).IsNonloop e e M.E \ M.closure C
      theorem Matroid.IsBasis.diff_subset_loops_contract {α : Type u_1} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis I X) :
      X \ I (M.contract I).loops

      Closure #

      theorem Matroid.contract_closure_eq_contract_delete {α : Type u_1} (M : Matroid α) (C : Set α) :
      M.contract (M.closure C) = (M.contract C).delete (M.closure C \ C)

      Contracting the closure of a set is the same as contracting the set, and then deleting the rest of its elements.

      @[simp]
      theorem Matroid.contract_closure_eq {α : Type u_1} (M : Matroid α) (C X : Set α) :
      (M.contract C).closure X = M.closure (X C) \ C
      theorem Matroid.contract_spanning_iff {α : Type u_1} {M : Matroid α} {X C : Set α} (hC : C M.E := by aesop_mat) :
      theorem Matroid.contract_spanning_iff' {α : Type u_1} {M : Matroid α} {X C : Set α} :
      (M.contract C).Spanning X M.Spanning (X C M.E) Disjoint X C

      A version of Matroid.contract_spanning_iff without the supportedness hypothesis.

      theorem Matroid.Spanning.contract {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Spanning X) (C : Set α) :
      (M.contract C).Spanning (X \ C)
      theorem Matroid.Spanning.contract_eq_loopyOn {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Spanning X) :
      M.contract X = loopyOn (M.E \ X)

      Circuits #

      theorem Matroid.IsCircuit.contract_isCircuit {α : Type u_1} {M : Matroid α} {K C : Set α} (hK : M.IsCircuit K) (hC : C K) :
      (M.contract C).IsCircuit (K \ C)
      theorem Matroid.IsCircuit.contractElem_isCircuit {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (hC : M.IsCircuit C) (hnt : C.Nontrivial) (heC : e C) :
      theorem Matroid.IsCircuit.contract_dep {α : Type u_1} {M : Matroid α} {K C : Set α} (hK : M.IsCircuit K) (hCK : Disjoint C K) :
      (M.contract C).Dep K
      theorem Matroid.IsCircuit.contract_dep_of_not_subset {α : Type u_1} {M : Matroid α} {K : Set α} (hK : M.IsCircuit K) {C : Set α} (hKC : ¬K C) :
      (M.contract C).Dep (K \ C)
      theorem Matroid.IsCircuit.contract_diff_isCircuit {α : Type u_1} {M : Matroid α} {K C : Set α} (hC : M.IsCircuit C) (hK : K.Nonempty) (hKC : K C) :
      (M.contract (C \ K)).IsCircuit K
      theorem Matroid.IsCircuit.exists_subset_isCircuit_of_contract {α : Type u_1} {M : Matroid α} {K C : Set α} (hC : (M.contract K).IsCircuit C) :
      ∃ (C' : Set α), M.IsCircuit C' C C' C' C K

      If C is a circuit of M / K, then M has a circuit in the interval [C, C ∪ K].

      theorem Matroid.IsCocircuit.of_contract {α : Type u_1} {M : Matroid α} {K C : Set α} (hK : (M.contract C).IsCocircuit K) :
      theorem Matroid.IsCocircuit.delete_isCocircuit {α : Type u_1} {M : Matroid α} {K D : Set α} (hK : M.IsCocircuit K) (hD : D K) :
      (M.delete D).IsCocircuit (K \ D)
      theorem Matroid.IsCocircuit.delete_diff_isCocircuit {α : Type u_1} {M : Matroid α} {K X : Set α} (hK : M.IsCocircuit K) (hXK : X K) (hX : X.Nonempty) :
      (M.delete (K \ X)).IsCocircuit X

      Commutativity #

      theorem Matroid.contract_delete_diff {α : Type u_1} (M : Matroid α) (C D : Set α) :
      (M.contract C).delete D = (M.contract C).delete (D \ C)
      theorem Matroid.contract_restrict_eq_restrict_contract {α : Type u_1} {R C : Set α} (M : Matroid α) (h : Disjoint C R) :
      (M.contract C).restrict R = (M.restrict (R C)).contract C
      theorem Matroid.restrict_contract_eq_contract_restrict {α : Type u_1} {R C : Set α} (M : Matroid α) (hCR : C R) :
      (M.restrict R).contract C = (M.contract C).restrict (R \ C)
      theorem Matroid.contract_delete_comm {α : Type u_1} {D C : Set α} (M : Matroid α) (hCD : Disjoint C D) :
      (M.contract C).delete D = (M.delete D).contract C

      Contraction and deletion commute for disjoint sets.

      theorem Matroid.contract_delete_comm' {α : Type u_1} (M : Matroid α) (C D : Set α) :
      (M.contract C).delete D = (M.delete (D \ C)).contract C

      A version of contract_delete_comm without the disjointness hypothesis, and hence a less simple RHS.

      theorem Matroid.delete_contract_eq_diff {α : Type u_1} (M : Matroid α) (D C : Set α) :
      (M.delete D).contract C = (M.delete D).contract (C \ D)
      theorem Matroid.delete_contract_comm' {α : Type u_1} (M : Matroid α) (D C : Set α) :
      (M.delete D).contract C = (M.contract (C \ D)).delete D

      A version of delete_contract_comm' without the disjointness hypothesis, and hence a less simple RHS.

      theorem Matroid.contract_delete_contract' {α : Type u_1} (M : Matroid α) (C D C' : Set α) :
      ((M.contract C).delete D).contract C' = (M.contract (C C' \ D)).delete D

      A version of contract_delete_contract without the disjointness hypothesis, and hence a less simple RHS.

      theorem Matroid.contract_delete_contract {α : Type u_1} (M : Matroid α) (C D C' : Set α) (h : Disjoint C' D) :
      ((M.contract C).delete D).contract C' = (M.contract (C C')).delete D
      theorem Matroid.contract_delete_contract_delete' {α : Type u_1} (M : Matroid α) (C D C' D' : Set α) :
      (((M.contract C).delete D).contract C').delete D' = (M.contract (C C' \ D)).delete (D D')

      A version of contract_delete_contract_delete without the disjointness hypothesis, and hence a less simple RHS.

      theorem Matroid.contract_delete_contract_delete {α : Type u_1} (M : Matroid α) (C D C' D' : Set α) (h : Disjoint C' D) :
      (((M.contract C).delete D).contract C').delete D' = (M.contract (C C')).delete (D D')
      theorem Matroid.delete_contract_delete' {α : Type u_1} (M : Matroid α) (D C D' : Set α) :
      ((M.delete D).contract C).delete D' = (M.contract (C \ D)).delete (D D')

      A version of delete_contract_delete without the disjointness hypothesis, and hence a less simple RHS.

      theorem Matroid.delete_contract_delete {α : Type u_1} (M : Matroid α) (D C D' : Set α) (h : Disjoint C D) :
      ((M.delete D).contract C).delete D' = (M.contract C).delete (D D')