The generic k-frame matroid (def:k-frame-matroid)

Whiteley's general k-frame (Whiteley 1988, The union of matroids and the rigidity of frameworks, SIAM J. Disc. Math. 1, Definition 2.2): for a multigraph G : Graph α β, the matrix with k · |V| columns whose row for a bar e carries indeterminate coefficients across k vertex blocks, each block holding a copy of the signed incidence pattern of e. Its k-frame matroid F(G, X) is the linear matroid of the rows (via Matroid.ofFun, the apnelson1/Matroid constructor LinearRigidityMatroid.lean uses for the planar case), and Whiteley's Theorem 1 identifies it with the union of k copies of the cycle matroid: F(G, X) = (⋃ⱼ G.cycleMatroid) ↾ E(G) (thm:k-frame-union-cycle, kFrameMatroid_eq_unionPow_cycleMatroid). The blueprint presents the file in sec:body-bar-k-frame.

Coefficient encoding

The genericity is realized over true indeterminates, not a real placement (cf. SimpleGraph.linearRigidityMatroid, which is parametrized by a placement p : Framework V d): the coefficient field is

K := FractionRing (MvPolynomial (β × Fin k) ℚ),

with one indeterminate X (e, j) per (bar, block) pair. The row for bar e in block j is X (e, j) • D.signedIncMatrix K e — the indeterminate scaling of the signed incidence row of e for a chosen orientation D of G (the same row vector Graph.cycleMatroidRep represents G.cycleMatroid by). The orientation is picked by G.orientation_nonempty.some, matching cycleMatroidRep; the choice is harmless for the generic matroid (orientations differ only by a per-row sign). The row vector lives in Fin k → α → K, the k-fold copy of the incidence-row space α → K — k · |V|-dimensional, the blueprint's "k vertex blocks".

The two directions of the identification: independent rows on a bar set E' give the count |Y| ≤ k · r(Y) on every Y ⊆ E' by a dimension bound (forest_count_of_linearIndepOn_kFrameRow; Whiteley proves this direction from a nonzero minor instead), and a (k, k)-sparse E' has independent rows by Whiteley's specialization (his proof of Theorem 1, p. 239): on a disjoint forest packing, setting X (e, j) to 1 when e lies in the j-th forest and to 0 otherwise gives a block-diagonal matrix of forest incidence rows (linearIndepOn_kFrameRow_of_isSparse_restrict).

@[reducible, inline]

abbrev Graph.KFrameField (β : Type u_3) (k : ℕ) : Type u_3

The coefficient field of the generic k-frame matroid: the field of fractions of the multivariate polynomial ring MvPolynomial (β × Fin k) ℚ, carrying one indeterminate MvPolynomial.X (e, j) per (bar, block) pair (e, j) : β × Fin k. A field (the fraction field of an integral domain), as Matroid.ofFun requires a DivisionRing.

Equations

• Graph.KFrameField β k = FractionRing (MvPolynomial (β × Fin k) ℚ)

noncomputable def Graph.kFrameIndet {β : Type u_2} (k : ℕ) (e : β) (j : Fin k) : KFrameField β k

The indeterminate X_{(e, j)} of KFrameField β k, the generic coefficient on the incidence row of bar e in vertex block j.

Equations

• Graph.kFrameIndet k e j = (algebraMap (MvPolynomial (β × Fin k) ℚ) (Graph.KFrameField β k)) (MvPolynomial.X (e, j))

noncomputable def Graph.kFrameRow {α : Type u_1} {β : Type u_2} {G : Graph α β} (k : ℕ) (D : G.orientation) : β → Fin k → α → KFrameField β k

The k-frame row function for an orientation D of G: the row for bar e, as a vector in the k · |V|-dimensional space Fin k → α → KFrameField β k, places in each vertex block j the indeterminate scaling X_{(e, j)} • (signed incidence row of e) of e's signed graph-incidence row (Graph.orientation.signedIncMatrix). Off the edge set the signed incidence row is 0, so the row is 0 there.

Equations

• Graph.kFrameRow k D e j = Graph.kFrameIndet k e j • D.signedIncMatrix (Graph.KFrameField β k) e

