linear_pmap_class

Stream: maths

[Moritz Doll]

Jireh Loreaux said:

Note: before we dive headlong into making that linear_pmap_class (which we should definitely do!), we should have a discussion about how to implement it, because I'm reasonably sure it won't be able to extend fun_like in any nice way.

So maybe we want to have a pfun_,like class hierarchy. Perhaps we don't, but I think we should outline the various partial function situations that commonly arise and see if there is any shot at unifying them, or if it isn't worth the effort to make a general framework.

@Jireh Loreaux @Anatole Dedecker let's move here.

[Moritz Doll]

The issue with pfun is that it is implemented differently than linear_pmap, even if it were implemented as a pair of domain and total function, I guess we might run into stupid coercion issues because linear_pmap's domain is a submodule and not a set.

[Moritz Doll]

My thought was that linear_pmap_class does not extend anything, but probably is extended by linear_map_class (taking top as domain), this has the annoying issue that there are two different coercions, the usual one and the one from the top-submodule to the codomain.

[Moritz Doll]

the linear_map_class would of course get a field that knows that these two coercions are equal and that should make it possible to transfer definitions for linear_pmap_class to linear_map_class. The downside is that there is some boilerplate involved, but I am afraid we cannot avoid that

[Jireh Loreaux]

My idea for pfun_like was that one of the arguments would be a set_like, which might address the fact that they aren't actually sets, but I haven't actually checked whether or not this idea works.

[Jireh Loreaux]

This would unify the implementations.

[Moritz Doll]

that would be great if it works

[Jireh Loreaux]

The other option (which works and is maybe the correct approach), is just to ignore the extra structure when creating the pfun_like and just use the bare sets underlying the fancy subobjects.

[Jireh Loreaux]

This morning I played around with some of these ideas. Using set_like I think can make this reasonable. However, I ran into some issues unrelated to set_like. Below are two attempts at getting the idea off the ground. Note that I was following the pattern of linear_pmap rather than pfun since the former is our real use case.

In the first approach, we encounter heterogeneous equality (yuck), and in the second approach, it goes against our current approach to f : linear_pmap R E F, where we only have a function f.to_fun : f.domain → F instead of a function E → F with junk values. Thoughts?

import linear_algebra.linear_pmap

--------- take 1 -----------

-- gross, heterogeneous equality is unavoidable if we want to have any sort of "extensionality"
-- also, unlike `fun_like`, we can't have dependent functions here (i.e., `β : Type*`, not
-- `β : α → Type*`)
class pfun_like (F : Type*) (α : out_param Type*) (γ : out_param Type*) (β : out_param Type*)
  [set_like γ α] :=
(domain : F → γ)
(coe : Π (f : F), (domain f) → β)
(ext : Π (f g : F), domain f = domain g → coe f == coe g → f = g)

namespace pfun_like

instance {F α γ β : Type*} [set_like γ α] [pfun_like F α γ β] :
  has_coe_to_fun F (λ f, (domain f : γ) → β) :=
{ coe := coe }

-- gross, we have to pass `[Π (f : F), has_zero ↥(domain f : γ)]` as a parameter and so there is
-- no way we can make this extend `pfun_like`. In practice, when creating instances of this class,
-- the Π-type instance should be inferred (e.g., if `F` is `linear_pmap_class R E F`, then
-- `domain f : submodule R E` which has a `module` instance), so in that case it wouldn't be a
-- headache, I guess?
class pmap_zero_class (F : Type*) (α : out_param Type*) (γ : out_param Type*) (β : out_param Type*)
  [set_like γ α] [has_zero β] [pfun_like F α γ β] [Π (f : F), has_zero ↥(domain f : γ)] :=
(map_zero : ∀ (f : F) (x : (domain f : γ)), f 0 = 0)

-- gross, we have to pass `[Π (f : F), has_zero ↥(domain f : γ)]` as a parameter and so there is
-- no way we can make this extend `pfun_like`.
class pmap_add_class (F : Type*) (α : out_param Type*) (γ : out_param Type*) (β : out_param Type*)
  [set_like γ α] [has_add β] [pfun_like F α γ β] [Π (f : F), has_add ↥(domain f : γ)] :=
(map_add : ∀ (f : F) (x y : (domain f : γ)), f (x + y) = f x + f y)

-- note that this approach never really had the changes to make use of the `set_like` instance,
-- aside from providing a `coe_to_sort` instance.
end pfun_like

--------- take 2 -----------

