structure Matroid.ModularCut {α : Type u_1} (M : Matroid α) : Type u_1

A ModularCut M is a collection of flats of M that is closed under taking superflats and under intersections of modular families. These parametrize the extensions of M by a single element outside M and hence also the projections of M; see Matroid.extendBy and Matroid.projectBy.

• carrier : Set (Set α)
• forall_isFlat (F : Set α) : F ∈ self.carrier → M.IsFlat F
• forall_superset (F F' : Set α) : F ∈ self.carrier → M.IsFlat F' → F ⊆ F' → F' ∈ self.carrier
• forall_inter (Fs : Set (Set α)) : Fs ⊆ self.carrier → Fs.Nonempty → (M.IsModularFamily fun (x : ↑Fs) => ↑x) → ⋂₀ Fs ∈ self.carrier

@[instance_reducible]

instance Matroid.ModularCut.instSetLikeSet {α : Type u_1} (M : Matroid α) : SetLike M.ModularCut (Set α)

Equations

• Matroid.ModularCut.instSetLikeSet M = { coe := Matroid.ModularCut.carrier, coe_injective := ⋯ }

@[simp]

theorem Matroid.ModularCut.mem_carrier_iff {α : Type u_1} {M : Matroid α} {F : Set α} {U : M.ModularCut} : F ∈ U.carrier ↔ F ∈ U

theorem Matroid.ModularCut.isFlat_of_mem {α : Type u_1} {M : Matroid α} {F : Set α} (U : M.ModularCut) (hF : F ∈ U) : M.IsFlat F

theorem Matroid.ModularCut.subset_ground {α : Type u_1} {M : Matroid α} {F : Set α} (U : M.ModularCut) (hF : F ∈ U) : F ⊆ M.E

theorem Matroid.ModularCut.superset_mem {α : Type u_1} {M : Matroid α} {F F' : Set α} (U : M.ModularCut) (hF : F ∈ U) (hF' : M.IsFlat F') (hFF' : F ⊆ F') : F' ∈ U

theorem Matroid.ModularCut.ext {α : Type u_1} {M : Matroid α} {U U' : M.ModularCut} (h : ∀ (F : Set α), M.IsFlat F → (F ∈ U ↔ F ∈ U')) : U = U'

theorem Matroid.ModularCut.ext_iff {α : Type u_1} {M : Matroid α} {U U' : M.ModularCut} : U = U' ↔ ∀ (F : Set α), M.IsFlat F → (F ∈ U ↔ F ∈ U')

def Matroid.ModularCut.copy {α : Type u_1} {M N : Matroid α} (U : M.ModularCut) (hNM : M = N) : N.ModularCut

Transfer a ModularCut across a matroid equality.

Equations

• U.copy hNM = { carrier := ↑U, forall_isFlat := ⋯, forall_superset := ⋯, forall_inter := ⋯ }

@[simp]

theorem Matroid.ModularCut.mem_copy_iff {α : Type u_1} {M : Matroid α} {F : Set α} {N : Matroid α} (U : M.ModularCut) {hNM : M = N} : F ∈ U.copy hNM ↔ F ∈ U

def Matroid.ModularCut.map {α : Type u_1} {M : Matroid α} {β : Type u_2} (U : M.ModularCut) (f : α → β) (hf : Set.InjOn f M.E) : (M.map f hf).ModularCut

Transfer a ModularCut along an injection

Equations

• U.map f hf = { carrier := Set.image f '' ↑U, forall_isFlat := ⋯, forall_superset := ⋯, forall_inter := ⋯ }

@[simp]

theorem Matroid.ModularCut.mem_map_iff {α : Type u_1} {M : Matroid α} {β : Type u_2} (U : M.ModularCut) (f : α → β) (hf : Set.InjOn f M.E) {F : Set β} : F ∈ U.map f hf ↔ ∃ F₀ ∈ U, f '' F₀ = F

theorem Matroid.ModularCut.image_mem_map_iff {α : Type u_1} {M : Matroid α} {β : Type u_2} (U : M.ModularCut) (f : α → β) (hf : Set.InjOn f M.E) {F : Set α} (hF : F ⊆ M.E) : f '' F ∈ U.map f hf ↔ F ∈ U

@[simp]

theorem Matroid.ModularCut.mem_mk_iff {α : Type u_1} {M : Matroid α} (S : Set (Set α)) (h₁ : ∀ F ∈ S, M.IsFlat F) (h₂ : ∀ (F F' : Set α), F ∈ S → M.IsFlat F' → F ⊆ F' → F' ∈ S) (h₃ : ∀ Fs ⊆ S, Fs.Nonempty → (M.IsModularFamily fun (x : ↑Fs) => ↑x) → ⋂₀ Fs ∈ S) {X : Set α} : X ∈ { carrier := S, forall_isFlat := h₁, forall_superset := h₂, forall_inter := h₃ } ↔ X ∈ S

theorem Matroid.ModularCut.closure_superset_mem {α : Type u_1} {M : Matroid α} {F X : Set α} (U : M.ModularCut) (hF : F ∈ U) (hFX : F ⊆ M.closure X) : M.closure X ∈ U

theorem Matroid.ModularCut.closure_superset_mem' {α : Type u_1} {M : Matroid α} {X Y : Set α} (U : M.ModularCut) (hX : M.closure X ∈ U) (hXY : X ⊆ Y) : M.closure Y ∈ U

theorem Matroid.ModularCut.sInter_mem {α : Type u_1} {M : Matroid α} (U : M.ModularCut) {Fs : Set (Set α)} (hne : Fs.Nonempty) (hFs : Fs ⊆ ↑U) (hFs_mod : M.IsModularFamily fun (F : ↑Fs) => ↑F) : ⋂₀ Fs ∈ U

theorem Matroid.ModularCut.iInter_mem {α : Type u_1} {M : Matroid α} (U : M.ModularCut) {ι : Type u_2} [Nonempty ι] (Fs : ι → Set α) (hFs : ∀ (i : ι), Fs i ∈ U) (hFs_mod : M.IsModularFamily Fs) : ⋂ (i : ι), Fs i ∈ U

theorem Matroid.ModularCut.inter_mem {α : Type u_1} {M : Matroid α} {F F' : Set α} (U : M.ModularCut) (hF : F ∈ U) (hF' : F' ∈ U) (h : M.IsModularPair F F') : F ∩ F' ∈ U

theorem Matroid.ModularCut.closure_mem_of_mem {α : Type u_1} {M : Matroid α} {F : Set α} {U : M.ModularCut} (hF : F ∈ U) : M.closure F ∈ U

def Matroid.ModularCut.principal {α : Type u_1} (M : Matroid α) (X : Set α) : M.ModularCut

The ModularCut of all flats containing X ∩ M.E.

Equations

• Matroid.ModularCut.principal M X = { carrier := {F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F}, forall_isFlat := ⋯, forall_superset := ⋯, forall_inter := ⋯ }

@[simp]

theorem Matroid.ModularCut.principal_carrier {α : Type u_1} (M : Matroid α) (X : Set α) : ↑(principal M X) = {F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F}

theorem Matroid.ModularCut.mem_principal_iff' {α : Type u_1} {M : Matroid α} {F X : Set α} : F ∈ principal M X ↔ M.IsFlat F ∧ X ∩ M.E ⊆ F

theorem Matroid.ModularCut.mem_principal_iff {α : Type u_1} {M : Matroid α} {F X : Set α} (hX : X ⊆ M.E := by aesop_mat) : F ∈ principal M X ↔ M.IsFlat F ∧ X ⊆ F

@[simp]

theorem Matroid.ModularCut.closure_mem_principal_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : X ⊆ M.E := by aesop_mat) : M.closure Y ∈ principal M X ↔ X ⊆ M.closure Y

@[simp]

theorem Matroid.ModularCut.closure_mem_principal {α : Type u_1} (M : Matroid α) (X : Set α) : M.closure X ∈ principal M X

@[simp]

theorem Matroid.ModularCut.principal_inter_ground {α : Type u_1} (M : Matroid α) (X : Set α) : principal M (X ∩ M.E) = principal M X

@[simp]

theorem Matroid.ModularCut.principal_closure_eq {α : Type u_1} (M : Matroid α) (X : Set α) : principal M (M.closure X) = principal M X

def Matroid.ModularCut.empty {α : Type u_1} (M : Matroid α) : M.ModularCut

The empty modular cut

Equations

• Matroid.ModularCut.empty M = { carrier := ∅, forall_isFlat := ⋯, forall_superset := ⋯, forall_inter := ⋯ }

@[simp]

theorem Matroid.ModularCut.empty_carrier {α : Type u_1} (M : Matroid α) : ↑(ModularCut.empty M) = ∅

@[instance_reducible]

instance Matroid.ModularCut.instPartialOrder {α : Type u_1} (M : Matroid α) : PartialOrder M.ModularCut

Equations

• Matroid.ModularCut.instPartialOrder M = { le := fun (U U' : M.ModularCut) => ↑U ⊆ ↑U', le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

theorem Matroid.ModularCut.le_iff_subset {α : Type u_1} {M : Matroid α} {U U' : M.ModularCut} : U ≤ U' ↔ ↑U ⊆ ↑U'

@[instance_reducible]

instance Matroid.ModularCut.instBoundedOrder {α : Type u_1} (M : Matroid α) : BoundedOrder M.ModularCut

Equations

• Matroid.ModularCut.instBoundedOrder M = { top := Matroid.ModularCut.principal M ∅, le_top := ⋯, bot := Matroid.ModularCut.empty M, bot_le := ⋯ }

@[simp]

theorem Matroid.ModularCut.notMem_bot {α : Type u_1} {M : Matroid α} (X : Set α) : X ∉ ⊥

@[simp]

theorem Matroid.ModularCut.coe_bot {α : Type u_1} (M : Matroid α) : ↑⊥ = ∅

theorem Matroid.ModularCut.eq_bot_or_ground_mem {α : Type u_1} {M : Matroid α} (U : M.ModularCut) : U = ⊥ ∨ M.E ∈ U

theorem Matroid.ModularCut.eq_bot_iff {α : Type u_1} {M : Matroid α} (U : M.ModularCut) : U = ⊥ ↔ M.E ∉ U

theorem Matroid.ModularCut.ne_bot_iff {α : Type u_1} {M : Matroid α} (U : M.ModularCut) : U ≠ ⊥ ↔ M.E ∈ U

@[simp]

theorem Matroid.ModularCut.principal_ne_bot {α : Type u_1} (M : Matroid α) (X : Set α) : principal M X ≠ ⊥

theorem Matroid.ModularCut.mem_top_of_isFlat {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) : F ∈ ⊤

@[simp]

theorem Matroid.ModularCut.mem_top_iff {α : Type u_1} {M : Matroid α} {F : Set α} : F ∈ ⊤ ↔ M.IsFlat F

theorem Matroid.ModularCut.eq_top_iff {α : Type u_1} {M : Matroid α} {U : M.ModularCut} : U = ⊤ ↔ M.loops ∈ U

theorem Matroid.ModularCut.top_ne_bot {α : Type u_1} (M : Matroid α) : ⊤ ≠ ⊥

@[simp]

theorem Matroid.ModularCut.map_top {α : Type u_1} {M : Matroid α} {β : Type u_2} {f : α → β} (hf : Set.InjOn f M.E) : ⊤.map f hf = ⊤

@[simp]

theorem Matroid.ModularCut.map_eq_top {α : Type u_1} {M : Matroid α} {β : Type u_2} {f : α → β} (hf : Set.InjOn f M.E) {U : M.ModularCut} : U.map f hf = ⊤ ↔ U = ⊤

@[simp]

theorem Matroid.ModularCut.map_bot {α : Type u_1} {M : Matroid α} {β : Type u_2} {f : α → β} (hf : Set.InjOn f M.E) : ⊥.map f hf = ⊥

@[simp]

theorem Matroid.ModularCut.map_eq_bot {α : Type u_1} {M : Matroid α} {β : Type u_2} {f : α → β} {U : M.ModularCut} (hf : Set.InjOn f M.E) : U.map f hf = ⊥ ↔ U = ⊥

theorem Matroid.ModularCut.principal_eq_top_iff' {α : Type u_1} {M : Matroid α} {F : Set α} : principal M F = ⊤ ↔ F ∩ M.E ⊆ M.loops

theorem Matroid.ModularCut.principal_eq_top_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hXE : X ⊆ M.E := by aesop_mat) : principal M X = ⊤ ↔ X ⊆ M.loops

theorem Matroid.ModularCut.principal_ground_ne_top {α : Type u_1} (M : Matroid α) [M.RankPos] : principal M M.E ≠ ⊤

theorem Matroid.ModularCut.mem_of_ssubset_indep_of_forall_diff {α : Type u_1} {M : Matroid α} {I J : Set α} (U : M.ModularCut) (hI : M.Indep I) (hJI : J ⊂ I) (h : ∀ e ∈ I \ J, M.closure (I \ {e}) ∈ U) : M.closure J ∈ U

theorem Matroid.ModularCut.covBy_of_maximal_closure {α : Type u_1} {M : Matroid α} (U : M.ModularCut) {X Y : Set α} (hXY : M.closure X ⊆ M.closure Y) (hYU : M.closure Y ∈ U) (hXU : M.closure X ∉ U) (hmax : ∀ x ∈ Y \ M.closure X, M.closure (insert x X) ∈ U) : M.closure X ⋖[M] M.closure Y

If X spans a flat outside U, but X ∪ {y} spans a flat in U for all y ∈ Y \ M.closure X, then M.closure X is covered by M.closure Y.

def Matroid.ModularCut.restrict {α : Type u_1} {M : Matroid α} (U : M.ModularCut) (R : Set α) : (M.restrict R).ModularCut

A ModularCut in M gives a ModularCut in M ↾ R for any R ⊆ M.E.

Equations

• U.restrict R = { carrier := {F : Set α | (M.restrict R).IsFlat F ∧ M.closure F ∈ U}, forall_isFlat := ⋯, forall_superset := ⋯, forall_inter := ⋯ }

@[simp]

theorem Matroid.ModularCut.mem_restrict_iff {α : Type u_1} {M : Matroid α} {F : Set α} (U : M.ModularCut) {R : Set α} : F ∈ U.restrict R ↔ (M.restrict R).IsFlat F ∧ M.closure F ∈ U

theorem Matroid.ModularCut.inter_mem_restrict_iff {α : Type u_1} {M : Matroid α} {F : Set α} (U : M.ModularCut) {R : Set α} (hF : M.IsFlat F) (hR : R ⊆ M.E) : F ∩ R ∈ U.restrict R ↔ M.closure (F ∩ R) ∈ U

@[simp]

theorem Matroid.ModularCut.restrict_copy {α : Type u_1} {M N : Matroid α} (U : M.ModularCut) (R : Set α) (hMN : M = N) : (U.restrict R).copy ⋯ = (U.copy hMN).restrict R

@[simp]

theorem Matroid.ModularCut.restrict_eq_top_iff {α : Type u_1} {M : Matroid α} {U : M.ModularCut} {R : Set α} : U.restrict R = ⊤ ↔ U = ⊤

@[simp]

theorem Matroid.ModularCut.restrict_eq_bot_iff {α : Type u_1} {M : Matroid α} {U : M.ModularCut} {R : Set α} : U.restrict R = ⊥ ↔ M.closure R ∉ U

def Matroid.ModularCut.delete {α : Type u_1} {M : Matroid α} (U : M.ModularCut) (D : Set α) : (M.delete D).ModularCut

a ModularCut in M gives a ModularCut in M ＼ D for any D.

Equations

• U.delete D = U.restrict (M.E \ D)

@[simp]

theorem Matroid.ModularCut.mem_delete_iff {α : Type u_1} {M : Matroid α} {F : Set α} (U : M.ModularCut) {D : Set α} : F ∈ U.delete D ↔ (M.delete D).IsFlat F ∧ M.closure F ∈ U

theorem Matroid.ModularCut.mem_delete_elem_iff {α : Type u_1} {M : Matroid α} {F : Set α} {e : α} {U : M.ModularCut} : F ∈ U.delete {e} ↔ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.closure F)

theorem Matroid.ModularCut.principal_restrict_eq_bot_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : X ⊆ M.E := by aesop_mat) : (principal M X).restrict Y = ⊥ ↔ ¬X ⊆ M.closure Y

theorem Matroid.ModularCut.principal_delete_eq_bot_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : X ⊆ M.E := by aesop_mat) : (principal M X).delete Y = ⊥ ↔ ¬X ⊆ M.closure (M.E \ Y)

theorem Matroid.ModularCut.principal_delete_self_eq_bot_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) : (principal M X).delete X = ⊥ ↔ M.Codep X

theorem Matroid.ModularCut.principal_restrict_eq_top_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : X ⊆ M.E := by aesop_mat) : (principal M X).restrict Y = ⊤ ↔ X ⊆ M.loops