noncomputable def Graph.kFrameMatroid {α : Type u_1} {β : Type u_2} (G : Graph α β) (k : ℕ) : Matroid β

The generic k-frame matroid F(G, X) of a multigraph G : Graph α β (def:k-frame-matroid; Whiteley 1988, Definition 2.2): the linear matroid on the bar type β, with ground set E(G), of the k-frame row function over the indeterminate coefficient field KFrameField β k. Built via Matroid.ofFun, like the planar SimpleGraph.linearRigidityMatroid. The orientation is picked by G.orientation_nonempty.some, matching Graph.cycleMatroidRep.

The identification kFrameMatroid G k = (Matroid.Union (fun _ : Fin k ↦ G.cycleMatroid)) ↾ E(G) is kFrameMatroid_eq_unionPow_cycleMatroid (thm:k-frame-union-cycle).

Equations

• G.kFrameMatroid k = Matroid.ofFun (Graph.KFrameField β k) G.edgeSet (Graph.kFrameRow k ⋯.some)

@[simp]

theorem Graph.kFrameMatroid_ground {α : Type u_1} {β : Type u_2} (G : Graph α β) (k : ℕ) : (G.kFrameMatroid k).E = G.edgeSet

def Graph.constPiSpanEquiv {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (W : Submodule R M) : ↥(Submodule.pi Set.univ fun (x : Fin n) => W) ≃ₗ[R] Fin n → ↥W

A product subspace as a product (lem:k-frame-pi-finrank): the Fin n-fold constant product subspace Submodule.pi univ (fun _ ↦ W) is linearly equivalent to the plain product Fin n → ↥W of the block submodule with itself. The forward map projects each block; the inverse re-bundles. It gives the dimension count finrank_constPiSpan.

Equations

• One or more equations did not get rendered due to their size.

theorem Graph.finrank_constPiSpan {R : Type u_3} {M : Type u_4} [DivisionRing R] [AddCommGroup M] [Module R M] (n : ℕ) (W : Submodule R M) [Module.Finite R ↥W] : Module.finrank R ↥(Submodule.pi Set.univ fun (x : Fin n) => W) = n * Module.finrank R ↥W

The dimension of a product subspace (lem:k-frame-pi-finrank): the dimension of the constant Fin n-fold product subspace over a division ring R is n times the dimension of the block submodule W. Piece (1) of the rank count of lem:k-frame-nonzero-monomial-forest: applied with W the K-span of the signed incidence rows of a bar set, it turns the blockPiSpanOn upper bound into k · (incidence-span dimension).

noncomputable def Graph.blockPiSpanOn {α : Type u_1} {β : Type u_2} (G : Graph α β) (k : ℕ) (D : G.orientation) (Y : Set β) : Submodule (KFrameField β k) (Fin k → α → KFrameField β k)

The product of incidence spans on a bar set (lem:k-frame-span-le-pi's A_Y^k): the Fin k-fold product subspace whose j-th block is the KFrameField β k-span of the signed incidence rows indexed by a bar set Y. For e ∈ Y the k-frame row kFrameRow k D e lies in this subspace (kFrameRow_mem_blockPiSpanOn), so the span of the k-frame rows on Y is contained in it (span_kFrameRowOn_le_blockPiSpanOn); its K-dimension is k times the dimension of the Y-incidence-row span, i.e. k · r_{cycleMatroid}(Y) — the per-Y upper bound in the rank count of lem:k-frame-nonzero-monomial-forest.

Equations

• G.blockPiSpanOn k D Y = Submodule.pi Set.univ fun (x : Fin k) => Submodule.span (Graph.KFrameField β k) (D.signedIncMatrix (Graph.KFrameField β k) '' Y)

theorem Graph.kFrameRow_mem_blockPiSpanOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ} {D : G.orientation} {Y : Set β} {e : β} (he : e ∈ Y) : kFrameRow k D e ∈ G.blockPiSpanOn k D Y

The k-frame row of a bar of Y lies in blockPiSpanOn G k D Y (lem:k-frame-span-le-pi): in each block j the row is the scalar multiple X_{(e,j)} • signedIncMatrix e, which lies in the span of the incidence rows over Y (since e ∈ Y).

theorem Graph.span_kFrameRowOn_le_blockPiSpanOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ} {D : G.orientation} {Y : Set β} : Submodule.span (KFrameField β k) (kFrameRow k D '' Y) ≤ G.blockPiSpanOn k D Y

