advice for defining bundled hom and equiv structures

Stream: mathlib4

[Edward van de Meent]

i'd like to define bundled hom and equiv structures for Codes (which i have defined in my personal branch), and i'd like to know how i should go about extending existing structs, like Equiv and such...
looking through how this was done for other structures, i have some specific questions i'd like to know the answer to, but general advice is also welcome.

1. Looking at LinearEquiv, it doesn't seem to explicitly require σ or σ' to be a ring-isomorphism, rather requiring them to be of type R →+* S and S →+* R respectively, and having parameters RingHomInvPair σ σ' and RingHomInvPair σ' σ, both of which contain fields stating that composing them either way gives id on either ring. why is this defined like this?

2. Looking at the same, i noticed that in the code, it extends M ≃+ M₂, while the snippet in the documentation doesn't... why is this?

3. It extends both LinearMap σ M M₂ and M ≃+ M₂. The left inheritance reveals a structure AddHom, and so does the right. there doesn't appear to be any field stating the values of these structures are the same... It is my understanding that if this were a class, this would lead to diamond issues, but because this is a structure, it doesn't. However, there is no field stating these fields are the same either. Does lean know these need to be the same by itself, or is this specified somewhere I overlooked?

4. Similarly, RingEquiv extends R ≃ S,R ≃* S and R ≃+ S (but only the first is mentioned in the documentation)... If lean knows to unify the R ≃ S field, why is it needed to explicitly state it as an extension in the code? Why doesn't it only extend R ≃* S and R ≃+ S?

5. If lean knows to unify these fields, why can't the same be done with classes? Why doesn't lean solve diamond issues by itself?

[Anne Baanen]

1. I believe this is so that turning a linear equivalence (not semilinear equivalence) into a semilinear map gives an actual linear map: RingHom.id instead of (RingEquiv.refl _).toRingHom. We are having similar issues in #6057 where Lean expects MonoidHom.id but gets (RingHom.id _).toMonoidHom.
2. You mean in the autogenerated declaration at docs#LinearEquiv it doesn't mention extends AddEquiv? I'm not sure why that happens, maybe the diamond inheritance that you mention? In most cases, it is much better to follow the actual code than the autogenerated documentation.
3. There is in fact diamond inheritance, but for both structures and classes this is not an issue. What happens under the hood is that a structure like LinearEquiv will look like a field toLinearMap containing everything from LinearMap and then separately all the fields that are in AddEquiv but not in LinearMap: invFun, left_inv and right_inv. When you want to apply LinearEquiv.toAddEquiv, under the hood it unpacks the required fields from toLinearMap and adds the remaining separate fields.
4. This is probably done to remain neutral between additive and multiplicative structure: under the hood a RingEquiv will have three fields: toEquiv, map_add' and map_mul'. If we wrote RingHom extends MulEquiv, AddEquiv then we get two asymmetrical fields: toMulEquiv and map_add'. It seems neater this way, although I don't have any technical reason that we need do this or something will break.
5. It does! To be technical, as long as your diamond inheritance is forgetful there will be no problems. When you use extends, Lean ensures this is the case. A diamond in the typeclass hierachy becomes a problem once you create data out of existing fields. The big example is scalar multiplication by a natural number: in any additive monoid A, we could define n • a := a + a + ... + a, n times. In any multiplicative monoid M, we could define a • b := a * b. So what if A = M = ℕ? Then we have to arrange these multiplications to coincide, which we do in Mathlib by not fixing the definition n • a = a + a + ... + a but instead adding this as an extra axiom.

[Notification Bot]

Edward van de Meent has marked this topic as resolved.

[Notification Bot]

Edward van de Meent has marked this topic as unresolved.

[Edward van de Meent]

is there somewhere i could find a list of definitions/theorems i should implement for bundled Homs/ Equivs (and their respective classes)? i'm thinking of things like .id, .rfl, .trans, etc?

[Edward van de Meent]

i am tempted to declare classes HomClass and EquivClass, because i think that is basically the pattern that we're implementing each time...
is it possibly the case that i want to use that objects and their Homs form a category?

