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

• Matroid.contract M C, written M ／ C, is the matroid on ground set M.E \ C in which a set I ⊆ M.E \ C is independent if and only if I ∪ J is independent in M, where J is an arbitrary basis for C.
• Matroid.contract_dual M C : (M ／ X)✶ = M✶ ＼ X; the dual of contraction is deletion.
• Matroid.delete_dual M C : (M ＼ X)✶ = M✶ ／ X; the dual of deletion is contraction.
• Matroid.IsBasis.contract_indep_iff; if I is a basis for C, then the independent sets of M ／ C are exactly the J ⊆ M.E \ C for which I ∪ J is independent in M.
• Matroid.contract_delete_comm : M ／ C ＼ D = M ＼ D ／ C for disjoint C and D.

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 α) : Matroid α

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

• M.contract C = (M✶.delete C)✶

def Matroid.«term_／_» : Lean.TrailingParserDescr

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

Equations

• Matroid.«term_／_» = Lean.ParserDescr.trailingNode `Matroid.«term_／_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ／ ") (Lean.ParserDescr.cat `term 76))

@[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 α) : (M✶.delete X)✶ = M.contract X

@[simp]

theorem Matroid.dual_delete {α : Type u_1} (M : Matroid α) (X : Set α) : (M.delete X)✶ = M✶.contract X

@[simp]

theorem Matroid.dual_contract {α : Type u_1} (M : Matroid α) (X : Set α) : (M.contract X)✶ = M✶.delete X

theorem Matroid.dual_contract_dual {α : Type u_1} (M : Matroid α) (X : Set α) : (M✶.contract X)✶ = M.delete X

@[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 α) : ((M.contract X).delete Y)✶ = (M✶.delete X).contract Y

theorem Matroid.dual_delete_contract {α : Type u_1} (M : Matroid α) (X Y : Set α) : ((M.delete X).contract Y)✶ = (M✶.contract X).delete Y

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 : e ∉ M.E) : M.contract {e} = M

@[simp]

theorem Matroid.contract_empty {α : Type u_1} (M : Matroid α) : M.contract ∅ = M

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 α} : (M.contract C).Coindep X ↔ M.Coindep X ∧ Disjoint X C

theorem Matroid.Coindep.coindep_contract_of_disjoint {α : Type u_1} {M : Matroid α} {X C : Set α} (hX : M.Coindep X) (hXC : Disjoint X C) : (M.contract C).Coindep X

@[simp]

theorem Matroid.contract_isCocircuit_iff {α : Type u_1} {M : Matroid α} {K C : Set α} : (M.contract C).IsCocircuit K ↔ M.IsCocircuit K ∧ Disjoint K C

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 ↔ e ∉ I ∧ 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] : (M.contract C).Finite

instance Matroid.contract_rankFinite {α : Type u_1} {M : Matroid α} {C : Set α} [M.RankFinite] : (M.contract C).RankFinite

instance Matroid.contract_finitary {α : Type u_1} {M : Matroid α} {C : Set α} [M.Finitary] : (M.contract C).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 ∧ e ∉ C

@[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 α) : (M.contract C).coloops = M.coloops \ C

@[simp]

theorem Matroid.contract_isColoop_iff {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} : (M.contract C).IsColoop e ↔ M.IsColoop e ∧ e ∉ C

theorem Matroid.IsNonloop.of_contract {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (h : (M.contract C).IsNonloop e) : M.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) : (M.contract C).Spanning X ↔ M.Spanning (X ∪ C) ∧ Disjoint X C

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) : (M.contract {e}).IsCircuit (C \ {e})

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) : M.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')