The span of the k-frame rows indexed by Y lies in blockPiSpanOn G k D Y (lem:k-frame-span-le-pi).

theorem Matroid.Rep.finrank_span_image_eq_rk {γ : Type u_3} {K : Type u_4} {W : Type u_5} [Field K] [AddCommGroup W] [Module K W] {M : Matroid γ} [M.RankFinite] (v : M.Rep K W) (Y : Set γ) : Module.finrank K ↥(Submodule.span K (⇑v '' Y)) = M.rk Y

Span finrank = matroid rank, via a representation (lem:k-frame-incidence-finrank-rk; piece (2) of lem:k-frame-nonzero-monomial-forest's rank count). For any finite-rank matroid M with a representation v : M.Rep K W, the K-dimension of the span of v '' Y equals the matroid rank M.rk Y. A basis I of Y has v '' Y ⊆ span (v '' I) and LinearIndepOn K v I (Rep.isBasis'_iff), so the two spans coincide; the LI image has finrank = (v '' I).ncard = I.ncard = M.rk Y (finrank_span_set_eq_card + IsBasis'.card).

theorem Graph.finrank_span_signedIncMatrix_eq_cycleMatroid_rk {α : Type u_1} {β : Type u_2} {G : Graph α β} [Finite β] (K : Type u_3) [Field K] (Y : Set β) : Module.finrank K ↥(Submodule.span K (⋯.some.signedIncMatrix K '' Y)) = G.cycleMatroid.rk Y

Incidence-span finrank = cycle-matroid rank (lem:k-frame-incidence-finrank-rk, its second statement; piece (2) of lem:k-frame-nonzero-monomial-forest's rank count). For the orientation G.orientation_nonempty.some underlying cycleMatroidRep (the same one kFrameMatroid uses), the K-dimension of the span of the signed incidence rows indexed by Y equals the cycle-matroid rank G.cycleMatroid.rk Y. This is the cycle-matroid specialization of Matroid.Rep.finrank_span_image_eq_rk to Graph.cycleMatroidRep, whose representation map is exactly signedIncMatrix for that orientation; it turns the finrank blockPiSpanOn = k · (incidence-span finrank) bound of the rank count into k · r_{cycleMatroid}(Y). Stated over any field K, so the body-bar converse uses it over ℝ.

theorem Graph.finrank_blockPiSpanOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ} [Finite β] (Y : Set β) : Module.finrank (KFrameField β k) ↥(G.blockPiSpanOn k ⋯.some Y) = k * G.cycleMatroid.rk Y

The K-dimension of the Y-restricted block-diagonal product subspace is k times the dimension of the Y-incidence-row span, which is k · r_{cycleMatroid}(Y) (a step of lem:k-frame-nonzero-monomial-forest: pieces (1) and (2) of its rank count). Assembled from finrank_constPiSpan and finrank_span_signedIncMatrix_eq_cycleMatroid_rk.

theorem Graph.forest_count_of_linearIndepOn_kFrameRow {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ} [Finite β] {E' : Set β} (hLI : LinearIndepOn (KFrameField β k) (kFrameRow k ⋯.some) E') {Y : Set β} (hYE' : Y ⊆ E') : Y.ncard ≤ k * G.cycleMatroid.rk Y

Generic independence ⟹ the count (lem:k-frame-nonzero-monomial-forest; the direction of Whiteley's Theorem 1 that he proves from a nonzero minor, here by a dimension bound). If the generic k-frame rows on a bar set E' are linearly independent over K, then |Y| ≤ k · r_{cycleMatroid}(Y) for every Y ⊆ E'.

Restricting hLI to Y keeps the |Y| rows independent, so |Y| = finrank (span (kFrameRow '' Y)) (finrank_span_set_eq_card); that span sits inside the Y-restricted block-diagonal product subspace (span_kFrameRowOn_le_blockPiSpanOn), whose dimension is k · r_{cycleMatroid}(Y) (finrank_blockPiSpanOn), giving the bound by Submodule.finrank_mono.

theorem Graph.specRow_linearIndependent {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ} {D : G.orientation} (𝔽 : Type u_3) [Field 𝔽] (Fs : Fin k → Set β) (hFs : ∀ (j : Fin k), G.IsAcyclicSet (Fs j)) : LinearIndependent 𝔽 fun (ji : (j : Fin k) × ↑(Fs j)) => Pi.single ji.fst (D.signedIncMatrix 𝔽 ↑ji.snd)

Block-diagonal specialization of the k-frame rows on a forest packing (lem:k-frame-specialize-li, the linear-algebra core of the converse half of Whiteley's proof of his Theorem 1). Given a k-tuple of acyclic bar sets Fs : Fin k → Set β, the rows obtained by placing, for a bar e ∈ Fs j, the signed incidence row signedIncMatrix D e in block j and 0 elsewhere — i.e. Pi.single j (signedIncMatrix D e) — are linearly independent over any field 𝔽, indexed by the disjoint union Σ j, ↥(Fs j).

This is the specialized-to-full-rank matrix of the converse half: setting the block-j indeterminate X_{(e,j)} to 1 on Fs j and 0 elsewhere turns each generic k-frame row kFrameRow k D e into exactly this block-single row, and the resulting block-diagonal matrix has full row rank because each block is the signed-incidence matrix of a forest (Graph.orientation.isAcyclicSet_linearIndepOn, linearly independent), assembled across blocks by Pi.linearIndependent_single. The step that a specialization of full rank witnesses generic linear independence over K is linearIndepOn_kFrameRow_of_isSparse_restrict.

theorem Graph.linearIndepOn_kFrameRow_iff_over_polyRing {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ} {D : G.orientation} (E' : Set β) : LinearIndepOn (KFrameField β k) (kFrameRow k D) E' ↔ LinearIndepOn (MvPolynomial (β × Fin k) ℚ) (kFrameRow k D) E'

Generic k-frame independence reduces to independence over the polynomial ring (lem:k-frame-li-over-poly-ring, the first half of the genericity-lift step of the converse direction). The coefficient field KFrameField β k = FractionRing (MvPolynomial (β × Fin k) ℚ) is the field of fractions of the polynomial ring R = MvPolynomial (β × Fin k) ℚ, and the k-frame rows of any bar set E' are linearly independent over KFrameField β k iff they are linearly independent over R. This is LinearIndependent.iff_fractionRing applied to the fixed row family in the K-module Fin k → α → KFrameField β k (which is also an R-module via the algebra map, with the scalar tower IsScalarTower R K M inherited from the Pi structure).

The point is to move the remaining nonzero-minor / specialization argument off the fraction field (awkward — no general ring hom extends to it) and onto the integral domain R, where the indeterminate-coefficient minors are honest polynomials. That step — that a forest-packing specialization of full rank witnesses linear independence of the generic rows over R (a nonzero polynomial minor specializing to a nonzero value cannot vanish identically) — is linearIndepOn_kFrameRow_of_isSparse_restrict.

theorem Graph.signedIncMatrix_map {α : Type u_1} {β : Type u_2} {G : Graph α β} {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] [DecidableEq α] [DecidablePred fun (x : β) => x ∈ G.edgeSet] (φ : R →+* S) (D : G.orientation) (e : β) : (fun (x : α) => φ (D.signedIncMatrix R e x)) = D.signedIncMatrix S e

Ring-hom naturality of the signed incidence matrix. The signed incidence row of a bar e has entries in {0, 1, -1}, so applying any ring homomorphism φ : R →+* S entrywise turns signedIncMatrix R e into signedIncMatrix S e. The converse half specializes the indeterminate-coefficient k-frame matrix down to ℚ via an MvPolynomial-evaluation hom; this lemma is what lets that specialization commute past the incidence pattern (which is the same over every ring). Local to this file — a statement about the apnelson1/Matroid-package Graph.orientation.signedIncMatrix, not a mathlib fact.

noncomputable def Graph.kFrameRowR {α : Type u_1} {β : Type u_2} {G : Graph α β} (k : ℕ) (D : G.orientation) : β → Fin k → α → MvPolynomial (β × Fin k) ℚ

The k-frame row function over the polynomial ring R = MvPolynomial (β × Fin k) ℚ (lem:k-frame-specialize-identity's R-valued rows): the row for bar e places in each vertex block j the indeterminate scaling X_{(e, j)} • signedIncMatrix R e of e's signed incidence row. This is the R-valued analogue of kFrameRow (which is its image under algebraMap R (KFrameField β k), by kFrameRow_eq_map_kFrameRowR); moving the row family onto the integral domain R is what makes the converse half's determinant / specialization argument (over R, then φ-specialized to ℚ) available.

Equations

• Graph.kFrameRowR k D e j = MvPolynomial.X (e, j) • D.signedIncMatrix (MvPolynomial (β × Fin k) ℚ) e

theorem Graph.kFrameRow_eq_map_kFrameRowR {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ} {D : G.orientation} (e : β) : kFrameRow k D e = fun (j : Fin k) (x : α) => (algebraMap (MvPolynomial (β × Fin k) ℚ) (KFrameField β k)) (kFrameRowR k D e j x)

The generic k-frame row kFrameRow k D e is the image of the polynomial-ring row kFrameRowR k D e under algebraMap R (KFrameField β k) applied entrywise. Both the indeterminate coefficient X_{(e, j)} (kFrameIndet, defined as algebraMap … (X (e, j))) and the incidence pattern (signedIncMatrix_map) push through the algebra map, so the two rows agree. This is the bridge that lets linearIndepOn_kFrameRow_iff_over_polyRing be combined with an R-level independence argument.

noncomputable def Graph.forestEval {β : Type u_2} {k : ℕ} (Fs : Fin k → Set β) : MvPolynomial (β × Fin k) ℚ →+* ℚ

The forest-packing specialization homomorphism R →+* ℚ of a k-tuple Fs : Fin k → Set β (lem:k-frame-specialize-identity's φ): the MvPolynomial-evaluation sending each indeterminate X_{(e, j)} to 1 if e ∈ Fs j and 0 otherwise. Specializing the polynomial-ring k-frame matrix kFrameRowR along this hom turns the generic rows into the block-diagonal forest matrix of specRow_linearIndependent (forestEval_kFrameRowR_eq_single).

Equations

• Graph.forestEval Fs = MvPolynomial.eval fun (p : β × Fin k) => if p.1 ∈ Fs p.2 then 1 else 0

theorem Graph.forestEval_kFrameRowR_eq_single {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ} {D : G.orientation} (Fs : Fin k → Set β) (hdisj : Pairwise (Function.onFun Disjoint Fs)) {e : β} {j₀ : Fin k} (he : e ∈ Fs j₀) : (fun (j : Fin k) (x : α) => (forestEval Fs) (kFrameRowR k D e j x)) = Pi.single j₀ (D.signedIncMatrix ℚ e)

The forest-packing specialization sends kFrameRowR to the block-single row (lem:k-frame-specialize-identity, the specialization identity of the converse half). For a disjoint k-forest packing Fs and a bar e ∈ Fs j₀, applying forestEval Fs entrywise to the polynomial-ring row kFrameRowR k D e yields exactly Pi.single j₀ (signedIncMatrix ℚ e) — the block-single row that specRow_linearIndependent proves linearly independent. In block j₀ the coefficient X_{(e, j₀)} evaluates to 1 (as e ∈ Fs j₀), leaving the real signed incidence row; in every other block j ≠ j₀ disjointness gives e ∉ Fs j, so X_{(e, j)} evaluates to 0 and the block vanishes. Incidence-pattern commutation with the evaluation hom is signedIncMatrix_map. With the minor-nonvanishing engine Matrix.linearIndependent_rows_of_specialized_submatrix_det_ne_zero, this identity finishes the converse half.

theorem Graph.linearIndepOn_kFrameRow_of_isSparse_restrict {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ} [Finite α] [Finite β] {E' : Set β} (hE' : E' ⊆ G.edgeSet) (hsparse : (G.restrict E').IsSparse k k) : LinearIndepOn (KFrameField β k) (kFrameRow k ⋯.some) E'

Forest decomposition ⟹ generic independence (lem:k-frame-specialize-forest, the converse half of Whiteley's proof of his Theorem 1, 1988, p. 239). If the edge-restriction G ↾ E' is (k, k)-sparse, then the generic k-frame rows on E' are linearly independent over the coefficient field K = KFrameField β k.

The proof combines the converse-half lemmas. By linearIndepOn_kFrameRow_iff_over_polyRing it suffices to argue over the polynomial ring R = MvPolynomial (β × Fin k) ℚ, and via kFrameRow_eq_map_kFrameRowR (the generic row is the entrywise algebraMap R K-image of the R-valued row kFrameRowR) over the R-valued rows. Those are passed, in uncurried Fin k × α matrix form, to the minor-nonvanishing engine Matrix.linearIndependent_rows_of_specialized_submatrix_det_ne_zero with the forest-packing evaluation hom forestEval Fs (Fs a disjoint forest packing covering E', from exists_forestPacking_cover_of_isSparse_restrict): by forestEval_kFrameRowR_eq_single the specialized rows are the block-single forest matrix, which is LI over ℚ (specRow_linearIndependent, reindexed along the disjoint-cover bijection Set.unionEqSigmaOfDisjoint), so it has a nonsingular maximal minor (Matrix.exists_submatrix_det_ne_zero_of_linearIndependent_rows) — the nonzero specialized determinant the engine takes.

theorem Graph.kFrameMatroid_indep_iff_isSparse_restrict {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ} [Finite α] [Finite β] {E' : Set β} (hE' : E' ⊆ G.edgeSet) : (G.kFrameMatroid k).Indep E' ↔ (G.restrict E').IsSparse k k

Generic k-frame independence by the count (lem:k-frame-indep-iff-count). A bar set E' ⊆ E(G) is independent in the generic k-frame matroid F(G, X) if and only if the edge-restriction G ↾ E' is (k, k)-sparse. The two directions of Whiteley's Theorem 1, by lem:k-frame-nonzero-monomial-forest and lem:k-frame-specialize-forest: the Matroid.ofFun independence predicate unfolds to linear independence of the generic k-frame rows on E', the forward direction (forest_count_of_linearIndepOn_kFrameRow) reads off the count ∀ Y ⊆ E', |Y| ≤ k · r_{cycleMatroid}(Y), and the converse (linearIndepOn_kFrameRow_of_isSparse_restrict) recovers linear independence from sparsity. The count is exactly what unionPow_cycleMatroid_indep_iff_isSparse_restrict (via Matroid.Union_pow_indep_iff_count) attaches to (k, k)-sparsity, which is what makes thm:k-frame-union-cycle collapse to matroid extensionality.

theorem Graph.kFrameMatroid_eq_unionPow_cycleMatroid {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ} [DecidableEq β] [Finite α] [Finite β] : G.kFrameMatroid k = (Matroid.Union fun (x : Fin k) => G.cycleMatroid).restrict G.edgeSet

The generic k-frame matroid is the k-fold cycle-matroid union (thm:k-frame-union-cycle; Whiteley 1988, Theorem 1). For every multigraph G : Graph α β and k, the generic k-frame matroid F(G, X) equals the k-fold union ⋃ⱼ G.cycleMatroid of the cycle matroid, restricted to the bar set E(G). Both sides are matroids on the edge type β with ground set E(G).

The ↾ E(G) is bookkeeping forced by the ground-set convention of the vendored Matroid.Union (Matroid.Union Ms = (Matroid.sum' Ms).adjMap _ univ, so its ground set is univ : Set β, not E(G) — elements of univ \ E(G) sit in the union as loops). Restricting to E(G) discards those loops and recovers the ground set E(G) of kFrameMatroid (Matroid.ofFun … E(G) …). On E' ⊆ E(G) both sides are independent exactly when G ↾ E' is (k, k)-sparse: the kFrameMatroid side is kFrameMatroid_indep_iff_isSparse_restrict (both directions), the union side is unionPow_cycleMatroid_indep_iff_isSparse_restrict, so the equality is Matroid.ext_indep.