def Matroid.ModularCut.comapOfSubsetRange {α : Type u_1} {β : Type u_2} {M : Matroid β} (U : M.ModularCut) (f : α → β) (hf : M.E ⊆ Set.range f) : (M.comap f).ModularCut

Equations

• U.comapOfSubsetRange f hf = { carrier := Set.preimage f '' ↑U, forall_isFlat := ⋯, forall_superset := ⋯, forall_inter := ⋯ }

@[simp]

theorem Matroid.ModularCut.mem_comapOfSubsetRange_iff {α : Type u_1} {F : Set α} {β : Type u_2} {M : Matroid β} (U : M.ModularCut) {f : α → β} {hf : M.E ⊆ Set.range f} : F ∈ U.comapOfSubsetRange f hf ↔ ∃ F₀ ∈ U, f ⁻¹' F₀ = F

def Matroid.ModularCut.comap {α : Type u_1} {β : Type u_2} {M : Matroid β} (U : M.ModularCut) (f : α → β) : (M.comap f).ModularCut

Equations

• U.comap f = ((U.restrict (Set.range f ∩ M.E)).comapOfSubsetRange f ⋯).copy ⋯

@[simp]

theorem Matroid.ModularCut.mem_comap_iff {α : Type u_1} {F : Set α} {β : Type u_2} {M : Matroid β} (U : M.ModularCut) (f : α → β) : F ∈ U.comap f ↔ M.closure (f '' F) ∈ U ∧ F = f ⁻¹' M.closure (f '' F)

