Relation between functions induced by embedding

Stream: new members

[Markus Schmaus]

Let's say I have a function ι : α → β, which I can interpret as an embedding.

I can use this to define a relation between functions f : α → α and g : β → β, stating that from the perspective of ι doing f in α is the same as doing g in β:

def sameish {α β : Type u} (ι : α → β)
    (f : α → α) (g : β → β) : Prop :=
  g ∘ ι = ι ∘ f

I can do a similar construction for functions with much more complex Type signatures, for example

def sameish' {α β : Type u} (ι : α → β)
    {p : β → Prop} {γ : Type v}
    (f : Nat → (x : α) → γ → (h : p (ι x)) → α)
    (g : Nat → (x : β) → γ → (h : p x) → β) : Prop :=
  ∀ n x y h, ι (f n x y h) = g n (ι x) y h

Is it possible to create a relation that works for any function of any type signature? Does this already exist somewhere in Lean or Mathlib? I guess this relation must be well known in the literature, what's its name?

[Matt Diamond]

docs#Function.Semiconj

[Matt Diamond]

not sure if there's a generalization like the one you're asking for

[Matt Diamond]

actually I'm not really sure what you're asking for... what do you mean by "a relation that works for any function of any type signature"? what would the type signature of such a relation look like?

[Markus Schmaus]

Thanks, I knew something like this had to exist in Mathlib. docs#Function.Semiconj₂ already generalizes this concept somewhat. And here is a further generalization (I didn't give too many thoughts on naming).

import Mathlib

inductive Sig where
  | codom (α : Type u) : Sig
  | dom (α : Type u) (s : Sig) : Sig
  | codomX : Sig
  | domX (s : Sig) : Sig

def Sig.ofList : List (Option (Type u)) → Option (Type u) → Sig
  | [], none => Sig.codomX
  | [], some α => Sig.codom α
  | none :: s, x => Sig.domX (Sig.ofList s x)
  | some α :: s, x => Sig.dom α (Sig.ofList s x)

def Sig.type (X : Type u): Sig → Type u
  | Sig.codom α => α
  | Sig.dom α s => α → (Sig.type X s)
  | Sig.codomX => X
  | Sig.domX s => X → (Sig.type X s)

def Sig.Semiconj (s : Sig) {α β : Type u} (f : α → β)
    (ga : Sig.type α s) (gb : Sig.type β s) : Prop :=
  match s with
  | Sig.codom _ => ga = gb
  | Sig.dom γ s => ∀ a : γ, Sig.Semiconj s f (ga a) (gb a)
  | Sig.codomX => f ga = gb
  | Sig.domX s => ∀ a : α, Sig.Semiconj s f (ga a) (gb (f a))

def Sig.SimiconjX {α β : Type u} (f : α → β)
    (ga : γa) (gb : γb) : Prop :=
  ∃ s, ∃ (ca : γa = Sig.type α s), ∃ (cb : γb = Sig.type β s),
  Sig.Semiconj s f (cast ca ga) (cast cb gb)

example {α β : Type u} (f : α → β) (ga : α → α) (gb : β → β ) :
    Function.Semiconj f ga gb = Sig.Semiconj (Sig.ofList [none] none) f ga gb := by
  simp only [Function.Semiconj, Sig.Semiconj]

example {α β : Type u} (f : α → β) (ga : α → α → α) (gb : β → β → β ) :
    Function.Semiconj₂ f ga gb = Sig.Semiconj (Sig.ofList [none, none] none) f ga gb := by
  simp only [Function.Semiconj, Sig.Semiconj]

One limitation of this construction is that all the other types in Sig need to be from the same universe. It also doesn't handle the dependently typed case. Generalizing to these cases starts to become messy, so I was hoping someone else had already dealt with that.

[Markus Schmaus]

To any interested future reader, this is what I have come up with. I can proof that it extends Function.Semiconj, but I haven't tested how well it works for any other use case.

import Mathlib

