theorem Matroid.ModularCut.projectBy_aux {α : Type u_1} {M : Matroid α} {I : Set α} (U : M.ModularCut) : ((((M.map some ⋯).extendBy none (U.map some ⋯)).contract {none}).comap some).Indep I ↔ M.Indep I ∧ (U ≠ ⊤ → M.closure I ∉ U)

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

Extend M using the modular cut U, and contract the new element. Defining this in terms of extendBy would be difficult if M.E = univ, so we define it directly instead.

Equations

• M.projectBy U = Matroid.ofExistsMatroid M.E (fun (I : Set α) => M.Indep I ∧ (U ≠ ⊤ → M.closure I ∉ U)) ⋯

theorem Matroid.ModularCut.projectBy_eq_map_comap {α : Type u_1} {M : Matroid α} (U : M.ModularCut) : M.projectBy U = (((M.map some ⋯).extendBy none (U.map some ⋯)).contract {none}).comap some

The messier expression for projectBy; projectBy is obtained from M by mapping it into Option α, extending by the new element none and contracting it, then comapping back to α.

@[simp]

theorem Matroid.ModularCut.projectBy_ground {α : Type u_1} {M : Matroid α} (U : M.ModularCut) : (M.projectBy U).E = M.E

@[simp]

theorem Matroid.ModularCut.projectBy_indep_iff {α : Type u_1} {M : Matroid α} {I : Set α} (U : M.ModularCut) : (M.projectBy U).Indep I ↔ M.Indep I ∧ (U ≠ ⊤ → M.closure I ∉ U)

theorem Matroid.ModularCut.projectBy_indep_iff_of_ne_top {α : Type u_1} {M : Matroid α} {U : M.ModularCut} {I : Set α} (hU : U ≠ ⊤) : (M.projectBy U).Indep I ↔ M.Indep I ∧ M.closure I ∉ U

@[simp]

theorem Matroid.ModularCut.projectBy_top {α : Type u_1} {M : Matroid α} : M.projectBy ⊤ = M

@[simp]

theorem Matroid.ModularCut.projectBy_bot {α : Type u_1} {M : Matroid α} : M.projectBy ⊥ = M

@[simp]

theorem Matroid.ModularCut.projectBy_copy {α : Type u_1} {M N : Matroid α} (U : N.ModularCut) (h : N = M) : M.projectBy (U.copy h) = N.projectBy U

@[simp]

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

theorem Matroid.ModularCut.projectBy_eq_self_iff {α : Type u_1} {M : Matroid α} (U : M.ModularCut) : M.projectBy U = M ↔ U = ⊥ ∨ U = ⊤

@[simp]

theorem Matroid.ModularCut.extendBy_contractElem {α : Type u_1} {M : Matroid α} {e : α} (U : M.ModularCut) (he : e ∉ M.E) : (M.extendBy e U).contract {e} = M.projectBy U

theorem Matroid.ModularCut.closure_subset_closure_projectBy {α : Type u_1} {M : Matroid α} (U : M.ModularCut) (X : Set α) : M.closure X ⊆ (M.projectBy U).closure X

theorem Matroid.ModularCut.projectBy_quotient {α : Type u_1} {M : Matroid α} (U : M.ModularCut) : M.projectBy U ≤q M

theorem Matroid.ModularCut.mem_closure_projectBy_iff {α : Type u_1} {M : Matroid α} {X : Set α} {f : α} (U : M.ModularCut) : f ∈ (M.projectBy U).closure X ↔ f ∈ M.closure X ∨ M.closure (insert f X) ∈ U ∧ M.closure X ∉ U

theorem Matroid.ModularCut.projectBy_spanning_iff {α : Type u_1} {M : Matroid α} {X : Set α} {U : M.ModularCut} (hU : U ≠ ⊥) (hX : X ⊆ M.E := by aesop_mat) : (M.projectBy U).Spanning X ↔ M.Spanning X ∨ M.eRelRk X M.E = 1 ∧ M.closure X ∉ U

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

