Matroid.Representation.Basic

source

structure Matroid.Rep {α : Type u_1} (M : Matroid α) (𝔽 : Type u_7) (W : Type u_8) [Semiring 𝔽] [AddCommMonoid W] [Module 𝔽 W] :

Type (max u_1 u_8)

M.Rep 𝔽 W is a function from α to a module W that represents M.

to_fun : α → W
indep_iff' (I : Set α) : M.Indep I ↔ LinearIndepOn 𝔽 self.to_fun I

Instances For

source

theorem Matroid.Rep.ext {α : Type u_1} {M : Matroid α} {𝔽 : Type u_7} {W : Type u_8} {inst✝ : Semiring 𝔽} {inst✝¹ : AddCommMonoid W} {inst✝² : Module 𝔽 W} {x y : M.Rep 𝔽 W} (to_fun : x.to_fun = y.to_fun) :

x = y

source

theorem Matroid.Rep.ext_iff {α : Type u_1} {M : Matroid α} {𝔽 : Type u_7} {W : Type u_8} {inst✝ : Semiring 𝔽} {inst✝¹ : AddCommMonoid W} {inst✝² : Module 𝔽 W} {x y : M.Rep 𝔽 W} :

x = y ↔ x.to_fun = y.to_fun

source

@[instance_reducible]

instance Matroid.instFunLikeRep {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] :

FunLike (M.Rep 𝔽 W) α W

Equations

Matroid.instFunLikeRep = { coe := fun (v : M.Rep 𝔽 W) => v.to_fun, coe_injective := ⋯ }

source

@[simp]

theorem Matroid.Rep.to_fun_eq_coe {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) :

v.to_fun = ⇑v

source