[Edward van de Meent]

and something similar for Equiv types?

[Edward van de Meent]

(i tried declaring the classes and ran into universe errors which i have no experience with solving, which tipped me off to this being some kind of category theory concept)

[Johan Commelin]

Yup, those universe problems are known, and they can't really be solved.

[Johan Commelin]

One solution would be to have some meta-code that can generate all these id, rfl, trans, etc... declarations.

[Johan Commelin]

But that's a substantial project

[Edward van de Meent]

a nice start would be to have a list of declarations and proofs, to at least make the convention documented somewhere

[Edward van de Meent]

i made a start with extracting the general API...
i have created a generic structure MyHom which extends structures XHom and YHom, where YHom has the same parameters as MyHom, while XHom has one less.

definitions and lemmas for XHom and YHom

import Mathlib.Data.FunLike.Basic

variable (T:Type*) {a:Type*} {b:Type*}
def PX (foo:a → b) : Prop := sorry
structure XHom (a:Type*) (b:Type*) where
  toFun : a → b
  xProp : PX toFun

instance (a:Type*) (b:Type*): FunLike (XHom a b) a b := {
  coe := XHom.toFun
  coe_injective' := fun f g h => by
    cases f; cases g; congr
}

@[ext]
lemma XHom.ext ⦃f:XHom a b⦄ ⦃g:XHom a b⦄ (h:∀ x, f x = g x): f = g :=
  DFunLike.ext _ _ h
variable (a b)

class XHomClass [FunLike T a b] where
  xProp' : ∀ (f:T), PX f

instance XHom.instXHomClass: XHomClass (XHom a b) a b where
  xProp' := XHom.xProp

protected def XHom.copy {a} {b} (f : XHom a b) (f' : a → b) (h : f' = f) :
    XHom a b where
  toFun := f'
  xProp := h.symm ▸ f.xProp