theorem Matroid.ModularCut.projectBy_project_eq_project_of_mem {α : Type u_1} {M : Matroid α} {F : Set α} (U : M.ModularCut) (hF : F ∈ U) : (M.projectBy U).project F = M.project F

Projecting out by a flat in a modular cut cancels the projection by the modular cut.

theorem Matroid.ModularCut.projectBy_project_eq_project_of_closure_mem {α : Type u_1} {M : Matroid α} {X : Set α} (U : M.ModularCut) (hX : M.closure X ∈ U) : (M.projectBy U).project X = M.project X

theorem Matroid.ModularCut.projectBy_contract_eq_contract_of_closure_mem {α : Type u_1} {M : Matroid α} {X : Set α} (U : M.ModularCut) (hX : M.closure X ∈ U) : (M.projectBy U).contract X = M.contract X

theorem Matroid.ModularCut.projectBy_base_diff_singleton_iff {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} {U : M.ModularCut} (hU : U ≠ ⊥) (hB : M.IsBase B) (he : e ∈ B) : (M.projectBy U).IsBase (B \ {e}) ↔ M.closure (B \ {e}) ∉ U

theorem Matroid.ModularCut.exists_diff_singleton_isBase_projectBy {α : Type u_1} {M : Matroid α} {B : Set α} {U : M.ModularCut} (hU_top : U ≠ ⊤) (hU_bot : U ≠ ⊥) (hB : M.IsBase B) : ∃ e ∈ B, (M.projectBy U).IsBase (B \ {e})

theorem Matroid.ModularCut.projectBy_eRank_add_one_eq {α : Type u_1} {M : Matroid α} (U : M.ModularCut) (hU_top : U ≠ ⊤) (hU_bot : U ≠ ⊥) : (M.projectBy U).eRank + 1 = M.eRank

theorem Matroid.ModularCut.projectBy_restrict {α : Type u_1} {M : Matroid α} (U : M.ModularCut) (R : Set α) : (M.restrict R).projectBy (U.restrict R) = (M.projectBy U).restrict R

@[simp]

theorem Matroid.ModularCut.projectBy_delete {α : Type u_1} {M : Matroid α} (U : M.ModularCut) (D : Set α) : (M.delete D).projectBy (U.delete D) = (M.projectBy U).delete D

@[simp]

theorem Matroid.ModularCut.projectBy_ofDeleteElem {α : Type u_1} (M : Matroid α) (e : α) : (M.delete {e}).projectBy (ofDeleteElem M e) = M.contract {e}

@[simp]

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

def Matroid.liftBy {α : Type u_1} (M : Matroid α) (U : M✶.ModularCut) : Matroid α

Lift a matroid using a modular cut of the dual.

Equations

• M.liftBy U = (M✶.projectBy U)✶

@[simp]

theorem Matroid.ModularCut.liftBy_ground {α : Type u_1} (M : Matroid α) (U : M✶.ModularCut) : (M.liftBy U).E = M.E

@[simp]

theorem Matroid.ModularCut.liftBy_dual {α : Type u_1} (M : Matroid α) (U : M✶.ModularCut) : (M.liftBy U)✶ = M✶.projectBy U

@[simp]

theorem Matroid.ModularCut.projectBy_dual {α : Type u_1} (M : Matroid α) (U : M✶.ModularCut) : (M✶.projectBy U)✶ = M.liftBy U

theorem Matroid.ModularCut.liftBy_contract {α : Type u_1} {M : Matroid α} (U : M✶.ModularCut) (C : Set α) : (M.contract C).liftBy ((U.delete C).copy ⋯) = (M.liftBy U).contract C

theorem Matroid.ModularCut.liftBy_delete_eq_delete_of_dual_closure_mem {α : Type u_1} {M : Matroid α} {X : Set α} (U : M✶.ModularCut) (hX : M✶.closure X ∈ U) : (M.liftBy U).delete X = M.delete X

theorem Matroid.ModularCut.liftBy_quotient {α : Type u_1} {M : Matroid α} (U : M✶.ModularCut) : M ≤q M.liftBy U