injective function

Stream: new members

[Busiso Chisala]

Is there an easy way to formulate/prove the existence of an injective function from finite set A to B given that the cardinalities (?) allow? The choose-using tactic will give a function (I guess) but ... I have the idea that a finset induction would do it, but worry there is a trivial way out there will save me the trouble. I want to use this in the 'extend to a basis' manner. Thanks

[Kevin Buzzard]

Can you formalise the precise statement which you want?

[Kevin Buzzard]

"finite set" can be said in several different ways in Lean and the answer to your question is probably "yes", but the details will depend on precisely how you want to state the maths assertion in type theory.

[Kevin Buzzard]

One thing I learnt very early on is that formalising the question is an important part of asking the question.

[Kevin Buzzard]

Another thing I learnt very early on is that choosing a random way to formalise the question and then solving it might lead to problems later when I want to apply the theorem I've already proved. I might find that it doesn't apply, because set.finite and fintype and finset are all different things.

[Kevin Buzzard]

In set theory, a set is a primitive notion and there is no question about what is meant. In type theory the type is the primitive notion, and various concepts of finite set can be built on top of this in different ways.

[Busiso Chisala]

An fintype indexed set of vectors v: ι → E some of which are zero, the rest linearly independent. Say on sets s,t :finset ι, respectively. Suppose that the dimension of E is |s|+|t| and I have a ready set of |s| vectors to complete my basis (say via a w: k → E). I suppose I am not very happy with how fin m objects work ... My use case is v: fin n → E. Must I really ?

[Kevin Buzzard]

Can you make a #mwe? A self-contained piece of code containing one sorry which is what you want filled in? This is the precise meaning of my original question.

[Kevin Buzzard]

This is an important skill to learn.

[Busiso Chisala]

I'll try

[Busiso Chisala]

I had some trouble, so this exercise was well worth it:

variables {n E:Type} [fintype n] [inner_product_space ℝ E] [finite_dimensional ℝ E]

-- rather than use 'fin k → E' I have used fintype n for illustration

local notation `⟪`x`, `y`⟫` := @inner ℝ _ _ x y

-- to simplify my statements

def is_orth (v: n → E) : Prop := ∀ i j:n, i ≠ j → ⟪v i, v j⟫=0

def is_nonzero (v: n → E) : Prop := ∀ i:n,  v i ≠ 0

def enlarges (v: n → E) (w: n → E) : Prop := ∀ i:n, v i ≠ 0 → w i = v i


example {v: n → E} (ho: is_orth v) : ∃ w: n → E, enlarges v w  ∧ is_orth w  ∧  is_nonzero w :=
begin
  let s := { i ∈ (finset.univ : finset n) | v i = 0 },
  have : ∃ z:fin (s.card) → E, is_orth z ∧ is_nonzero z := sorry ,
  -- would like to use z, which we can engineer to be in the orthogonal to v.range
  cases this with z hz,
  -- how to interweave z with v ?
  sorry
end

? use .val?

[Kevin Buzzard]

Here's what I came up with:

import data.fintype.basic

variables { m p :Type } [fintype m] [fintype p]

open fintype

example  {s: finset m} {h: s.card = fintype.card p} :
  ∃ f: p → m, function.injective f ∧ ∀ i:m, i ∈ s → ∃ t:p, i=f t :=
begin
  let S := {x : m // x ∈ s},
  have hS : fintype.card S = s.card,
    apply subtype_card, simp,
  rw [h, fintype.card_eq] at hS,
  cases hS with e,
  -- e is a bijection S -> p
  use (λ x, e.symm x),
  split,
  { intros x y hxy,
    apply equiv.injective e.symm,
    exact subtype.ext hxy },
  { intros i hi,
    use e ⟨i, hi⟩,
    simp }
end

[Kevin Buzzard]

Looking around in the library I found fintype.card_eq which says that if two fintypes have the same cardinality then there's an equiv between them, i.e. a bijection. I built the proof on that.

[Kevin Buzzard]

s is a finset so it's not a type, it's a term. The corresponding type is S.

[Busiso Chisala]

Kevin Buzzard said:

Looking around in the library I found fintype.card_eq which says that if two fintypes have the same cardinality then there's an equiv between them, i.e. a bijection. I built the proof on that.

Thanks ! I was about to moot an induction. This clears quite a few things :+1:

[Eric Wieser]

Can you use coe_sort s as the type instead rather than defining S? I can never remember how to input the coe_sort up arrow...

[Kevin Buzzard]

Probably -- but I have exactly the same problem!

[Eric Wieser]

Usually I resort to finding a lemma that does a coercion, and copying it from the goal window...