Define a (well defined) function using choice

Stream: Is there code for X?

[Antoine Chambert-Loir]

I want to define a function whose construction depends on several auxiliary choices, but does not depend on them, such as this:

variable {α β γ : Type*} {c : β → Prop} {p : β → α}

variable (f : Π b, c b → γ) (has_lift : ∀ a : α, ∃ b : β, c b ∧ p b = a)
  (lift_indep : ∀ b b' (hb : c b) (hb' : c b') (_ :  p b = p b'), f b hb = f b' hb')

def g (a : α) : γ := sorry

example (b : β) (hb : c b) : f b hb = g (p b) := sorry

I tried something for g, involving a lot of choose and choose_spec, but I can't prove the example afterwards.

NB. My actual situation is the following (it says that an element of a tensor product comes from something small, and
and two choices coincide in something small) :

open TensorProduct

variable {R : Type u} [CommSemiring R]
  {M N : Type*} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
  (f : Π (S : Type u) (_ : CommSemiring S) (_ : Algebra R S) (_ : S ⊗[R] M),
    S ⊗[R] N)
  (S : Type*) [CommSemiring S] [Algebra R S]

theorem hasLift (x : S ⊗[R] M) :
    ∃ (S' : Type u) (_: CommSemiring S') (_ : Algebra R S') (j : S' →ₐ[R] S) (x' : S' ⊗[R] M),
    LinearMap.rTensor M j.toLinearMap x' = x := by
  sorry

