Matroid.Representation.Map

source

def Matroid.Rep.comp {α : Type u_1} {W : Type u_3} {W' : Type u_4} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [AddCommGroup W'] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (ψ : W →ₗ[𝔽] W') (h_inj : Disjoint (Submodule.span 𝔽 (Set.range ⇑v)) ψ.ker) :

M.Rep 𝔽 W'

Compose a representation v with a linear map that is injective on the range of v

Equations

v.comp ψ h_inj = { to_fun := ⇑ψ ∘ ⇑v, indep_iff' := ⋯ }

Instances For

Maps between representations #

source

def Matroid.Rep.comp' {α : Type u_1} {W : Type u_3} {W' : Type u_4} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [AddCommGroup W'] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (ψ : W →ₗ[𝔽] W') (hψ : ψ.ker = ⊥) :

M.Rep 𝔽 W'

Compose a representation with a linear injection.

Equations

v.comp' ψ hψ = v.comp ψ ⋯

Instances For

source

def Matroid.Rep.compEquiv {α : Type u_1} {W : Type u_3} {W' : Type u_4} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [AddCommGroup W'] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (ψ : W ≃ₗ[𝔽] W') :

M.Rep 𝔽 W'

Compose a representation with a linear equivalence.

Equations

v.compEquiv ψ = v.comp' ↑ψ ⋯

Instances For

source

@[simp]

theorem Matroid.Rep.comp_apply {α : Type u_1} {W : Type u_3} {W' : Type u_4} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [AddCommGroup W'] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (ψ : W →ₗ[𝔽] W') (h_inj : Disjoint (Submodule.span 𝔽 (Set.range ⇑v)) ψ.ker) (e : α) :

(v.comp ψ h_inj) e = ψ (v e)

source

@[simp]

theorem Matroid.Rep.comp_coeFun {α : Type u_1} {W : Type u_3} {W' : Type u_4} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [AddCommGroup W'] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (ψ : W →ₗ[𝔽] W') (h_inj : Disjoint (Submodule.span 𝔽 (Set.range ⇑v)) ψ.ker) :

⇑(v.comp ψ h_inj) = ⇑ψ ∘ ⇑v

source

@[simp]

theorem Matroid.Rep.comp'_apply {α : Type u_1} {W : Type u_3} {W' : Type u_4} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [AddCommGroup W'] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (ψ : W →ₗ[𝔽] W') (hψ : ψ.ker = ⊥) (e : α) :

(v.comp' ψ hψ) e = ψ (v e)

source

@[simp]

theorem Matroid.Rep.comp'_coeFun {α : Type u_1} {W : Type u_3} {W' : Type u_4} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [AddCommGroup W'] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (ψ : W →ₗ[𝔽] W') (h_inj : ψ.ker = ⊥) :

⇑(v.comp' ψ h_inj) = ⇑ψ ∘ ⇑v

source

@[simp]

theorem Matroid.Rep.compEquiv_apply {α : Type u_1} {W : Type u_3} {W' : Type u_4} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [AddCommGroup W'] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (ψ : W ≃ₗ[𝔽] W') (e : α) :

(v.compEquiv ψ) e = ψ (v e)

source

@[simp]

theorem Matroid.Rep.compEquiv_coeFun {α : Type u_1} {W : Type u_3} {W' : Type u_4} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [AddCommGroup W'] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (ψ : W ≃ₗ[𝔽] W') :

⇑(v.compEquiv ψ) = ⇑ψ ∘ ⇑v

source

@[simp]

theorem Matroid.Rep.compEquiv_compEquiv_symm {α : Type u_1} {W : Type u_3} {W' : Type u_4} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [AddCommGroup W'] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (ψ : W ≃ₗ[𝔽] W') :

(v.compEquiv ψ).compEquiv ψ.symm = v

source

@[simp]

theorem Matroid.Rep.compEquiv_symm_compEquiv {α : Type u_1} {W : Type u_3} {W' : Type u_4} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [AddCommGroup W'] [Module 𝔽 W'] (v : M.Rep 𝔽 W') (ψ : W ≃ₗ[𝔽] W') :

(v.compEquiv ψ.symm).compEquiv ψ = v

source

def Matroid.Rep.subtype_ofEq {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {W₁ W₂ : Submodule 𝔽 W} (v : M.Rep 𝔽 ↥W₁) (h : W₁ = W₂) :

M.Rep 𝔽 ↥W₂

Compose a representation with a module equality

Equations

v.subtype_ofEq h = v.compEquiv (LinearEquiv.ofEq W₁ W₂ h)

Instances For

source

@[simp]

theorem Matroid.Rep.subtype_ofEq_apply {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {W₁ W₂ : Submodule 𝔽 W} (v : M.Rep 𝔽 ↥W₁) (h : W₁ = W₂) (e : α) :

(v.subtype_ofEq h) e = (LinearEquiv.ofEq W₁ W₂ h) (v e)

source

noncomputable def Matroid.Rep.finsuppToFun {α : Type u_1} {β : Type u_2} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] (v : M.Rep 𝔽 (β →₀ 𝔽)) :

M.Rep 𝔽 (β → 𝔽)

Equations

v.finsuppToFun = v.comp' Finsupp.lcoeFun ⋯

Instances For

source

@[simp]

theorem Matroid.Rep.finsuppToFun_to_fun {α : Type u_1} {β : Type u_2} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] (v : M.Rep 𝔽 (β →₀ 𝔽)) (a✝ : α) (a✝¹ : β) :

v.finsuppToFun.to_fun a✝ a✝¹ = (v a✝) a✝¹

source

def Matroid.Rep.comap {α : Type u_1} {β : Type u_2} {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {M : Matroid β} (v : M.Rep 𝔽 W) (f : α → β) :

(M.comap f).Rep 𝔽 W

A representation gives a representation of a comap

Equations

v.comap f = { to_fun := ⇑v ∘ f, indep_iff' := ⋯ }

Instances For

source

@[simp]

theorem Matroid.Rep.comap_to_fun {α : Type u_1} {β : Type u_2} {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {M : Matroid β} (v : M.Rep 𝔽 W) (f : α → β) (a✝ : α) :

(v.comap f).to_fun a✝ = (⇑v ∘ f) a✝

source

theorem Matroid.Rep.comap_coeFun_eq {α : Type u_1} {β : Type u_2} {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {M : Matroid β} (f : α → β) (v : M.Rep 𝔽 W) :

⇑(v.comap f) = ⇑v ∘ f

source

@[simp]

theorem Matroid.Rep.comap_apply {α : Type u_1} {β : Type u_2} {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {M : Matroid β} (f : α → β) (v : M.Rep 𝔽 W) (a : α) :

(v.comap f) a = v (f a)

source

def Matroid.Rep.ofEq {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {M N : Matroid α} (v : M.Rep 𝔽 W) (h : M = N) :

N.Rep 𝔽 W

Equations

v.ofEq h = { to_fun := ⇑v, indep_iff' := ⋯ }

Instances For

source

@[simp]

theorem Matroid.Rep.ofEq_to_fun {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {M N : Matroid α} (v : M.Rep 𝔽 W) (h : M = N) (a : α) :

(v.ofEq h).to_fun a = v a

source

@[simp]

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

⇑(v.ofEq h) = ⇑v

source

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

(M.restrictSubtype X).Rep 𝔽 W

Equations

v.restrictSubtype X = (v.restrict X).comap Subtype.val

Instances For

source

noncomputable def Matroid.Rep.map {α : Type u_1} {β : Type u_2} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (f : α → β) (hf : Set.InjOn f M.E) [DecidablePred fun (x : β) => ∃ y ∈ M.E, f y = x] :

(M.map f hf).Rep 𝔽 W

Transfer a Rep along a matroid map. The definition involves extending a function with zero, so requires a DecidablePred assumption.

Equations

v.map f hf = Matroid.Rep.ofGround (fun (x : β) => if h : ∃ y ∈ M.E, f y = x then v h.choose else 0) ⋯ ⋯

Instances For

source

theorem Matroid.Rep.matroidMap_apply {α : Type u_1} {β : Type u_2} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) {f : α → β} {hf : Set.InjOn f M.E} [DecidablePred fun (x : β) => ∃ y ∈ M.E, f y = x] {x : α} (hx : x ∈ M.E) :

(v.map f hf) (f x) = v x

source

theorem Matroid.Rep.matroidMap_image {α : Type u_1} {β : Type u_2} {W : Type u_3} {𝔽 : Type u_5} {X : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (f : α → β) (hf : Set.InjOn f M.E) [DecidablePred fun (x : β) => ∃ y ∈ M.E, f y = x] (hX : X ⊆ M.E) :

⇑(v.map f hf) '' f '' X = ⇑v '' X

source

def Matroid.Rep.scale {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (c : α → 𝔽ˣ) :

M.Rep 𝔽 W

Scale a representation by an invertible scalar for each element of α.

Equations

v.scale c = { to_fun := c • ⇑v, indep_iff' := ⋯ }

Instances For

source

@[simp]

theorem Matroid.Rep.scale_to_fun {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (c : α → 𝔽ˣ) (a : α) :

(v.scale c).to_fun a = (c • ⇑v) a

source

def Module.matroid (𝔽 : Type u_7) (W : Type u_8) [AddCommGroup W] [DivisionRing 𝔽] [Module 𝔽 W] :

Matroid W

The 𝔽-representable matroid whose ground set is a vector space W over 𝔽, and independence is linear independence.

Equations

Module.matroid 𝔽 W = (IndepMatroid.ofFinitaryCardAugment Set.univ (fun (I : Set W) => LinearIndepOn 𝔽 id I) ⋯ ⋯ ⋯ ⋯ ⋯).matroid

Instances For

source

def Module.matroidRep (𝔽 : Type u_7) (W : Type u_8) [AddCommGroup W] [DivisionRing 𝔽] [Module 𝔽 W] :

(Module.matroid 𝔽 W).Rep 𝔽 W

Equations

Module.matroidRep 𝔽 W = { to_fun := id, indep_iff' := ⋯ }

Instances For

source

@[simp]

theorem Module.matroidRep_to_fun (𝔽 : Type u_7) (W : Type u_8) [AddCommGroup W] [DivisionRing 𝔽] [Module 𝔽 W] (a : W) :

(Module.matroidRep 𝔽 W).to_fun a = a

source

@[simp]

theorem Module.matroid_subsingleton (𝔽 : Type u_7) (W : Type u_8) [AddCommGroup W] [DivisionRing 𝔽] [Module 𝔽 W] [Subsingleton W] :

Module.matroid 𝔽 W = Matroid.loopyOn {0}

source

instance Module.matroid_finitary {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] :

(Module.matroid 𝔽 W).Finitary

source

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

M = (Module.matroid 𝔽 W).comapOn M.E ⇑v

source

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

M.Finitary

Representations from functions #

source

def Matroid.ofFun {α : Type u_1} {W : Type u_3} [AddCommGroup W] (𝔽 : Type u_7) [DivisionRing 𝔽] [Module 𝔽 W] (E : Set α) (f : α → W) :

Matroid α

The 𝔽-representable matroid given by a function f : α → W for a vector space W over 𝔽, and a ground set E : Set α.

Equations

Matroid.ofFun 𝔽 E f = (Module.matroid 𝔽 W).comapOn E f

Instances For

source

theorem Matroid.ofFun_congr {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {E : Set α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {v v' : α → W} (hvv' : Set.EqOn v v' E) :

Matroid.ofFun 𝔽 E v = Matroid.ofFun 𝔽 E v'

source

@[simp]

theorem Matroid.ofFun_indicator {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {E : Set α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {v : α → W} :

Matroid.ofFun 𝔽 E (E.indicator v) = Matroid.ofFun 𝔽 E v

source

noncomputable def Matroid.repOfFun {α : Type u_1} {W : Type u_3} [AddCommGroup W] (𝔽 : Type u_7) [DivisionRing 𝔽] [Module 𝔽 W] (E : Set α) (f : α → W) :

(Matroid.ofFun 𝔽 E f).Rep 𝔽 W

Equations

Matroid.repOfFun 𝔽 E f = ((Module.matroidRep 𝔽 W).comap f).restrict E

Instances For

source

theorem Matroid.repOfFun_coeFun_eq {α : Type u_1} {W : Type u_3} [AddCommGroup W] (𝔽 : Type u_7) [DivisionRing 𝔽] [Module 𝔽 W] (E : Set α) (f : α → W) :

⇑(repOfFun 𝔽 E f) = E.indicator f

source

theorem Matroid.repOfFun_coeFun_eq' {α : Type u_1} {W : Type u_3} [AddCommGroup W] (𝔽 : Type u_7) [DivisionRing 𝔽] [Module 𝔽 W] (E : Set α) (f : α → W) (hf : Function.support f ⊆ E) :

⇑(repOfFun 𝔽 E f) = f

source

@[simp]

theorem Matroid.repOfFun_image_eq {α : Type u_1} {W : Type u_3} [AddCommGroup W] (𝔽 : Type u_7) [DivisionRing 𝔽] [Module 𝔽 W] (E : Set α) (f : α → W) :

⇑(repOfFun 𝔽 E f) '' E = f '' E

source

theorem Matroid.repOfFun_apply {α : Type u_1} {W : Type u_3} {e : α} {E : Set α} [AddCommGroup W] (𝔽 : Type u_7) [DivisionRing 𝔽] [Module 𝔽 W] {v : α → W} (he : e ∈ E) :

(repOfFun 𝔽 E v) e = v e

source

instance Matroid.matroidOfFun_finitary {α : Type u_1} {W : Type u_3} [AddCommGroup W] (𝔽 : Type u_7) [DivisionRing 𝔽] [Module 𝔽 W] (f : α → W) (E : Set α) :

(Matroid.ofFun 𝔽 E f).Finitary

source

theorem Matroid.ofFun_finite {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (f : α → W) (E : Set α) (hfin : E.Finite) :

(Matroid.ofFun 𝔽 E f).Finite

source

@[simp]

theorem Matroid.ofFun_ground_eq {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {v : α → W} {E : Set α} :

(Matroid.ofFun 𝔽 E v).E = E

source

@[simp]

theorem Matroid.ofFun_indep_iff {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {I : Set α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {v : α → W} {E : Set α} :

(Matroid.ofFun 𝔽 E v).Indep I ↔ LinearIndepOn 𝔽 v I ∧ I ⊆ E

source

@[simp]

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

Matroid.ofFun 𝔽 M.E ⇑v = M

source

theorem Matroid.ofFun_closure_eq {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {X : Set α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {v : α → W} {E : Set α} (hvE : Function.support v ⊆ E) :

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

source

theorem Matroid.ofFun_closure_eq_of_subset_ground {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {X : Set α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {v : α → W} {E : Set α} (hXE : X ⊆ E) :

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

source

theorem Module.Basis.ofFun_isBase {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {v : α → W} {E B : Set α} (b : Basis (↑B) 𝔽 W) (hfb : ∀ (x : ↑B), v ↑x = b x) (hBE : B ⊆ E) :

(Matroid.ofFun 𝔽 E v).IsBase B

source

@[simp]

theorem Matroid.ofFun_zero {α : Type u_1} {W : Type u_3} [AddCommGroup W] (𝔽 : Type u_7) [Field 𝔽] [Module 𝔽 W] (E : Set α) :

Matroid.ofFun 𝔽 E 0 = loopyOn E