Matroid Closure #
A Flat
of a matroid M
is a combinatorial analogue of a subspace of a vector space,
and is defined to be a subset F
of the ground set of M
such that for each basis
I
for M
, every set having I
as a basis is contained in F
.
The closure of a set X
in a matroid M
is the intersection of all flats of M
containing X
.
This is a combinatorial analogue of the linear span of a set of vectors.
For M : Matroid α
, this file defines a predicate M.Flat : Set α → Prop
and a function
M.closure : Set α → Set α
corresponding to these notions, and develops API for the latter.
API for Matroid.Flat
will appear in another file; we include the definition here since
it is used in the definition of Matroid.closure
.
Main definitions #
- For
M : Matroid α
andF : Set α
,M.Flat F
means thatF
is a flat ofM
. - For
M : Matroid α
andX : Set α
,M.closure X
is the closure ofX
inM
. - For
M : Matroid α
andX : ↑(Iic M.E)
(i.e. a bundled subset ofM.E
),M.subtypeClosure X
is the closure ofX
, viewed as a term in↑(Iic M.E)
. This is aClosureOperator
on↑(Iic M.E)
.
Implementation details #
If X : Set α
satisfies X ⊆ M.E
, then it is clear how M.closure X
should be defined.
But M.closure X
also needs to be defined for all X : Set α
,
so a convention is needed for how it handles sets containing junk elements outside M.E
.
All such choices come with tradeoffs. Provided that M.closure X
has already been defined
for X ⊆ M.E
, the two best candidates for extending it to all X
seem to be:
(1) The function for which M.closure X = M.closure (X ∩ M.E)
for all X : Set α
(2) The function for which M.closure X = M.closure (X ∩ M.E) ∪ X
for all X : Set α
For both options, the function closure
is monotone and idempotent with no assumptions on X
.
Choice (1) has the advantage that M.closure X ⊆ M.E
holds for all X
without the assumption
that X ⊆ M.E
, which is very nice for aesop_mat
. It is also fairly convenient to rewrite
M.closure X
to M.closure (X ∩ M.E)
when one needs to work with a subset of the ground set.
Its disadvantage is that the statement X ⊆ M.closure X
is only true provided that X ⊆ M.E
.
Choice (2) has the reverse property: we would have X ⊆ M.closure X
for all X
,
but the condition M.closure X ⊆ M.E
requires X ⊆ M.E
to hold.
It has a couple of other advantages too: it is actually the closure function of a matroid on α
with ground set univ
(specifically, the direct sum of M
and a free matroid on M.Eᶜ
),
and because of this, it is an example of a ClosureOperator
on α
, which in turn gives access
to nice existing API for both ClosureOperator
and GaloisInsertion
.
This also relates to flats; F ⊆ M.E ∧ ClosureOperator.IsClosed F
is equivalent to M.Flat F
.
(All of this fails for choice (1), since X ⊆ M.closure X
is required for
a ClosureOperator
, but isn't true for non-subsets of M.E
)
The API that choice (2) would offer is very beguiling, but after extensive experimentation in
an external repo, it seems that (1) is far less rough around the edges in practice,
so we go with (1). It may be helpful at some point to define a primed version
Matroid.closure' : ClosureOperator (Set α)
corresponding to choice (2).
Failing that, the ClosureOperator
/GaloisInsertion
API is still available on
the subtype ↑(Iic M.E)
via Matroid.SubtypeClosure
, albeit less elegantly.
The property of being a flat gives rise to a ClosureOperator
on the subsets of M.E
,
in which the IsClosed
sets correspond to Flat
s.
(We can't define such an operator on all of Set α
,
since this would incorrectly force univ
to always be a flat.)
Equations
- M.subtypeClosure = ClosureOperator.ofCompletePred (fun (F : ↑(Set.Iic M.E)) => M.Flat ↑F) ⋯
Instances For
For a nonempty collection of subsets of a given independent set, the closure of the intersection is the intersection of the closure.