structure Matroid.Quotient {α : Type u_1} (M N : Matroid α) : Prop

TODO: rename IsQuotient.

• forall_isFlat_of_isFlat (F : Set α) : M.IsFlat F → N.IsFlat F
• ground_eq : M.E = N.E

theorem Matroid.quotient_iff {α : Type u_1} (M N : Matroid α) : M ≤q N ↔ (∀ (F : Set α), M.IsFlat F → N.IsFlat F) ∧ M.E = N.E

def Matroid.«term_≤q_» : Lean.TrailingParserDescr

Equations

• Matroid.«term_≤q_» = Lean.ParserDescr.trailingNode `Matroid.«term_≤q_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤q ") (Lean.ParserDescr.cat `term 51))

theorem Matroid.Quotient.ground_eq_of_dual {α : Type u_1} {M N : Matroid α} (h : N✶ ≤q M✶) : N.E = M.E

theorem Matroid.Quotient.isFlat_of_isFlat {α : Type u_1} {M N : Matroid α} {F : Set α} (h : M ≤q N) (hF : M.IsFlat F) : N.IsFlat F

theorem Matroid.Quotient.trans {α : Type u_1} {M₁ M₂ M₃ : Matroid α} (h : M₁ ≤q M₂) (h' : M₂ ≤q M₃) : M₁ ≤q M₃

theorem Matroid.Quotient.refl {α : Type u_1} (M : Matroid α) : M ≤q M

theorem Matroid.Quotient.antisymm {α : Type u_1} {M₁ M₂ : Matroid α} (h : M₁ ≤q M₂) (h' : M₂ ≤q M₁) : M₁ = M₂

theorem Matroid.Quotient.closure_subset_closure {α : Type u_1} {M N : Matroid α} (h : M ≤q N) (X : Set α) : N.closure X ⊆ M.closure X

theorem Matroid.Quotient.weakLE {α : Type u_1} {M N : Matroid α} (h : N ≤q M) : N ≤w M

theorem Matroid.quotient_of_forall_closure_subset_closure {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (hQ : ∀ X ⊆ M₁.E, M₁.closure X ⊆ M₂.closure X) : M₂ ≤q M₁

theorem Matroid.quotient_of_forall_closure_subset_closure_indep {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (hQ : ∀ (I : Set α), M₁.Indep I → M₁.closure I ⊆ M₂.closure I) : M₂ ≤q M₁

theorem Matroid.Quotient.closure_closure_eq_closure_right {α : Type u_1} {M₁ M₂ : Matroid α} (h : M₂ ≤q M₁) (X : Set α) : M₂.closure (M₁.closure X) = M₂.closure X

theorem Matroid.Quotient.closure_closure_eq_closure_left {α : Type u_1} {M₁ M₂ : Matroid α} (h : M₂ ≤q M₁) (X : Set α) : M₁.closure (M₂.closure X) = M₂.closure X

theorem Matroid.Quotient.cyclic_of_isCircuit {α : Type u_1} {M₁ M₂ : Matroid α} (hQ : M₂ ≤q M₁) {C : Set α} (hC : M₁.IsCircuit C) : M₂.Cyclic C

If M₂ ≤q M₁, then every circuit of M₁ is cyclic (a union of circuits) in M₂.

theorem Matroid.quotient_of_forall_cyclic_of_isCircuit {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (h : ∀ (C : Set α), M₁.IsCircuit C → M₂.Cyclic C) : M₂ ≤q M₁

If every circuit of M₁ is cyclic (a union of circuits) in M₂, then M₂ ≤q M₁.

theorem Matroid.Quotient.dual {α : Type u_1} {M₁ M₂ : Matroid α} (hQ : M₂ ≤q M₁) : M₁✶ ≤q M₂✶

theorem Matroid.Quotient.of_dual {α : Type u_1} {M₁ M₂ : Matroid α} (hQ : M₂✶ ≤q M₁✶) : M₁ ≤q M₂

@[simp]

theorem Matroid.quotient_dual_iff {α : Type u_1} {M₁ M₂ : Matroid α} : M₁✶ ≤q M₂✶ ↔ M₂ ≤q M₁

theorem Matroid.Quotient.spanning_of_spanning {α : Type u_1} {M₁ M₂ : Matroid α} (hQ : M₂ ≤q M₁) {S : Set α} (hS : M₁.Spanning S) : M₂.Spanning S

theorem Matroid.Quotient.nonspanning_of_nonspanning {α : Type u_1} {M₁ M₂ : Matroid α} (hQ : M₂ ≤q M₁) {S : Set α} (hS : M₂.Nonspanning S) : M₁.Nonspanning S

theorem Matroid.Quotient.contract {α : Type u_1} {M₁ M₂ : Matroid α} (hQ : M₂ ≤q M₁) (C : Set α) : M₂.contract C ≤q M₁.contract C

theorem Matroid.Quotient.delete {α : Type u_1} {M₁ M₂ : Matroid α} (hQ : M₂ ≤q M₁) (D : Set α) : M₂.delete D ≤q M₁.delete D

theorem Matroid.contract_quotient_delete {α : Type u_1} (N : Matroid α) (X : Set α) : N.contract X ≤q N.delete X

theorem Matroid.Quotient.restrict {α : Type u_1} {M₁ M₂ : Matroid α} (hQ : M₂ ≤q M₁) (R : Set α) : M₂.restrict R ≤q M₁.restrict R

theorem Matroid.Quotient.eRelRk_le {α : Type u_1} {M₁ M₂ : Matroid α} (hQ : M₂ ≤q M₁) (X Y : Set α) : M₂.eRelRk X Y ≤ M₁.eRelRk X Y

theorem Matroid.quotient_of_forall_eRelRk_le {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (hYZ : ∀ (Y Z : Set α), Y ⊆ Z → Z ⊆ M₁.E → M₂.eRelRk Y Z ≤ M₁.eRelRk Y Z) : M₂ ≤q M₁

theorem Matroid.TFAE_quotient {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) : [M₂ ≤q M₁, ∀ (Y Z : Set α), Y ⊆ Z → Z ⊆ M₁.E → M₂.eRelRk Y Z ≤ M₁.eRelRk Y Z, ∀ X ⊆ M₁.E, M₁.closure X ⊆ M₂.closure X, ∀ (C : Set α), M₁.IsCircuit C → M₂.Cyclic C, M₁✶ ≤q M₂✶].TFAE

theorem Matroid.Quotient.rankFinite {α : Type u_1} {M₁ M₂ : Matroid α} [hM₁ : M₁.RankFinite] (hQ : M₂ ≤q M₁) : M₂.RankFinite

theorem Matroid.Quotient.eq_of_isBase_indep {α : Type u_1} {M₁ M₂ : Matroid α} [M₂.Finitary] (hQ : M₂ ≤q M₁) {B : Set α} (hB₁ : M₁.IsBase B) (hB₂ : M₂.Indep B) : M₂ = M₁

If M₂ is a finitary quotient of a matroid M₁, and some base of M₁ is independent in M₂, then M₁ = M₂. This is not true for general matroids; see Matroid.TruncateFamily.

theorem Matroid.Quotient.eq_of_spanning_indep {α : Type u_1} {M₁ M₂ : Matroid α} {X : Set α} [M₂.Finitary] (h : M₂ ≤q M₁) (hs : M₁.Spanning X) (hi : M₂.Indep X) : M₂ = M₁

theorem Matroid.Quotient.eq_of_closure_indep {α : Type u_1} {M₁ M₂ : Matroid α} {X : Set α} [M₂.Finitary] (h : M₂ ≤q M₁) (hcl : M₁.E ⊆ M₁.closure X) (hi : M₂.Indep X) : M₂ = M₁

theorem Matroid.Quotient.eq_of_eRank_ge {α : Type u_1} {M₁ M₂ : Matroid α} [M₂.RankFinite] (h : M₂ ≤q M₁) (hge : M₁.eRank ≤ M₂.eRank) : M₂ = M₁

theorem Matroid.Quotient.eq_of_eRank_ge' {α : Type u_1} {M₁ M₂ : Matroid α} [M₁.RankFinite] (h : M₂ ≤q M₁) (hge : M₁.eRank ≤ M₂.eRank) : M₂ = M₁

theorem Matroid.Quotient.map {α : Type u_1} {M₁ M₂ : Matroid α} {β : Type u_2} {f : α → β} (hQ : M₂ ≤q M₁) (hf : Set.InjOn f M₂.E) : M₂.map f hf ≤q M₁.map f ⋯

theorem Matroid.Quotient.comap {α : Type u_1} {β : Type u_2} {M₂ M₁ : Matroid β} (hQ : M₂ ≤q M₁) (f : α → β) : M₂.comap f ≤q M₁.comap f

theorem Matroid.Quotient.intCast_rank_sub_mono {α : Type u_1} {M₁ M₂ : Matroid α} {X Y : Set α} [M₁.RankFinite] (hQ : M₂ ≤q M₁) (hXY : X ⊆ Y) : ↑(M₂.rk Y) - ↑(M₂.rk X) ≤ ↑(M₁.rk Y) - ↑(M₁.rk X)

theorem Matroid.Quotient.rank_sub_mono {α : Type u_1} {M₁ M₂ : Matroid α} {X Y : Set α} [M₁.RankFinite] (hQ : M₂ ≤q M₁) (hXY : X ⊆ Y) : ↑(M₁.rk X) - ↑(M₂.rk X) ≤ ↑(M₁.rk Y) - ↑(M₂.rk Y)

theorem Matroid.Quotient.wcovBy_of_covBy {α : Type u_1} {M₁ M₂ : Matroid α} {F F' : Set α} (hQ : M₂ ≤q M₁) (hco : F ⋖[M₁] F') : M₂.closure F ⩿[M₂] M₂.closure F'

theorem Matroid.exists_project_indep_coindep {α : Type u_1} (P : Matroid α) (X : Set α) : ∃ (Q : Matroid α) (Y : Set α), Q.Indep Y ∧ Q.Coindep Y ∧ Q.contract Y = P.contract X ∧ Q.delete Y = P.delete X

If there exist P and X so that M = P ＼ X and N = P ／ X, then we can choose such a P and X so that X is independent and coindependent in P.