def Matroid.ModularCut.ofDeleteElem {α : Type u_1} (M : Matroid α) (e : α) : (M.delete {e}).ModularCut

Given an element e of a matroid M, the modular cut of M ＼ e corresponding to the extension M of M ＼ e. Intended to apply when e ∈ M.E.

Equations

• Matroid.ModularCut.ofDeleteElem M e = { carrier := {F : Set α | (M.delete {e}).IsFlat F ∧ e ∈ M.closure F}, forall_isFlat := ⋯, forall_superset := ⋯, forall_inter := ⋯ }

theorem Matroid.ModularCut.mem_ofDeleteElem_iff {α : Type u_1} {M : Matroid α} {F : Set α} {e : α} : F ∈ ofDeleteElem M e ↔ e ∉ F ∧ M.closure F = insert e F

@[simp]

theorem Matroid.ModularCut.mem_ofDeleteElem_iff' {α : Type u_1} {M : Matroid α} {F : Set α} {e : α} : F ∈ ofDeleteElem M e ↔ e ∈ M.closure F \ F ∧ M.IsFlat (insert e F)

@[simp]

theorem Matroid.ModularCut.ofDeleteElem_eq_top_iff {α : Type u_1} {M : Matroid α} {e : α} : ofDeleteElem M e = ⊤ ↔ M.IsLoop e