@[simp]
theorem XHom.coe_copy (f : XHom a b) (f' : a → b) (h : f' = f) :
    (f.copy f' h) = f' := rfl


@[simps]
def XHom.id (a:Type*) : XHom a a where
  toFun x := x
  xProp := sorry


def XHom.comp {a} {b} {c:Type*} (hnp : XHom b c) (hmn : XHom a b) : XHom a c where
  toFun := hnp ∘ hmn
  xProp := sorry

@[simp]
theorem XHom.coe_comp {a} {b} {c:Type*} (g : XHom b c) (f : XHom a b) :
    ↑(g.comp f) = g ∘ f := rfl

theorem XHom.comp_apply {a} {b} {c:Type*} (g : XHom b c) (f : XHom a b) (x : a) :
    g.comp f x = g (f x) := rfl


theorem XHom.comp_assoc {a} {b} {c:Type*} {d : Type*}
    (f : XHom a b) (g : XHom b c) (h : XHom c d) :
    (h.comp g).comp f = h.comp (g.comp f) := rfl

theorem XHom.cancel_right {a} {b} {c:Type*} {g₁ g₂ : XHom b c} {f : XHom a b}
    (hf : Function.Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => XHom.ext <| hf.forall.2 (DFunLike.ext_iff.1 h), fun h => h ▸ rfl⟩

theorem XHom.cancel_left {a} {b} {c:Type*} {g : XHom b c} {f₁ f₂ : XHom a b}
    (hg : Function.Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => XHom.ext fun x => hg <| by rw [← XHom.comp_apply, h, XHom.comp_apply],
    fun h => h ▸ rfl⟩

@[simp]
theorem XHom.comp_id (f : XHom a b) : f.comp (XHom.id a) = f :=
  XHom.ext fun _ => rfl

@[simp]
theorem XHom.id_comp (f : XHom a b) : (XHom.id b).comp f = f :=
  XHom.ext fun _ => rfl

variable {a} {s:a→ Prop} {b}

section

def PY (foo:a → b) (s:a → Prop) : Prop := sorry-- some statement about foo and s
end

structure YHom (s:a→Prop) (b) where
  toFun : a → b
  yProp : PY toFun s -- a proof that P holds for toFun and s


class YHomClass (T) (s) (b) [FunLike T a b] where
  yProp' : ∀ f:T, PY f s

instance (s:a → Prop) (b): FunLike (YHom s b) a b := {
  coe := YHom.toFun
  coe_injective' := fun f g h => by
    cases f; cases g; congr
}

@[ext]
lemma YHom.ext ⦃f:YHom s b⦄ ⦃g:YHom s b⦄ (h:∀ x, f x = g x): f = g :=
  DFunLike.ext _ _ h

instance YHom.instYHomClass (s:a→ Prop) (b) : YHomClass (YHom s b) s b where
  yProp' := yProp


section
protected def YHom.copy (f : YHom s b) (f' : a → b) (h : f' = f) :
    YHom s b where
  toFun := f'
  yProp := h.symm ▸ f.yProp

@[simp]
theorem YHom.coe_copy (f : YHom s b) (f' : a → b) (h : f' = f) :
    (f.copy f' h) = f' := rfl

@[simps]
def YHom.id (s:a → Prop) : YHom s a where
  toFun x := x
  yProp := sorry


def YHom.comp {s₂:b → Prop} {c:Type*} (hnp : YHom s₂ c) (hmn : YHom s b) : YHom s c where
  toFun := hnp ∘ hmn
  yProp := sorry

@[simp]
theorem YHom.coe_comp {s₂:b → Prop} {c:Type*} (g : YHom s₂ c) (f : YHom s b) :
    ↑(g.comp f) = g ∘ f := rfl

theorem YHom.comp_apply {s₂:b → Prop} {c:Type*} (g : YHom s₂ c) (f : YHom s b) (x : a) :
    g.comp f x = g (f x) := rfl

theorem YHom.comp_assoc {s₂:b → Prop} {c:Type*} {s₃: c → Prop} {d : Type*}
    (f : YHom s b) (g : YHom s₂ c) (h : YHom s₃ d) :
    (h.comp g).comp f = h.comp (g.comp f) := rfl

theorem YHom.cancel_right {s₂:b → Prop} {c:Type*} {g₁ g₂ : YHom s₂ c} {f : YHom s b}
    (hf : Function.Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => YHom.ext <| hf.forall.2 (DFunLike.ext_iff.1 h), fun h => h ▸ rfl⟩

theorem YHom.cancel_left {s₂:b → Prop} {c:Type*} {g : YHom s₂ c} {f₁ f₂ : YHom s b}
    (hg : Function.Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => YHom.ext fun x => hg <| by rw [← YHom.comp_apply, h, YHom.comp_apply],
    fun h => h ▸ rfl⟩

@[simp]
theorem YHom.comp_id (f : YHom s b) : f.comp (YHom.id s) = f :=
  YHom.ext fun _ => rfl

@[simp]
theorem YHom.id_comp {s₂:b → Prop} (f : YHom s b) : (YHom.id s₂).comp f = f :=
  YHom.ext fun _ => rfl

definitions and lemmas for MyHom

import [the file with definitions of `XHom` and `YHom`]

variable {T:Type*} {a:Type*} {s:a→ Prop} {b:Type*}

def MyProp (foo:a → b) (s:a→ Prop): Prop := sorry

variable (s b)

structure MyHom extends XHom a b, YHom s b where
  myProp : MyProp toFun s

-- DFunLike where applicable/necessary
instance MyHom.instFunLike : FunLike (MyHom s b) a b where
    coe := fun f => f.toYHom
    coe_injective' := fun f g h => by -- this proof is typically a tad annoying to do
      sorry

variable {s b}

-- weird brackets to later allow for magicks at cancel_right
@[ext]
lemma MyHom.ext ⦃f:MyHom s b⦄ ⦃g:MyHom s b⦄ (h:∀ x, f x = g x): f = g :=
  DFunLike.ext _ _ h

-- take [XHomClass T a b] as a parameter.
-- this is because when lean tries to infer [XHomClass T a b],
-- it will try to look for [MyHomClass T s b] and not know what s to use.
-- [YHomClass T s b] is ok tho
class MyHomClass
    (T:Type*) {a:Type*} (s:Set a) (b:Type*) [FunLike T a b] [XHomClass T a b]
    extends YHomClass T s b where
  myProp' : ∀ (f:T), MyProp f s

-- declare instances for classes when it is a parameter to MyHomClass
instance MyHom.instXHomClass {a:Type*} (s:Set a) (b:Type*) : XHomClass (MyHom s b) a b where
  xProp' := fun f => f.xProp

-- in declaring this, you also declare immediately `YHomClass s b`
instance MyHom.instMyHomClass {a:Type*} (s:Set a) (b:Type*) : MyHomClass (MyHom s b) s b where
  yProp' := fun f => f.yProp
  myProp' := fun f => f.myProp

variable--? [MyHomClass T s b] =>
  [FunLike T a b] [XHomClass T a b]

@[coe]
def MyHomClass.toMyHom [MyHomClass T s b] (f:T) : MyHom s b where
  toFun := f
  xProp := XHomClass.xProp' f
  yProp := YHomClass.yProp' f
  myProp := MyHomClass.myProp' f

instance [MyHomClass T s b] : CoeTC T (MyHom s b) :=
  ⟨MyHomClass.toMyHom⟩

@[simp]
theorem MyHom.coe_coe [MyHomClass T s b] (f : T) : ((f : MyHom s b) : a → b) = f := rfl

@[simp]
theorem MyHom.coe_mk
  (f : XHom a b) (yProp: PY f s) (myProp :MyProp f s): (MyHom.mk f yProp myProp : a → b) = f := rfl


protected def MyHom.copy (f : MyHom s b) (f' : a → b) (h : f' = f) :
    MyHom s b where
  toFun := f'
  xProp := h.symm ▸ f.xProp
  yProp := h.symm ▸ f.yProp
  myProp := h.symm ▸ f.myProp

@[simp]
theorem MyHom.coe_copy (f : MyHom s b) (f' : a → b) (h : f' = f) :
    (f.copy f' h) = f' := rfl

-- alternatively, if you want to focus only on added fields:
protected def MyHom.copy' (f: MyHom s b) (f' : a → b) (h : f' = f): MyHom s b := {
  f.toXHom.copy f' h, f.toYHom.copy f' h with
  myProp := by
    simp only
    rw [XHom.copy]
    exact h.symm ▸ f.myProp
  }

theorem MyHom.coe_copy_eq (f :MyHom s b) (f' : a → b) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

@[simps]
def MyHom.id (s:a→Prop) : MyHom s a := {
  XHom.id a, YHom.id s with
  myProp := by
    simp only
    rw [XHom.id]
    simp only
    sorry
}

variable {s₂:b → Prop} {c:Type*}
def MyHom.comp (hnp : MyHom s₂ c) (hmn : MyHom s b) : MyHom s c := {
  hnp.toXHom.comp hmn.toXHom, hnp.toYHom.comp hmn.toYHom with
  myProp := by
    simp only
    rw [XHom.comp]
    simp only
    sorry
}

@[simp]
theorem MyHom.coe_comp {s₂:b → Prop} {c:Type*} (g : MyHom s₂ c) (f : MyHom s b) :
    ↑(g.comp f) = g ∘ f := rfl

theorem MyHom.comp_apply {s₂:b → Prop} {c:Type*} (g : MyHom s₂ c) (f : MyHom s b) (x : a) :
    g.comp f x = g (f x) := rfl

theorem MyHom.comp_assoc {s₂:b → Prop} {c:Type*} {s₃: c → Prop} {d : Type*}
    (f : MyHom s b) (g : MyHom s₂ c) (h : MyHom s₃ d) :
    (h.comp g).comp f = h.comp (g.comp f) := rfl

theorem MyHom.cancel_right {s₂:b → Prop} {c:Type*} {g₁ g₂ : MyHom s₂ c} {f : MyHom s b}
    (hf : Function.Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => MyHom.ext <| hf.forall.2 (DFunLike.ext_iff.1 h), fun h => h ▸ rfl⟩


theorem MyHom.cancel_left {s₂:b → Prop} {c:Type*} {g : MyHom s₂ c} {f₁ f₂ : MyHom s b}
    (hg : Function.Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => MyHom.ext fun x => hg <| by rw [← MyHom.comp_apply, h, MyHom.comp_apply],
    fun h => h ▸ rfl⟩

@[simp]
theorem MyHom.comp_id (f : MyHom s b) : f.comp (MyHom.id s) = f :=
  MyHom.ext fun _ => rfl

@[simp]
theorem MyHom.id_comp {s₂:b → Prop} (f : MyHom s b) : (MyHom.id s₂).comp f = f :=
  MyHom.ext fun _ => rfl

[Edward van de Meent]

there is also MyHomClass in there.
if anyone is missing some lemmas/definitions, please say so

[Edward van de Meent]

i ported all of these from Mathlib.Algebra.Group.Hom .Defs, if anyone wants to know

[Edward van de Meent]

i'll see if i can expand this to also include Equiv versions and the like

[Edward van de Meent]

some of these lemmas are proven using the fact that MyHom only adds Prop-valued fields. other than that, there are still some other lemmas using sorry.
those are:

• MyHom.id, where you need to provide values for all extra fields of MyHom compared to its parents, such as proofs that id has the properties that MyHom describes
• MyHom.comp, where you need to provide those values too, such as proofs that composition preserves the properties that MyHom describes

[Edward van de Meent]

if you are adding other non-prop fields, however, that will make it all a tad bit more complicated... for instance, the proof of cancel_left depends on the FunLike.coe_injective' field, while comp_assoc is currently proven rfl

[Edward van de Meent]

although honestly i have yet to think of an example where that is relevant

[Edward van de Meent]

I'm implementing my own Isometry structure, and i ran into the following:
The docs in Mathlib.Data.FunLike.Equiv say i should implement .copy for my Equiv as follows:

protected def copy (f : MyIso A B) (f' : A → B) (f_inv : B → A) (h : f' = ⇑f) : MyIso A B :=
  { toFun := f',
    invFun := f_inv,
    left_inv := h.symm ▸ f.left_inv,
    right_inv := h.symm ▸ f.right_inv,
    map_op' := h.symm ▸ f.map_op' }

However, the example provided doesn't work, as you also need f_inv = f.invFun, or leave f.invFun the same between the instances...
I looked for examples in mathlib where this pattern is implemented, but a quick search didn't result in anything much.
Could someone tell me if this pattern is actually wanted, and if so, where i can find a working example of this API for any isometry-like structure?

[Jireh Loreaux]

You don't need them to be equal because they are provably equal.

[Edward van de Meent]

are they? f_inv is a generic function B -> A though?

[Edward van de Meent]

completely independent from f'

[Jireh Loreaux]

oh, sorry, you haven't proved copy, I misunderstood. Yes, you need that hypothesis in order to prove left_inv and right_inv.

[Jireh Loreaux]

And you should definitely allow the user to replace the invFun too, because the whole purpose is for providing better definitional properties.

[Edward van de Meent]

ok... is there some implementation in mathlib i could look at for inspiration?

[Jireh Loreaux]

A PR updating the text in Mathlib.Data.FunLike.Equiv would be appreciated.

[Jireh Loreaux]

Without the morphism properties, it just looks like this:

variable {α β : Type*}

def Equiv.copy (e : α ≃ β) (f : α → β) (f_inv : β → α) (hf : f = ↑e) (hf_inv : f_inv = ⇑e.symm) :
    α ≃ β where
  toFun := f
  invFun := f_inv
  left_inv := hf_inv.symm ▸ hf.symm ▸ e.left_inv
  right_inv := hf_inv.symm ▸ hf.symm ▸ e.right_inv

[Jireh Loreaux]

Does that answer your question? I'm not sure we have very many (any?) of these .copy defs for EquivLike types.

[Jireh Loreaux]

(Although it would be convenient if we did)

[Edward van de Meent]

yes, thanks! indeed, i haven't found any EquivLike types implementing this.

[Edward van de Meent]

it turns out it is a tad trickier when extending other copy lemmas, as apparently lean is unable to rewrite with hf and hf_inv at the inverse lemmas of e. what does consistently work, however, is this:

variable {α β : Type*}

def Equiv.copy (e : α ≃ β) (f : α → β) (f_inv : β → α) (hf : f = ↑e) (hf_inv : f_inv = ⇑e.symm) :
    α ≃ β where
  toFun := f
  invFun := f_inv
  left_inv := by
    simp_rw [hf_inv,hf]
    exact f.left_inv
  right_inv := by
    simp_rw [hf_inv,hf]
    exact f.right_inv

[Edward van de Meent]

i also ran into some trouble with the suggested way to define MyIsoClass..
defining MyIso.instMyIsoClass as suggested (see section A in MWE) gives an error. my current solution to this is section B, although i do think that's hacky and somewhat ugly...
#mwe :

import Mathlib.Data.FunLike.Equiv
import Mathlib.Logic.Equiv.Defs

variable {α β :Type*}
structure MyHom (α β :Type*) where
  toFun : α → β

class MyHomClass (T:Type*) (α β: outParam Type*) [FunLike T α β]
namespace MyHom
instance instFunLike : FunLike (MyHom α β) α β where
  coe := MyHom.toFun
  coe_injective' := fun f g h => by cases f; cases g; congr

instance instMyHomClass : MyHomClass (MyHom α β) α β where
end MyHom
structure MyEquiv (α β:Type*) extends α ≃ β, MyHom α β where

class MyEquivClass (T:Type*) (α β: outParam Type*) extends EquivLike T α β, MyHomClass T α β

namespace MyEquiv

section A
-- /-
instance instMyEquivClass : MyEquivClass (MyEquiv α β) α β := {-- failed to synthesize instance FunLike (MyEquiv α β) α β
  coe := fun f => f.toFun
  inv := fun f => f.invFun
  left_inv := fun f => f.left_inv
  right_inv := fun f => f.right_inv
  coe_injective' := fun f g h => by cases f; cases g; congr; simp_all
}
-- -/
end A

section B
/-
def instEquivLike : EquivLike (MyEquiv α β) α β := {
  coe := fun f => f.toFun
  inv := fun f => f.invFun
  left_inv := fun f => f.left_inv
  right_inv := fun f => f.right_inv
  coe_injective' := fun f g h => by cases f; cases g; congr; simp_all
}

def instMyHomClass :
  @MyHomClass (MyEquiv α β) α β (@EquivLike.toFunLike
      (MyEquiv α β) α β MyEquiv.instEquivLike) :=
  (@MyHomClass.mk (MyEquiv α β) α β (@EquivLike.toFunLike
    (MyEquiv α β) α β MyEquiv.instEquivLike))


instance instMyEquivClass : MyEquivClass (MyEquiv α β) α β :=
  @MyEquivClass.mk (MyEquiv α β) α β MyEquiv.instEquivLike MyEquiv.instMyHomClass
-/
end B
end MyEquiv

[Edward van de Meent]

basically, my current solution is using MyIsoClass.mk with explicit arguments.

[Edward van de Meent]

i honestly expected lean to be able to handle version A, but apparently not...

[Edward van de Meent]

i found a shorter solution, but i'm still not really happy...

instance instMyEquivClass : MyEquivClass (MyEquiv α β) α β := {({
  coe := fun f => f.toFun
  inv := fun f => f.invFun
  left_inv := fun f => f.left_inv
  right_inv := fun f => f.right_inv
  coe_injective' := fun f g h => by cases f; cases g; congr; simp_all} : EquivLike (MyEquiv α β) α β) with
}