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
, writtenM / C
, is the matroid on ground setM.E \ C
in which a setI ⊆ M.E \ C
is independent if and only ifI ∪ J
is independent inM
, whereJ
is an arbitrary basis forC
.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
; ifI
is a basis forC
, then the independent sets ofM / C
are exactly theJ ⊆ M.E \ C
for whichI ∪ J
is independent inM
.Matroid.contract_delete_comm
:M / C \ D = M \ D / C
for disjointC
andD
.
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 α
.
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.
Instances For
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))
Instances For
Independence and Coindependence #
Bases #
Finiteness #
Loops and Coloops #
Closure #
Circuits #
Commutativity #
A version of contract_delete_contract_delete
without the disjointness hypothesis,
and hence a less simple RHS.