-- in this iteration, we just have a bare function from `α → β` (presumably filled in with junk
-- values in practice), so there is no need for heterogeneous equality in our extensionality.
-- Also, this *could* support dependent functions, although I didn't set it up that way here.
class pfun_like₂ (F : Type*) (α : out_param Type*) (γ : out_param Type*) (β : out_param Type*)
  [set_like γ α] :=
(domain : F → γ)
(coe : Π (f : F), α → β)
(ext : Π (f g : F), domain f = domain g → (∀ (x : α), x ∈ domain f → coe f x = coe g x) → f = g)

namespace pfun_like₂

instance {F α γ β : Type*} [set_like γ α] [pfun_like₂ F α γ β] :
  has_coe_to_fun F (λ _, α → β) :=
{ coe := coe }

-- note: this is weird in a *different* way from `pmap_zero_class`, which is that it doesn't need
-- to assume anything about the relationship between `γ` and `0` (e.g., there is no need for
-- `zero_mem_class γ α` here).
class pmap_zero_class₂ (F : Type*) (α : out_param Type*) (γ : out_param Type*) (β : out_param Type*)
  [set_like γ α] [has_zero α] [has_zero β] extends pfun_like₂ F α γ β :=
(map_zero : ∀ f : F, f 0 = 0)

-- Here we see the key distinction with our normal set up for `linear_pmap`. In particular, we have
-- as hypotheses for `foo` that `x y ∈ domain f`, instead of `x y : domain f` because our coercion
-- of `f` to a function takes it to `α → β`, not `domain f → β`.
class pmap_add_class₂ (F : Type*) (α : out_param Type*) (γ : out_param Type*) (β : out_param Type*)
  [set_like γ α] [has_add α] [has_add β] extends pfun_like₂ F α γ β :=
(map_add : ∀ (f : F) (x y ∈ domain f), f (x + y) = f x + f y)

end pfun_like₂

[Jireh Loreaux]

Note: Moritz, with the second approach, we would definitely not be able to have an instance of linear_pmap_class for linear_map_class because we would end up having two definitionally non-equal has_coe_to_fun instances (at least in practice).

[Frédéric Dupuis]

Have you also considered copying the design of fun_like, but replacing the coercion to a function by a coercion to a pfun?

[Jireh Loreaux]

Not yet, but I'll play around with that later.

[Jireh Loreaux]

I have some variations which seem to be working decently (the ones I posted above can be improved); but also one using pfun. Will update later.

[Jireh Loreaux]

Okay, this is the proof of concept. I define a pfun_like class and it's associated has_coe_to_fun instance. I also create a structure pmul_hom of partial mul_homs defined as a subsemigroup and mul_hom from this subsemigroup into some other semigroup. We extend pfun_like to pmul_hom_class with a new field pmap_mul. This field takes full advantage of the subobject refactor by making use of mul_mem_class.has_mul to make sense of the statement. Then we have a nice ext lemma (without any heterogeneous equality nonsense). In addition, we show that we can get the natural instances.

(Note: I'm not advocating for defining pmul_homs unless someone needs them, it's only to show that the idea works.)

All of this should also work for defining a linear_pmap_class modulo filling in missing stuff for set_like subobjects (e.g., zero_mem_class.has_zero is missing, and there is no smul_mem_class yet).

import group_theory.subsemigroup.operations
import data.pfun

class pfun_like (F : Type*) (α : out_param Type*) (γ : out_param Type*) (β : out_param Type*)
  [set_like γ α] :=
(domain : F → γ)
(coe : Π (f : F), (domain f) → β)
(coe_injective : Π (f g : F), domain f = domain g →
  (∀ (x : domain f) (y : domain g), (x : α) = (y : α) → coe f x = coe g y) → f = g)

namespace pfun_like

instance {F α γ β : Type*} [set_like γ α] [pfun_like F α γ β] :
  has_coe_to_fun F (λ f, (domain f : γ) → β) :=
{ coe := coe }