theorem Matroid.ModularCut.ofDeleteElem_eq_bot_of_notMem {α : Type u_1} {M : Matroid α} {e : α} (he : e ∉ M.E) : ofDeleteElem M e = ⊥

def Matroid.ModularCut.ofForallIsModularPairChainInter {α : Type u_1} (M : Matroid α) (U : Set (Set α)) (h_isFlat : ∀ F ∈ U, M.IsFlat F) (h_superset : ∀ ⦃F F' : Set α⦄, F ∈ U → M.IsFlat F' → F ⊆ F' → F' ∈ U) (h_pair : ∀ ⦃F F' : Set α⦄, F ∈ U → F' ∈ U → M.IsModularPair F F' → F ∩ F' ∈ U) (h_chain : ∀ Cs ⊆ U, Cs.Infinite → (M.IsModularFamily fun (x : ↑Cs) => ↑x) → IsChain (fun (x1 x2 : Set α) => x1 ⊆ x2) Cs → ⋂₀ Cs ∈ U) : M.ModularCut

The modular family condition can be replaced by a condition about modular pairs and infinite chains.

Equations

• Matroid.ModularCut.ofForallIsModularPairChainInter M U h_isFlat h_superset h_pair h_chain = { carrier := U, forall_isFlat := h_isFlat, forall_superset := h_superset, forall_inter := ⋯ }

