Finitely supported restriction

Stream: maths

[Seb Roach]

Hi, I have a finitely supported map for the coefficients of a linear combination of vectors. Its domain is Sum A Unit, and I want to restrict it to just A. This is so I can use the restriction (also a finitely supported function) to define the linear combination of a subfamily of vectors.

[Yaël Dillies]

Are you looking for docs#Finsupp.comapDomain ?

[Seb Roach]

(deleted)

[Seb Roach]

sorry thanks this it it

[Seb Roach]

(deleted)

[Seb Roach]

Just struggling with the proof of infectivity unfortunately. What if by definition the function f is injective, since it is Sum.inl? I can't seem to invoke properties of Sum.inl to apply to f

[Aaron Liu]

Can you please post your code in #backticks so I don't have to work to inspect it?

[Kevin Buzzard]

Read #backticks and #mwe and then edit your above post so that it becomes a better question; this will make you more likely to get a good answer.

[Seb Roach]

import mathlib

lemma Sum_inl_inj_on_preimage {A B K : Type*} [Field K]
  (l : Sum A B →₀ K) (f : A → Sum A B := Sum.inl) :
  Set.InjOn f (f ⁻¹' (↑l.support : Set (Sum A B))) := by

  intros a1 ha_in1 a2 ha_in2 ha_eq


  exact Sum.inl_injective ha_eq




def left_fun (l : Sum ι Unit →₀ K) (f : ι → Sum ι Unit := Sum.inl) : ι →₀ K :=
Finsupp.comapDomain f l (Sum_inl_inj_on_preimage l f)

Apologies

[Aaron Liu]

When you write

def left_fun (l : Sum ι Unit →₀ K) (f : ι → Sum ι Unit := Sum.inl) : ι →₀ K :=
  ...

this means that left_fun takes two arguments called l and f, and f can be anything but if the user doesn't specify then it's Sum.inl by default. If you meant to define f as Sum.inl then you can write

def left_fun (l : Sum ι Unit →₀ K) : ι →₀ K :=
  let f : ι → Sum ι Unit := Sum.inl
  ...

[Aaron Liu]

Once you do this, you can use docs#Sum.inl_injective and docs#Set.injOn_of_injective instead of proving it yourself.

[Seb Roach]

Thank you, and sorry for how trivial these errors are

[Kevin Buzzard]

Note that this link

view.png

conveniently supplied by Zulip, still does not work for your code. For the third time I suggest you read #mwe -- I'm trying to help. People click on these links, it doesn't work, and they give up. If you ask a better question you are more likely to get a good answer.

[Seb Roach]

import Mathlib

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]
variable {ι : Type*}  -- Index set for the original vectors
variable (v' : Sum ι Unit → V) (v: ι → V)  -- Full family of vectors, including u
axiom v_subset_v' : ∀ i : ι, v i = v' (Sum.inl i)

[Seb Roach]

Wondering how to proceed here? I want that the restricted coefficient function is in the kernel of the linear combination map of the vectors v \subset v'. I have that the original coefficient function is in the kernel of linear combination of v'

[Seb Roach]

thanks

[Seb Roach]

It is certainly possible this method of extending a family of vectors is suboptimal

[Aaron Liu]

Once again, (f : ι → Sum ι Unit := Sum.inl) means that f is a parameter with default value Sum.inl. It does not mean that f = Sum.inl.
Right now when I run your code I get a type mismatch near Finsupp.comapDomain f. If you fix your code or explain what you want to prove in words, I might be able to help you better.

[Seb Roach]

I scrapped the lemma, but given:
'''
l : Sum \iota Unit \r K
'''
is a non-zero function only on iota, and the linear combination of v' above with l is zero.
Then the restriction of l using Finsupp.comapDomain I want to create a zero linear combination with v.
Noting that v is a subset of v' defined above.

[Seb Roach]

image.png

[Seb Roach]

This idea if \lambda is zero

[Aaron Liu]

This is my best guess. Did I get it right?

import Mathlib

example {K V ι : Type*} [Semiring K] [AddCommMonoid V] [Module K V]
    {s : Finset ι} {u : V} {v : ι → V} {lu : K} {lv : ι → K}
    (hv : ∑ i ∈ s, lv i • v i ≠ 0) (h : lu • u + ∑ i ∈ s, lv i • v i = 0) : lu ≠ 0 := by
  rintro rfl
  apply hv
  simpa using h

[Seb Roach]

Thanks