Where to put notation for orthogonality

Stream: mathlib4

[Brendan Seamas Murphy]

I decided to try and add some stuff about factorization systems, and for these I want to be able to write i ⟂ p to mean that either (1) lifting problems framed by i and p have solutions, i.e. HasLiftingProperty i p, or that (2) lifting problems framed by i and p have unique solutions. So (1) is used in the notion of a weak factorization system and (2) in an orthogonal factorization system. I have seen people frequently write ⟂ for the "weak orthogonality" notion of (1), and beyond these two there are also more notions of orthogonality in use in category theory (eg orthogonality of objects in a triangulated category). Also for (1) and (2) we inevitably want to talk about single morphisms which are orthogonal to a class of morphisms, so not only are orthogonality relations common but heterogeneous ones (heterogeneous in the sense of HAdd vs Add); heterogeneity is appealing to me also because it gives a nice way of talking about lifting problems that happen across an adjunction, or more generally across a profunctor. As far as I can tell, the only place orthogonality comes up in mathlib at the moment is in vector spaces. I would like to create a notation and typeclass for an orthogonality relation (and a heterogeneous orthogonality one). Where should I put this?

[Brendan Seamas Murphy]

I ask because I'm not really familiar with the typeclass/notation hierarchy of mathlib and it seems intricate but robust(?)

[Brendan Seamas Murphy]

Also, it occurs to me that when we consider an orthogonality relation on first order things (vectors, morphisms, objects) we immediately start wanting to consider an orthogonality relation on second order things (submodules, classes of morphisms, classes of objects). And on these we want to consider the left and right orthogonal complements Xᗮ and ᗮX of second order things, which form a galois connection. I'm not sure how to fit this into a typeclass framework but I would appreciate suggestions

[Eric Wieser]

Just noting we already have docs#Submodule.IsOrtho

[Brendan Seamas Murphy]

Yeah, if there were no existing instances of the notion of orthgonality I wouldn't sweat structuring the code as much

[Brendan Seamas Murphy]

(deleted)

[Eric Wieser]

Edited above

[Joël Riou]

In my draft implementation of model categories (Lean3), I defined a predicate morphism_property.has_lifting_property taking two morphism_properties as inputs. Given a class of morphisms G (i.e. morphism_property), I defined two others morphism_property G.llp_with and G.rlp_with in order to denote those morphisms which have the left (resp. right) lifting property with respect to G. Then, to say that a morphism is "(weak) left orthogonal to G" means that it belongs to G.llp_with. Then, I am not so sure we need to introduce a heterogeneous notation in this situation.
(See https://github.com/joelriou/homotopical_algebra/blob/main/src/for_mathlib/category_theory/lifting_properties/morphism_property.lean )

[Brendan Seamas Murphy]

I'll take a look at that draft. I understand that it's possible to work only with the homogenous version of the relation, but the heterogenous one feels closer to the natural language use of the terms "orthogonal" and "has the _ lifting property". Also, I have been interested in thinking about heterogenous lifting properties across profunctors recently (in non-lean math) and so I'm inclined to set up the notation in a way that would allow me to talk about these

[Reid Barton]

I had a similar setup.
https://github.com/rwbarton/lean-model-categories/blob/top-dev/src/category_theory/model/wfs.lean
If mathlib had a notation like f \in C for simply C f, then it would be pretty natural to write e.g. f \in llp S.

[Brendan Seamas Murphy]

I'm going to tentatively put it in Mathlib.Init.Algebra.Classes, I guess?

[Eric Wieser]

I think that's a bad place, most of Init is vestigial stuff from Lean3 core

[Brendan Seamas Murphy]

Where else would you suggest?

[Brendan Seamas Murphy]

also to be clear, where to put it is orthogonal (heh) to whether it should have both a heterogeneous and homogeneous version or just a homogeneous version

[Brendan Seamas Murphy]

Maybe I could put it with galois connection stuff, since orthogonality relations usually induce a galois connection?

[Brendan Seamas Murphy]

Also, just looking at other places where there's notation in mathlib, the HImp class that gives notation for heyting algebra implication clashes with the naming convention of HAdd, HSub, HEq, etc

[Brendan Seamas Murphy]

H for Heyting vs H for heterogeneous

[Eric Wieser]

I wouldn't bother with the heterogenous version

[Yaël Dillies]

Heterogeneous operators have proven pretty useless so far, except for making our life harder with weaker unification. I think we should scrap them back.

[Eric Wieser]

They were useful for Matrix, but not overwhelmingly so.

[Eric Wieser]

Either way, I think the takeaway is that heterogeneous operations came from Lean core not mathlib, and mathlib doesn't really make use of them, or necessarily ever intend to.

[Yury G. Kudryashov]

Should we drop HSMul then?

[Kyle Miller]

Just so you know, in kmill_lean_fixes_2778 I'm putting HSMul onto the same type coercion algorithm as the rest of the operators, once lean4#2778 is merged after a bit more work. This makes it so that in a • b the expected type influences the type of b, and also that the type of b influences the type of the entire algebraic expression.