theorem Matroid.Rep.indep_iff {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {I : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) :

M.Indep I ↔ LinearIndepOn 𝔽 (⇑v) I

source

theorem Matroid.Rep.onIndep {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {I : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (hI : M.Indep I) :

LinearIndepOn 𝔽 (⇑v) I

source

theorem Matroid.Rep.injOn_of_indep {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {I : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (hI : M.Indep I) :

Set.InjOn (⇑v) I

source

theorem Matroid.Rep.isBasis'_iff {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {I X : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) :

M.IsBasis' I X ↔ I ⊆ X ∧ LinearIndepOn 𝔽 (⇑v) I ∧ ⇑v '' X ⊆ ↑(Submodule.span 𝔽 (⇑v '' I))

source

theorem Matroid.Rep.mem_closure_iff {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {e : α} {X : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (heE : e ∈ M.E := by aesop_mat) :

e ∈ M.closure X ↔ v e ∈ Submodule.span 𝔽 (⇑v '' X)

source

theorem Matroid.Rep.closure_eq {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (X : Set α) :

M.closure X = ⇑v ⁻¹' ↑(Submodule.span 𝔽 (⇑v '' X)) ∩ M.E

source

theorem Matroid.Rep.mem_closure_iff' {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {e : α} {X : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) :

e ∈ M.closure X ↔ v e ∈ Submodule.span 𝔽 (⇑v '' X) ∧ e ∈ M.E

source

theorem Matroid.Rep.eq_zero_iff_not_indep {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {e : α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] {v : M.Rep 𝔽 W} :

v e = 0 ↔ ¬M.Indep {e}

source

theorem Matroid.Rep.eq_zero_iff {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] (v : M.Rep 𝔽 W) (e : α) (he : e ∈ M.E := by aesop_mat) :

v e = 0 ↔ M.IsLoop e

source

theorem Matroid.Rep.eq_zero_of_notMem_ground {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {e : α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] (v : M.Rep 𝔽 W) (he : e ∉ M.E) :

v e = 0

source

theorem Matroid.Rep.eq_zero_of_isLoop {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {e : α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] (v : M.Rep 𝔽 W) (h : M.IsLoop e) :

v e = 0

source

theorem Matroid.Rep.ne_zero_of_isNonloop {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {e : α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] (v : M.Rep 𝔽 W) (h : M.IsNonloop e) :

v e ≠ 0

source

theorem Matroid.Rep.ne_zero_iff_isNonloop {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] (v : M.Rep 𝔽 W) (e : α) :

v e ≠ 0 ↔ M.IsNonloop e

source

theorem Matroid.Rep.support_subset_ground {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] (v : M.Rep 𝔽 W) :

Function.support ⇑v ⊆ M.E

source

theorem Matroid.Rep.mem_ground_of_apply_ne_zero {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {e : α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] {v : M.Rep 𝔽 W} (hv : v e ≠ 0) :

e ∈ M.E

source

theorem Matroid.Indep.rep_apply_ne_zero_of_mem {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {e : α} {I : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] {v : M.Rep 𝔽 W} (hI : M.Indep I) (heI : e ∈ I) :

v e ≠ 0

source

theorem Matroid.Rep.span_le_of_closure_subset {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {X Y : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] (v : M.Rep 𝔽 W) (hXY : M.closure X ⊆ M.closure Y) :

Submodule.span 𝔽 (⇑v '' X) ≤ Submodule.span 𝔽 (⇑v '' Y)

source

theorem Matroid.Rep.closure_subset_iff_span_le {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {X Y : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] (v : M.Rep 𝔽 W) :

M.closure X ⊆ M.closure Y ↔ Submodule.span 𝔽 (⇑v '' X) ≤ Submodule.span 𝔽 (⇑v '' Y)

source

theorem Matroid.Rep.span_closure_congr {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {X Y : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] (v : M.Rep 𝔽 W) (hXY : M.closure X = M.closure Y) :

Submodule.span 𝔽 (⇑v '' X) = Submodule.span 𝔽 (⇑v '' Y)

source

theorem Matroid.Rep.span_closure_congr_iff {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {X Y : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] (v : M.Rep 𝔽 W) :

M.closure X = M.closure Y ↔ Submodule.span 𝔽 (⇑v '' X) = Submodule.span 𝔽 (⇑v '' Y)

source

@[simp]

theorem Matroid.Rep.span_image_loops {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] (v : M.Rep 𝔽 W) :

Submodule.span 𝔽 (⇑v '' M.loops) = ⊥

source

theorem Matroid.Rep.skew_iff_span_disjoint {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {X Y : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] (v : M.Rep 𝔽 W) (hXE : X ⊆ M.E) (hYE : Y ⊆ M.E) :

M.Skew X Y ↔ Disjoint (Submodule.span 𝔽 (⇑v '' X)) (Submodule.span 𝔽 (⇑v '' Y))

Constructors #

source

def Matroid.Rep.ofGround {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : α → W) (h_support : Function.support v ⊆ M.E) (h_indep : ∀ I ⊆ M.E, M.Indep I ↔ LinearIndepOn 𝔽 v I) :

M.Rep 𝔽 W

A function with support contained in M.E that gives the correct independent sets within the ground set gives a representation

Equations

Matroid.Rep.ofGround v h_support h_indep = { to_fun := v, indep_iff' := ⋯ }

Instances For

source

@[simp]

theorem Matroid.Rep.ofGround_to_fun {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : α → W) (h_support : Function.support v ⊆ M.E) (h_indep : ∀ I ⊆ M.E, M.Indep I ↔ LinearIndepOn 𝔽 v I) (a✝ : α) :

(ofGround v h_support h_indep).to_fun a✝ = v a✝

source

@[simp]

theorem Matroid.Rep.ofGround_apply {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (f : α → W) (hs : Function.support f ⊆ M.E) (hf : ∀ I ⊆ M.E, M.Indep I ↔ LinearIndependent (ι := ↑I) 𝔽 (I.domRestrict f)) (a : α) :

(ofGround f hs hf) a = f a

source

noncomputable def Matroid.Rep.ofSubtypeFun {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (f : ↑M.E → W) [DecidablePred fun (x : α) => x ∈ M.E] (hf : ∀ (I : Set ↑M.E), M.Indep (Subtype.val '' I) ↔ LinearIndepOn 𝔽 f I) :

M.Rep 𝔽 W

A function from M.E to a module determines a representation

Equations

Matroid.Rep.ofSubtypeFun f hf = Matroid.Rep.ofGround (fun (a : α) => if ha : a ∈ M.E then f ⟨a, ha⟩ else 0) ⋯ ⋯

Instances For

source

@[simp]

theorem Matroid.Rep.ofSubtypeFun_to_fun {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (f : ↑M.E → W) [DecidablePred fun (x : α) => x ∈ M.E] (hf : ∀ (I : Set ↑M.E), M.Indep (Subtype.val '' I) ↔ LinearIndepOn 𝔽 f I) (a : α) :

(ofSubtypeFun f hf).to_fun a = if ha : a ∈ M.E then f ⟨a, ha⟩ else 0

source

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

(M.restrict X).Rep 𝔽 W

A representation gives a representation of any restriction

Equations

v.restrict X = Matroid.Rep.ofGround (X.indicator ⇑v) ⋯ ⋯

Instances For

source

@[simp]

theorem Matroid.Rep.restrict_apply {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (X : Set α) :

⇑(v.restrict X) = X.indicator ⇑v

source

@[simp]

theorem Matroid.Rep.ne_zero {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] [M.Loopless] [M.OnUniv] (v : M.Rep 𝔽 W) (e : α) :

v e ≠ 0

source

theorem Matroid.Rep.loopless_iff {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] (v : M.Rep 𝔽 W) :

M.Loopless ↔ ∀ e ∈ M.E, v e ≠ 0

source

theorem Matroid.Rep.parallel_iff {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {e f : α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] (v : M.Rep 𝔽 W) (he : M.IsNonloop e) :

M.Parallel e f ↔ ∃ (c : 𝔽), c ≠ 0 ∧ c • v f = v e

source

theorem Matroid.Rep.parallel_iff' {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {e f : α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] (v : M.Rep 𝔽 W) (he : M.IsNonloop e) :

M.Parallel e f ↔ ∃ (c : 𝔽ˣ), c • v f = v e

source

theorem Matroid.Rep.simple_iff {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] [M.RankPos] (v : M.Rep 𝔽 W) :

M.Simple ↔ ∀ {e f : α}, e ∈ M.E → f ∈ M.E → ∀ (c : 𝔽), c • v f = v e → e = f

source

theorem Matroid.Rep.injOn_of_simple {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module.IsTorsionFree 𝔽 W] (v : M.Rep 𝔽 W) [h : M.Simple] :

Set.InjOn (⇑v) M.E