Bundled morphisms

Stream: mathlib4

[Yury G. Kudryashov]

I have an idea about how bundled morphisms can be done in Lean 4 (after we port mathlib3).

-- Auxiliary classes
class ComposablePred (A B C) (p : (B → C) → Prop) (q : (A → B) → Prop) (r : outParam ((A → C) → Prop)) : Prop where
  comp : ∀ f g, p f → q g → r (f ∘ g)

class WeakerPred (A B) (p q : (A → B) → Prop) : Prop where
  weaker : ∀ f, p f → q f

class IdPred (A) (p : (A → A) → Prop) : Prop where
  id : p id

class InvertiblePred (A B) (p : (A → B) → Prop) (q : outParam ((B → A) → Prop)) : Prop where
  symm : ∀ f g, p f → LeftInverse g f → RightInverse g f → q g

-- hom-specific data
structure IsMulHom [Mul A] [Mul B] (f : A → B) : Prop where
  map_mul : ∀ a b, f (a * b) = f a * f b

instance {A B C} [Mul A] [Mul B] [Mul C] : ComposablePred A B C IsMulHom IsMulHom IsMulHom := sorry
instance {A} [Mul A] : IdPred A IsMulHom

-- generic constructions
structure BundledHom (A B : Type*) (p : (A → B) → Prop) where
  toFun : A → B
  property : p toFun

attribute [coe] BundledHom.toFun

instance : CoeFun (BundledHom A B p) fun _ => A → B := ⟨BundledHom.toFun⟩

structure BundledEmbedding (A B : Type*) (p : (A → B) → Prop) extends BundledHom A B p where
  injective : Injective toFun

instance : CoeFun (BundledEmbedding A B p) fun _ => A → B := ⟨fun f => f.toBundledHom⟩

structure BundledEquiv (A B : Type*) (p : (A → B) → Prop) extends BundledHom A B p where
  invFun : B → A
  left_inv : LeftInverse invFun toFun
  right_inv : RightInverse invFun toFun

def BundledEquiv.toBundledEmbedding := sorry

instance : CoeFun (BundledEquiv A B p) fun _ => A → B := ⟨fun f => f.toBundledEmbedding⟩

def BundledEquiv.symm {A B : Type*} {p : (A → B) → Prop} {q : outParam ((B → A) → Prop)} [InvertiblePred A B p q]
    (e : BundledEquiv A B p) : BundledEquiv B A q := sorry

-- auxiliary abbreviations
abbrev MulHom A B [Mul A] [Mul B] := BundledHom A B IsMulHom
abbrev MulEquiv A B [Mul A] [Mul B] := BundledEquiv A B IsMulHom

lemma map_mul {p : (A → B) → Prop} [WeakerPred A B p IsMulHom] (f : BundledHom A B p) (a b : A) :
    f (a * b) = f a * f b := sorry

Then main "pro" of this approach is that we can use a generic construction to define, e.g., *.comp, *.id, and *.End with pow = iterate. Also, map_mul can be stated for a BundledHom because coercions of BundledEmbeddings and BundledEquivs are unfolded to BundledHoms (with two and three arrows, resp.).

There are a few things I don't know how to do with this approach yet:

• auto upgrade from MulEquiv to MonoidHom; maybe,

class HasProp {p : (A → B) → Prop} (f : BundledHom A B p) (q : (A → B) → Prop) : Prop where
  prop : q f

instead of WeakerPred?

• FunLikes that have other data fields (e.g., Finsupp).
• define a MulHom with nice where syntax instead of

def f : MulHom A B where
  toFun := f
  property := { map_mul := _ }

What do you think? @Anne Baanen you wrote the current *HomClass approach, so probably you have some insight here.

[Yury G. Kudryashov]

One more issue with this approach is that we have to either handle Function.Embedding/Equiv separately, or have an extra property : True := trivial field.

[Eric Wieser]

Equiv would need to be handled separately anyway since it carries data in the inv_fun, right?

[Yury G. Kudryashov]

In the code above, I define a generic BundledEquiv structure.

[Yury G. Kudryashov]

We can have Equiv α β := BundledEquiv α β fun _ => True and Function.Embedding α β := BundedEmbedding α β fun _ => True.

[Yury G. Kudryashov]

Created !4#2202