lemma ext {F α β γ : Type*} [set_like γ α] [pfun_like F α γ β] {f g : F} (h : domain f = domain g)
  (h' : ∀ ⦃x : (domain f : γ)⦄ ⦃y : (domain g : γ)⦄, (x : α) = (y : α) → f x = g y) : f = g :=
pfun_like.coe_injective f g h h'

end pfun_like

class pmul_hom_class (F : Type*) (α : out_param Type*) (γ : out_param Type*) (β : out_param Type*)
  [set_like γ α] [has_mul α] [has_mul β] [mul_mem_class γ α] extends pfun_like F α γ β :=
(pmap_mul : ∀ (f : F) (x y : (domain f : γ)), f (x * y) = f x * f y)

export pmul_hom_class (pmap_mul)

structure pmul_hom (α β : Type*) [has_mul α] [has_mul β] :=
(domain : subsemigroup α)
(to_mul_hom : domain →ₙ* β)

infixr ` →.ₙ* `:25 := pmul_hom

namespace pmul_hom

instance (α β : Type*) [has_mul α] [has_mul β] :
  pmul_hom_class (pmul_hom α β) α (subsemigroup α) β :=
{ domain := pmul_hom.domain,
  coe := λ f, f.to_mul_hom,
  coe_injective := λ f g h h',
  begin
    rcases f with ⟨f_dom, f⟩,
    rcases g with ⟨g_dom, g⟩,
    obtain rfl : f_dom = g_dom := h,
    obtain rfl : f = g := mul_hom.ext (λ x, h' _ _ rfl),
    refl,
  end,
  pmap_mul := λ f, map_mul f.to_mul_hom }

-- this would be our standard `ext` lemma
@[ext]
lemma ext {α β : Type*} [has_mul α] [has_mul β] {f g : α →.ₙ* β} (h : domain f = domain g)
  (h' : ∀ ⦃x : domain f⦄ ⦃y : domain g⦄, (x : α) = (y : α) → f x = g y) : f = g :=
pfun_like.coe_injective f g h h'

-- see? it works!
example {α β : Type*} [has_mul α] [has_mul β] (f : α →.ₙ* β) (x y : domain f) :
  f (x * y) = f x * f y :=
pmap_mul f x y

-- this instance seems dangerous: all of a sudden `α →ₙ* β` would have *two* `has_coe_to_fun`
-- instances, one coercing to `α → β` from the `fun_like` instance and another coercing to
-- `λ f, domain f → β` from the `pfun_like` instance, but maybe this isn't so much of a problem.
-- even if it is a problem, perhaps we can just solve it by lowering the priority on this one?
instance dangerous {α β : Type*} [has_mul α] [has_mul β] :
  pmul_hom_class (mul_hom α β) α (subsemigroup α) β  :=
{ domain := λ f, ⊤,
  coe := λ f x, match x with ⟨x, _⟩ := f x end,
  coe_injective := λ f g _ h, mul_hom.ext (λ x, h ⟨x, true.intro⟩ ⟨x, true.intro⟩ rfl),
  pmap_mul := λ f,
  begin
    simp_rw [set_like.forall],
    rintros x _ y _,
    exact map_mul f x y,
  end }

end pmul_hom

[Jireh Loreaux]

Another note: I think going through pfun is the wrong way to go. The reason is that you have to go all the way down to a set α instead of staying at the subobject level, which means that you would lose access to mul_mem_class. In a sense, pfun is too unbundled.

[Moritz Doll]

The instance seems to be too dangerous. I've tried to make a toy model of the kinds of definition I need and it fails because I cannot get the correct coercion, Lean really wants to coerce to pfun now. Lean was also a bit stupid in the second to last lemma, but this no problem because in that case you should not use the definition by hand anyways.

import group_theory.subsemigroup.operations
import data.pfun

class pfun_like (F : Type*) (α : out_param Type*) (γ : out_param Type*) (β : out_param Type*)
  [set_like γ α] :=
(domain : F → γ)
(coe : Π (f : F), (domain f) → β)
(coe_injective : Π (f g : F), domain f = domain g →
  (∀ (x : domain f) (y : domain g), (x : α) = (y : α) → coe f x = coe g y) → f = g)

namespace pfun_like

instance {F α γ β : Type*} [set_like γ α] [pfun_like F α γ β] :
  has_coe_to_fun F (λ f, (domain f : γ) → β) :=
{ coe := coe }

lemma ext {F α β γ : Type*} [set_like γ α] [pfun_like F α γ β] {f g : F} (h : domain f = domain g)
  (h' : ∀ ⦃x : (domain f : γ)⦄ ⦃y : (domain g : γ)⦄, (x : α) = (y : α) → f x = g y) : f = g :=
pfun_like.coe_injective f g h h'

end pfun_like

class pmul_hom_class (F : Type*) (α : out_param Type*) (γ : out_param Type*) (β : out_param Type*)
  [set_like γ α] [has_mul α] [has_mul β] [mul_mem_class γ α] extends pfun_like F α γ β :=
(pmap_mul : ∀ (f : F) (x y : (domain f : γ)), f (x * y) = f x * f y)

def is_comm {F α β γ : Type*} [set_like γ α] [has_mul α] [has_mul β] [mul_mem_class γ α]
  [pmul_hom_class F α γ β] (f : F) : Prop :=
  ∀ (x y : @pfun_like.domain F α γ β _ _ f), f (x * y) = f (y * x)

export pmul_hom_class (pmap_mul)

structure pmul_hom (α β : Type*) [has_mul α] [has_mul β] :=
(domain : subsemigroup α)
(to_mul_hom : domain →ₙ* β)

infixr ` →.ₙ* `:25 := pmul_hom

namespace pmul_hom

instance (α β : Type*) [has_mul α] [has_mul β] :
  pmul_hom_class (pmul_hom α β) α (subsemigroup α) β :=
{ domain := pmul_hom.domain,
  coe := λ f, f.to_mul_hom,
  coe_injective := λ f g h h',
  begin
    rcases f with ⟨f_dom, f⟩,
    rcases g with ⟨g_dom, g⟩,
    obtain rfl : f_dom = g_dom := h,
    obtain rfl : f = g := mul_hom.ext (λ x, h' _ _ rfl),
    refl,
  end,
  pmap_mul := λ f, map_mul f.to_mul_hom }

-- this would be our standard `ext` lemma
@[ext]
lemma ext {α β : Type*} [has_mul α] [has_mul β] {f g : α →.ₙ* β} (h : domain f = domain g)
  (h' : ∀ ⦃x : domain f⦄ ⦃y : domain g⦄, (x : α) = (y : α) → f x = g y) : f = g :=
pfun_like.coe_injective f g h h'

-- see? it works!
example {α β : Type*} [has_mul α] [has_mul β] (f : α →.ₙ* β) (x y : domain f) :
  f (x * y) = f x * f y :=
pmap_mul f x y

-- This also works
example {α β : Type*} [has_mul α] [has_mul β] (f : α →.ₙ* β) (h : is_comm f) (x y : domain f) :
  f (x * y) = f (y * x) := h x y

-- this instance seems dangerous: all of a sudden `α →ₙ* β` would have *two* `has_coe_to_fun`
-- instances, one coercing to `α → β` from the `fun_like` instance and another coercing to
-- `λ f, domain f → β` from the `pfun_like` instance, but maybe this isn't so much of a problem.
-- even if it is a problem, perhaps we can just solve it by lowering the priority on this one?
@[priority 10]
instance dangerous {α β : Type*} [has_mul α] [has_mul β] :
  pmul_hom_class (mul_hom α β) α (subsemigroup α) β  :=
{ domain := λ f, ⊤,
  coe := λ f x, match x with ⟨x, _⟩ := f x end,
  coe_injective := λ f g _ h, mul_hom.ext (λ x, h ⟨x, true.intro⟩ ⟨x, true.intro⟩ rfl),
  pmap_mul := λ f,
  begin
    simp_rw [set_like.forall],
    rintros x _ y _,
    exact map_mul f x y,
  end }

-- This also works
example {α β : Type*} [has_mul α] [has_mul β] (f : mul_hom α β) (h : is_comm f)
  (x y : @pfun_like.domain (mul_hom α β) α (subsemigroup α) β _ _ f) :
  f (x * y) = f (y * x) := h x y

-- This does not
example {α β : Type*} [has_mul α] [has_mul β] (f : mul_hom α β) (h : is_comm f)
  (x y : α) :
  is_comm f ↔ ∀ (x y : α), f (x * y) = f (y * x) :=
begin
  sorry,
end

end pmul_hom

[Jireh Loreaux]

yeah, that's what I was afraid of. I think Lean 3 is too dumb about how it handles coercion to functions (I think it literally picks the most recent instance). I also believe this might be something Lean 4 can handle, but I'm not sure.

[Moritz Doll]

If that is the case, then there would be a really nasty hack: just define the linear_pmap_class instance before the linear_map_class :scream:

[Moritz Doll]

I would really hope that Lean 4 is better in that regard

[Moritz Doll]

and thanks Jireh for taking the time to try out whether this is possible

[Moritz Doll]

Moritz Doll said:

If that is the case, then there would be a really nasty hack: just define the linear_pmap_class instance before the linear_map_class :scream:

for some weird reason this does not work in Lean 3, in Lean 4 it does. I really don't understand how Lean 3 finds instances.
Lean 4 seems to be able to deal with multiple CoeFun, but one actually has to be careful with the order they are defined in to get the default instance correct and changing the priority seems to have no effect on that (at least setting one to @[defaultInstance low] and the other to @[defaultInstance high])