passing to the quotient via surjective maps

Stream: new members

[Antoine Chambert-Loir]

I have an explicit surjective map p : X -> Y and a map g : X -> T such that p(x) = p(x') implies g(x)=g(x'); how can I define the unique function f : Y -> Tsuch that f o p = g?

I can do it like this, but I am certain that there is a simpler way ? Is it necessary to pass through the quotient infrastructure ?

open function
variables (α β γ : Type*)

lemma factor (p : α → β) (hp : surjective p) (g : α → γ) (hpg : ∀ (x y : α), p(x) = p(y) → g(x) = g(y)) :
  ∃ (f: β → γ), comp f p = g :=
  begin
    obtain ⟨q, hq⟩ := surjective.has_right_inverse hp,
    use comp g q,
    ext x,
    simp only [comp_app],
    exact hpg (q (p x)) x (hq (p x))
  end

[Johan Commelin]

Passing through quotient still wouldn't give you a map out of Y, right.

[Kevin Buzzard]

[usual #mwe moan -- your code doesn't paste]

[Kevin Buzzard]

You don't need the simp only [comp_app],, it's definitional.

[Kevin Buzzard]

The quotient infrastructure would give you a map out of quotient R for some R :-/

[Antoine Chambert-Loir]

Kevin Buzzard said:

[usual #mwe moan -- your code doesn't paste]

It was copy pasted from VSCode, but I forgot to include the open function line, sorry !

[Kevin Buzzard]

And the import tactic line ;-)

[Johan Commelin]

import logic.function.basic

open function

variables {α β γ : Type*}

noncomputable
def function.surjective.lift {p : α → β} (hp : surjective p) (g : α → γ) :
  β → γ :=
g ∘ hp.has_right_inverse.some

lemma function.surjective.lift_eq (p : α → β) (hp : surjective p) (g : α → γ)
  (hg : ∀ {x y}, p x = p y → g x = g y) :
  hp.lift g ∘ p = g :=
funext $ λ x, hg $ hp.has_right_inverse.some_spec _ -- edit to include final `_`

[Kevin Buzzard]

Johan is making an API for surjections analogous to the API for quotient.

[Antoine Chambert-Loir]

Kevin Buzzard said:

And the import tactic line ;-)

What is this line ? I fear I'm missing some magic here…

[Johan Commelin]

You can't use the ext tactic if you don't import it.

[Johan Commelin]

import tactic at the top of the file gives you (almost) all tactics.

[Antoine Chambert-Loir]

But I don't have this line at the top of my file !

[Johan Commelin]

Right, so you should see errors.

[Johan Commelin]

I had errors when I copy-pasted your snippet.

[Kevin Buzzard]

use is also not a core lean tactic

[Johan Commelin]

Nor is obtain

[Antoine Chambert-Loir]

Capisco, I had an import data.fintype.basic (because my sandbox.lean file has many purposes) and I presume that this import was doing the job!

[Adam Topaz]

@Antoine Chambert-Loir docs#setoid.ker and docs#setoid.quotient_ker_equiv_of_surjective would be helpful to relate the surjective map to the quotient api in this case.

[Antoine Chambert-Loir]

@Johan Commelin
Your version renders an error,

type mismatch at application
  hg (Exists.some_spec hp.has_right_inverse)
term
  Exists.some_spec hp.has_right_inverse
has type
  right_inverse (Exists.some _) p
but is expected to have type
  p ?m_1 = p ?m_2

(but I don't understand it, because I don't understand the $ ... $constructions (and can't find their explanation in the docs, while I'm sure I've read it once!)

[Johan Commelin]

f $ g x = f (g x). It just reduced the amount of ().

[Johan Commelin]

So f $ g $ h x = f (g (h x))

[Johan Commelin]

My code compiles on my side. So I don't know what's wrong.

[Kevin Buzzard]

It doesn't compile on today's master

[Johan Commelin]

Oops, let me update my lean

[Johan Commelin]

-- rano% git show | head -1
-- commit 812431404d4669d4e055e2a790e964068ba5ac92
-- rano% cat src/demo.lean
import logic.function.basic

open function

variables {α β γ : Type*}

noncomputable
def function.surjective.lift {p : α → β} (hp : surjective p) (g : α → γ) :
  β → γ :=
g ∘ hp.has_right_inverse.some

lemma function.surjective.lift_eq (p : α → β) (hp : surjective p) (g : α → γ)
  (hg : ∀ {x y}, p x = p y → g x = g y) :
  hp.lift g ∘ p = g :=
funext $ λ x, hg $ hp.has_right_inverse.some_spec _
-- rano% lean src/demo.lean
-- rano%

[Johan Commelin]

I seem to be on latest master, end Lean compiles this without error

[Kevin Buzzard]

type mismatch at application
  hg (Exists.some_spec hp.has_right_inverse)
term
  Exists.some_spec hp.has_right_inverse
has type
  right_inverse (Exists.some _) p
but is expected to have type
  p ?m_1 = p ?m_2

also on commit 812431404d4669d4e055e2a790e964068ba5ac92

[Kevin Buzzard]

Error on the $ in funext $ λ x, hg $ hp.has_right_inverse.some_spec

[Eric Wieser]

Is has_right_inverse.some just docs#function.surj_inv?

[Kevin Buzzard]

Oh lol your first post doesn't work and your second one does

[Kevin Buzzard]

The first time you posted you missed off the final _

[Johan Commelin]

Oops, copy-paste-error :sorry: