too many `out`s

Stream: mathlib4

[Kevin Buzzard]

A nice unexpected error below:

import Mathlib.Algebra.Module.Projective
import Mathlib.RingTheory.Finiteness.Defs

variable (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M]

-- finite projective modules
class IsFiniteProjective extends Module.Projective R M, Module.Finite R M : Prop where -- oops

/-
parent field type mismatch, field 'out' from parent 'Module.Finite' has type
  ⊤.FG : Prop
but is expected to have type
  ∃ s, Function.LeftInverse ⇑(Finsupp.linearCombination R id) ⇑s : Prop
-/

The issue is that the axiom for finite modules and the axiom for projective modules are both called out so no class can extend both (this is not an artificial example: it just happened in #20489).

Looking through mathlib, an axiom for a ring/module/algebra is called out in

class Module.FinitePresentation : Prop where
  out : ∃ (s : Finset M), Submodule.span R (s : Set M) = ⊤ ∧
    (LinearMap.ker (Finsupp.linearCombination R ((↑) : s → M))).FG

class Algebra.IsCentral
    (K : Type u) [CommSemiring K] (D : Type v) [Semiring D] [Algebra K D] : Prop where
  out : Subalgebra.center K D ≤ ⊥

/-- A type-class version of `n ≠ 0`.  -/
class NeZero (n : R) : Prop where
  /-- The proposition that `n` is not zero. -/
  out : n ≠ 0

@[mk_iff] class Module.Injective : Prop where
  out : ∀ ⦃X Y : Type v⦄ [AddCommGroup X] [AddCommGroup Y] [Module R X] [Module R Y]
    (f : X →ₗ[R] Y) (_ : Function.Injective f) (g : X →ₗ[R] Q),
    ∃ h : Y →ₗ[R] Q, ∀ x, h (f x) = g x

class Module.Projective (R : Type*) [Semiring R] (P : Type*) [AddCommMonoid P] [Module R P] :
    Prop where
  out : ∃ s : P →ₗ[R] P →₀ R, Function.LeftInverse (Finsupp.linearCombination R id) s

protected class Module.Finite [Semiring R] [AddCommMonoid M] [Module R M] : Prop where
  out : (⊤ : Submodule R M).FG

and there are similar notation clashes in various category theory declarations which I won't list here. Unlike toFun, which always means the same thing, out seems to mean several things in mathlib. Are we OK with this or should we come up with some more helpful naming convention, like e.g.

protected class Module.Finite [Semiring R] [AddCommMonoid M] [Module R M] : Prop where
  finite : (⊤ : Submodule R M).FG

class Module.Projective (R : Type*) [Semiring R] (P : Type*) [AddCommMonoid P] [Module R P] :
    Prop where
  projective : ∃ s : P →ₗ[R] P →₀ R, Function.LeftInverse (Finsupp.linearCombination R id) s

etc?

[Ruben Van de Velde]

More descriptive names seems like the way to go

[Johan Commelin]

... seems like the way out

[Kevin Buzzard]

#20506

[Edward van de Meent]

I'd just like to mention that it is not for a lack of usecases that toFun has no clashes; for Free Probability Theory, really id like a structure extending Algebra R A, LinearMap R A R and OneHom A R, but since Algebra bundles it's algebraMap via extends RingHom R A, that causes a similar clash

[Edward van de Meent]

i.e. there are no toFun clashes because we haven't gotten to those usecases yet.

[Edward van de Meent]

(if this is something that people think should be possible, maybe adding the algebramap as an explicit field rather than via extends is an acceptable fix?)

[Johan Commelin]

I think that makes sense. Algebra is certainly a bit different from the other ones.

[Edward van de Meent]

#20518

[Eric Wieser]

Can you elaborate on why you would want to extend both Algebra and LinearMap?

[Eric Wieser]

Are you writing a class or a structure? If the latter, it seems rather strange to extend a class; if the former, it sounds like the same complaint could be levelled at your class for extending LinearMap as to algebra

[Edward van de Meent]

I am working on free probability theory, and one of the first definitions is that of a (free) probability space, which is a unital algebra with a unital linear map to its ring

[Edward van de Meent]

I think I'd like it to be a class, but I'm not entirely sure yet. I'm still working out the details.

[Edward van de Meent]

You are right that extending in my case doesn't make sense for the same reason. I only mentioned my case to demonstrate that there is a context where one would want to add multiple Homs to a structure or class, and therefore one can't/shouldn't use the extends pattern for one/all of them, respectively.