@[simp]

theorem Matroid.ModularCut.mem_ofForallIsModularPairChainInter_iff {α : Type u_1} (M : Matroid α) (U : Set (Set α)) (h_isFlat : ∀ F ∈ U, M.IsFlat F) (h_superset : ∀ ⦃F F' : Set α⦄, F ∈ U → M.IsFlat F' → F ⊆ F' → F' ∈ U) (h_pair : ∀ ⦃F F' : Set α⦄, F ∈ U → F' ∈ U → M.IsModularPair F F' → F ∩ F' ∈ U) (h_chain : ∀ Cs ⊆ U, Cs.Infinite → (M.IsModularFamily fun (x : ↑Cs) => ↑x) → IsChain (fun (x1 x2 : Set α) => x1 ⊆ x2) Cs → ⋂₀ Cs ∈ U) {F : Set α} : F ∈ ofForallIsModularPairChainInter M U h_isFlat h_superset h_pair h_chain ↔ F ∈ U

def Matroid.ModularCut.ofForallIsModularPairInter {α : Type u_1} (M : Matroid α) [M.RankFinite] (U : Set (Set α)) (h_isFlat : ∀ F ∈ U, M.IsFlat F) (h_superset : ∀ ⦃F F' : Set α⦄, F ∈ U → M.IsFlat F' → F ⊆ F' → F' ∈ U) (h_pair : ∀ ⦃F F' : Set α⦄, F ∈ U → F' ∈ U → M.IsModularPair F F' → F ∩ F' ∈ U) : M.ModularCut