theorem isLiftUnique
    (S' : Type u) [CommSemiring S'] [Algebra R S'] (j' : S' →ₐ[R] S)
    (x' : S' ⊗[R] M)
    (S'' : Type u) [CommSemiring S''] [Algebra R S''] (j'' : S'' →ₐ[R] S)
    (x'' : S'' ⊗[R] M)
    (h : LinearMap.rTensor M j'.toLinearMap x' = LinearMap.rTensor M j''.toLinearMap x'') :
    ∃ (T : Type u) (_ : CommSemiring T) (_ : Algebra R T) (j : T →ₐ[R] S)
      (k' : S' →ₐ[R] T) (k'' : S'' →ₐ[R] T),
      j.comp k' = j' ∧ j.comp k'' =j'' ∧
      LinearMap.rTensor M k'.toLinearMap x' = LinearMap.rTensor M k''.toLinearMap x'' := by
  sorry

noncomputable def liftAux (x : S⊗[R] M)
  (S' : Type u) (hC : CommSemiring S') (hA : Algebra R S') (j : S' →ₐ[R] S) (x' : S' ⊗[R] M) (_ : LinearMap.rTensor M j.toLinearMap x' = x) : S ⊗[R] N :=
  LinearMap.rTensor N j.toLinearMap (f S' hC hA x')

noncomputable def lift (x : S ⊗[R] M) :
    S ⊗[R] N := by
    let S' := (hasLift S x).choose
    let hCS' : CommSemiring S' := (hasLift S x).choose_spec.choose
    let hAS' : Algebra R S' := (hasLift S x).choose_spec.choose_spec.choose
    let j : S' →ₐ[R] S := (hasLift S x).choose_spec.choose_spec.choose_spec.choose
    let x' : S' ⊗[R] M  := (hasLift S x).choose_spec.choose_spec.choose_spec.choose_spec.choose
    let hx' := (hasLift S x).choose_spec.choose_spec.choose_spec.choose_spec.choose_spec
    exact liftAux f S x S' hCS' hAS' j x' hx'

[Sabrina Jewson]

Probably not the best solution, but this works:

variable {α β γ : Type u} {c : β → Prop} {p : β → α}

variable (f : ∀ b, c b → γ) (has_lift : ∀ a : α, ∃ b : β, c b ∧ p b = a)
  (lift_indep : ∀ b b' (hb : c b) (hb' : c b') (_ :  p b = p b'), f b hb = f b' hb')

noncomputable def g (a : α) : γ :=
  have ⟨b, hb, _⟩ := Classical.indefiniteDescription _ (has_lift a)
  f b hb

example (b : β) (hb : c b) : f b hb = g f has_lift (p b) :=
  match e : Classical.indefiniteDescription _ (has_lift (p b)) with
    | ⟨b', hb', h⟩ => by rw [g, e]; exact lift_indep b b' hb hb' h.symm

[Riccardo Brasca]

Have you had a look at the choose tactic? I am not sure it applies here, but it can help.

[Antoine Chambert-Loir]

I'll have a look. For the moment, I'm trying to understand Quot (and there's a bug in mathlib4_docs that when you click on docs#Quot.lift, you go nowhere, because the opaque definition has no link).
And I'm stuck with the definition of a Sigma type on which my relation would live:

variable {α β γ : Type*} (c : β → Prop) {p : β → α}
#check Σ b, c b -- fails

I expected the failing type to be a choice of b such that c b holds, but…

[Antoine Chambert-Loir]

This is really strange :

#check Sigma -- Sigma.{u, v} {α : Type u} (β : α → Type v) : Type (max u v)
variable {α β γ : Type*} (c : β → Prop)
#check c -- c : β → Prop
#check Sigma c -- type mismatch  c b has type  Prop : Type
  -- but is expected to have type   Type ?u.165704 : Type (?u.165704 + 1)

[Edward van de Meent]

i suppose the error itself does make sense, as Prop is not the same as Type u for some u. it seems like you actually want setOf c? see docs#setOf

[Edward van de Meent]

in that case, you will be able to turn x:setOf c into b:β and hb:c b using obtain ⟨b,hb⟩ := x

[Matt Diamond]

a choice of b such that c b holds

you want Subtype, not Sigma

[Edward van de Meent]

isn't that basically the same thing?

[Edward van de Meent]

as setOf, i mean?

[Antoine Chambert-Loir]

Well, my minimal example was too minimal, for my c is really Type-valued. I made it Prop for the sake of minimizing my example and got into an additional problem. With Type, the sigma type problem that you explained disappears and I need something such as:

variable {α β γ : Type*} (c : β → Type*) {p : β → α}
  (f : Π b, c b → γ)
  (has_lift : ∀ a : α, ∃ (b : β) (h : c b), p b = a)
  (lift_indep : ∀ b b' (hb : c b) (hb' : c b') (_ :  p b = p b'), f b hb = f b' hb')

def g : α → γ := by sorry

theorem g_comp_p (b : β) (hb : c b) : g (p b) = f b hb  := sorry

[Kevin Buzzard]

Antoine Chambert-Loir said:

This is really strange :

#check Sigma -- Sigma.{u, v} {α : Type u} (β : α → Type v) : Type (max u v)
variable {α β γ : Type*} (c : β → Prop)
#check c -- c : β → Prop
#check Sigma c -- type mismatch  c b has type  Prop : Type
  -- but is expected to have type   Type ?u.165704 : Type (?u.165704 + 1)

If the strangeness is supposed to be the c b in the final output then I can't reproduce -- did you have a b later on in the file?

[Antoine Chambert-Loir]

(yes, many things later on, I probably should have sectioned it…)

[Antoine Chambert-Loir]

Riccardo Brasca said:

Have you had a look at the choose tactic? I am not sure it applies here, but it can help.

In my toy example, I could do this:

variable {α β γ : Type*} (c : β → Type*) (p : β → α)
  (f : Π b, c b → γ)
  (has_lift : ∀ a : α, ∃ (b : β) (_ : c b), p b = a)
  (lift_indep : ∀ {b b'} {hb : c b} {hb' : c b'} (_ :  p b = p b'), f b hb = f b' hb')

noncomputable def G : { g : α → γ // ∀ (b : β) (hb : c b), g (p b) = f b hb } := by
  choose lift cond_lift proj_lift using has_lift
  use fun a ↦ f (lift a) (cond_lift a), fun b hb ↦ lift_indep (proj_lift (p b))

Now, I'll try with my real life application.

[Kevin Buzzard]

Before you try -- can you prove anything about this definition?

[Antoine Chambert-Loir]

Yes, because the out-type of Gcontains the property that characterizes g.