Redesign bundled morphisms and sets

[urkud]

Draft proposal, see also Zulip

-- 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 := _ }

A similar redesign can be done with SetLike. Then we can have CanMap/CanComap classes (in Prop) that say something like p s → p (f '' s) with p in different universes.

[Vierkantor]

From another Zulip thread:

I'm somewhat wary of the (p : (A → B) → Prop) predicates as parameters to the classes. These can have quite nontrivial equalities and equivalences that typeclasses cannot see through, or see through only very slowly. For example: if someone writes a monoid hom when an additive hom is expected, will Lean end up trying to unify * with +? This tends to get expensive quite quickly. Quite probably, we're okay as long as we stick to predicates of the form structure IsMonoidHom extends IsMulHom, IsOneHom (rather than IsMonoidHom := IsMulHom ∧ IsOneHom; we'd also avoid issues that would arise if someone writes the predicate as IsOneHom ∧ IsMulHom).

[Vierkantor]

I tried rewriting Algebra.Hom.Group, replacing the bundled hom structures with abbrevs for BundledHom.

It was quite tedious to replace the nice where syntax with property := { map_mul := sorry, map_one := sorry }. Is there a way to define a "custom constructor" for an abbrev type, of the form MonoidHom.mk : ∀ (f : A → B) (map_one : f 1 = 1) (map_mul : ∀ x y, f (x * y) = f x * f y), BundledHom A B IsMonoidHom?

I kept the HomClasses around, which saved a lot of refactoring. Of course that meant that there wasn't much improvement in actual ease of use over the existing situation.

Some notes:

• Defining ComposablePred instances for conjunctions of predicates (like IsMonoidHom from IsMulHom and IsOneHom) gets tedious very quickly. Can we automate this somehow?
• I struggled in Lean 3 with choosing which params to make outParam in my attempts at ComposablePred and InvertiblePred, it seems even in basic files each parameter has to be inferred. In Lean 4 metavariables are allowed in instance search goals, so we could choose to use no outParams at all (as long as we keep the search space small enough).
• Should we allow composition of a MulHom with a MonoidHom by adding an instance for ComposablePred p q r from ComposablePred p' q' r that takes in WeakerPred p p' and WeakerPred q q'? (Or maybe weaken p and q separately?)

[urkud]

It was quite tedious to replace the nice where syntax with property := { map_mul := sorry, map_one := sorry }. Is there a way to define a "custom constructor" for an abbrev type, of the form MonoidHom.mk : ∀ (f : A → B) (map_one : f 1 = 1) (map_mul : ∀ x y, f (x * y) = f x * f y), BundledHom A B IsMonoidHom?

If we want to do this, then we'll need an extended syntax. E.g., an ability to write something like

structure BundledHom α β (p : (α → β) → Prop) where
  toFun : α → β
  structure prop : p toFun -- or some other marker

structure IsMulHom [Mul α] [Mul β] (f : α → β) : Prop where
  map_mul : ∀ x y, f (x * y) = f x * f y

def f [Mul α] : BundledHom α α IsMulHom where
  toFun := id
  map_mul x y := rfl

* Defining `ComposablePred` instances for conjunctions of predicates (like `IsMonoidHom` from `IsMulHom` and `IsOneHom`) gets tedious very quickly. Can we automate this somehow?

We can put mk_iff on IsMonoidHom, then rw [isMonoidHom_iff]; infer_instance with an otherwise unused instance for And.

* I struggled in Lean 3 with choosing which params to make `outParam` in my attempts at `ComposablePred`

I thought that [ComposablePred p q r] should have r as an outParam, the same way we deal with ring_hom_triple. But I never did an experiment.

* Should we allow composition of a `MulHom` with a `MonoidHom` by adding an instance for `ComposablePred p q r` from `ComposablePred p' q' r` that takes in `WeakerPred p p'` and `WeakerPred q q'`? (Or maybe weaken `p` and `q` separately?)

IMHO, we should require explicit coercions, otherwise we'll have a huge search space (e.g., how Lean should decide which predicate to use for a composition of a ring homomorphism and a linear map?).