For a finite-rank matroid, the intersection condition can be replaced with a condition about modular pairs rather than families.

Equations

• Matroid.ModularCut.ofForallIsModularPairInter M U h_isFlat h_superset h_pair = Matroid.ModularCut.ofForallIsModularPairChainInter M U h_isFlat h_superset h_pair ⋯

@[simp]

theorem Matroid.ModularCut.ofForallIsModularPairInter_carrier {α : Type u_1} (M : Matroid α) [M.RankFinite] (U : Set (Set α)) (h_isFlat : ∀ F ∈ U, M.IsFlat F) (h_superset : ∀ ⦃F F' : Set α⦄, F ∈ U → M.IsFlat F' → F ⊆ F' → F' ∈ U) (h_pair : ∀ ⦃F F' : Set α⦄, F ∈ U → F' ∈ U → M.IsModularPair F F' → F ∩ F' ∈ U) : ↑(ofForallIsModularPairInter M U h_isFlat h_superset h_pair) = U

@[simp]

theorem Matroid.ModularCut.mem_ofForallIsModularPairInter_iff {α : Type u_1} (M : Matroid α) [M.RankFinite] (U : Set (Set α)) (h_isFlat : ∀ F ∈ U, M.IsFlat F) (h_superset : ∀ ⦃F F' : Set α⦄, F ∈ U → M.IsFlat F' → F ⊆ F' → F' ∈ U) (h_pair : ∀ ⦃F F' : Set α⦄, F ∈ U → F' ∈ U → M.IsModularPair F F' → F ∩ F' ∈ U) {F : Set α} : F ∈ ofForallIsModularPairInter M U h_isFlat h_superset h_pair ↔ F ∈ U