/-- An inductive type representing the signature of a function with some
unbound positions, to allow for type dependency this assumes that any such
dependency factors through a type `model`, the default `PUnit` implies that
there is no such dependency. -/
inductive AbstractSignature (model : Type u := PUnit) where
  /-- The final return value has type `α` -/
  | codom (α : Type v) : AbstractSignature model
  /-- The final return value has an unbound -/
  | codomUnbound : AbstractSignature model
  /-- The next argument has type `α`, and the remaining type signature
  depends via `sf` -/
  | dom (α : Type v) (sf : α → AbstractSignature model) : AbstractSignature model
  /-- The next argument has unbound type, and the remaining type signature
  depends via `sf` -/
  | domUnbound (sf : model → AbstractSignature model) : AbstractSignature model

namespace AbstractSignature

/-- Construct a non-dependent `AbstractSignature` from a `List` of types. -/
def ofList : List (Option (Type u)) → Option (Type u) → AbstractSignature
  | [], some α => .codom α
  | [], none => .codomUnbound
  | some α :: tail, out => .dom α (fun _ => ofList tail out)
  | none :: tail, out => .domUnbound (fun _ => ofList tail out)

/-- Construct a concrete type from an `AbstractSignature`, fill in positions in
the domain with the domain of `m` which is used to resolve type dependency,
the type of the codomain can be specified speratly, but defaults to the same type. -/
def type {model : Type u} (s : AbstractSignature model) {imp : Type u}
    (m : imp → model) (codom : Type u := imp) : Type u :=
  match s with
  | .codom α => α
  | .codomUnbound => codom
  | .dom α sf => (x : α) → (type (sf x) m codom)
  | .domUnbound sf => (x : imp) → (type (sf (m x)) m codom)

/-- Compose `f` after `g` in the ultimate codomain, unlike with the usual
composition by `∘`, `g` is allowed to have multiple curried arguments, as
specified by `s`, if the ultimate codomain is not unbound in `s`,
then this is a noop. -/
def comp {model : Type u} (s : AbstractSignature model) {α β : Type u} (f : α → β)
    {m : α → model} (g : s.type m) : s.type m β :=
  match s with
  | .codom _ => g
  | .codomUnbound => f g
  | .dom _ sf => fun x => comp (sf x) f (g x)
  | .domUnbound sf => fun x : α => comp (sf (m x)) f (g x)

/-- Compose `g` after `f` in the unbound arguments, as specified by `s`, unlike
with the usual composition by `∘`, `g` is allowed to have multiple curried
arguments, if there are no unbound arguments in `s`, then is is a noop. -/
def lift {model : Type u} (s : AbstractSignature model) {α β : Type u}
    {m : β → model} (g : s.type m) (f : α → β) : s.type (m ∘ f) β :=
  match s with
  | .codom _ => g
  | .codomUnbound => g
  | .dom _ sf => fun x => lift (sf x) (g x) f
  | .domUnbound sf => fun x : α => lift (sf ((m ∘ f) x)) (g (f x)) f

/-- A function `f` semiconjugates two functions `ga` and `gb` with signatures
specified by `s` if `comp s f ga = lift s gb f`, this generalizes
[Function.Semiconj] and [Function.Semiconj₂]. -/
def Semiconj {model : Type u} (s : AbstractSignature model) {α β : Type u} (f : α → β)
    [m : Inhabited (β → model)] (ga : type s (m.default ∘ f)) (gb : type s m.default) : Prop :=
  comp s f ga = lift s gb f

/-- Proof that [Function.Semiconj] is indeed a special case of
[AbstractSignature.Semiconj]. -/
theorem semiconj_eq_function_semiconj {α model : Type u} (f : α → model)
    (ga : α → α) (gb : model → model ) :
    Semiconj (ofList [none] none) f ga gb = Function.Semiconj f ga gb := by
  simp only [Function.semiconj_iff_comp_eq, Function.comp_def, Semiconj, Pi.default_def,
    PUnit.default_eq_unit, comp, lift]

/-- Proof that [Function.Semiconj₂] is indeed a special case of
[AbstractSignature.Semiconj]. -/
example {α model : Type u} (f : α → model) (ga : α → α → α) (gb : model → model → model ) :
    Semiconj (ofList [none, none] none) f ga gb = Function.Semiconj₂ f ga gb := by
  simp only [Function.Semiconj₂, Semiconj, Pi.default_def, PUnit.default_eq_unit, Function.comp_def,
    comp, lift, eq_iff_iff]
  simp only [← Function.funext_iff]