Zulip Chat Archive

Stream: new members

Topic: injective function


view this post on Zulip Busiso Chisala (Nov 05 2020 at 12:21):

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

view this post on Zulip Kevin Buzzard (Nov 05 2020 at 12:22):

Can you formalise the precise statement which you want?

view this post on Zulip Kevin Buzzard (Nov 05 2020 at 12:23):

"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.

view this post on Zulip Kevin Buzzard (Nov 05 2020 at 12:24):

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

view this post on Zulip Kevin Buzzard (Nov 05 2020 at 12:26):

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.

view this post on Zulip Kevin Buzzard (Nov 05 2020 at 12:28):

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.

view this post on Zulip Busiso Chisala (Nov 05 2020 at 13:25):

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 ?

view this post on Zulip Kevin Buzzard (Nov 05 2020 at 13:27):

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.

view this post on Zulip Kevin Buzzard (Nov 05 2020 at 13:28):

This is an important skill to learn.

view this post on Zulip Busiso Chisala (Nov 05 2020 at 13:28):

I'll try

view this post on Zulip Busiso Chisala (Nov 05 2020 at 15:26):

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?

view this post on Zulip Kevin Buzzard (Nov 06 2020 at 11:42):

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

view this post on Zulip Kevin Buzzard (Nov 06 2020 at 11:43):

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.

view this post on Zulip Kevin Buzzard (Nov 06 2020 at 11:44):

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

view this post on Zulip Busiso Chisala (Nov 06 2020 at 13:38):

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:

view this post on Zulip Eric Wieser (Nov 06 2020 at 14:23):

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...

view this post on Zulip Kevin Buzzard (Nov 06 2020 at 17:51):

Probably -- but I have exactly the same problem!

view this post on Zulip Eric Wieser (Nov 07 2020 at 11:42):

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


Last updated: May 11 2021 at 14:11 UTC