def Matroid.Rep.contract {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (C : Set α) : (M.contract C).Rep 𝔽 (W ⧸ Submodule.span 𝔽 (⇑v '' C))

Contracting a set preserves representability.

Equations

• v.contract C = { to_fun := ⇑(Submodule.span 𝔽 (⇑v '' C)).mkQ ∘ ⇑v, indep_iff' := ⋯ }

@[simp]

theorem Matroid.Rep.contract_to_fun {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (C : Set α) (a✝ : α) : (v.contract C).to_fun a✝ = Submodule.Quotient.mk (v a✝)

noncomputable def Matroid.Rep.delete {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (D : Set α) : (M.delete D).Rep 𝔽 W

Equations

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

@[simp]

theorem Matroid.Rep.delete_to_fun {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (D : Set α) (x : α) : (v.delete D).to_fun x = (M.E \ D).indicator (⇑v) x

theorem Matroid.Representable.contract {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] (hM : M.Representable 𝔽) {C : Set α} : (M.contract C).Representable 𝔽

theorem Matroid.Representable.delete {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] (hM : M.Representable 𝔽) {D : Set α} : (M.delete D).Representable 𝔽

theorem Matroid.Representable.restrict {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] (hM : M.Representable 𝔽) {R : Set α} : (M.restrict R).Representable 𝔽

theorem Matroid.Representable.of_isMinor {α : Type u_1} {𝔽 : Type u_5} [DivisionRing 𝔽] {M N : Matroid α} (hM : M.Representable 𝔽) (hNM : N ≤m M) : N.Representable 𝔽

theorem Matroid.Representable.isoMinor {α : Type u_1} {β : Type u_2} {𝔽 : Type u_5} [DivisionRing 𝔽] {M : Matroid α} {N : Matroid β} (hM : M.Representable 𝔽) (hNM : IsoMinor N M) : N.Representable 𝔽