Trans vs Comp naming

Stream: mathlib4

[Eric Paul]

Sometimes things are called trans and sometimes comp. What's the distinction?

Trans:

/-- Composition of two relation embeddings is a relation embedding. -/
protected def trans (f : r ↪r s) (g : s ↪r t) : r ↪r t :=
  ⟨f.1.trans g.1, by simp [f.map_rel_iff, g.map_rel_iff]⟩

Comp:

/-- Composition of two relation homomorphisms is a relation homomorphism. -/
@[simps]
protected def comp (g : s →r t) (f : r →r s) : r →r t :=
  ⟨fun x => g (f x), fun h => g.2 (f.2 h)⟩

[Eric Paul]

I'm also confused about what simp tags are being used when and why.

For example we have that definition of trans with no simp tags

protected def trans (f : r ↪r s) (g : s ↪r t) : r ↪r t :=
  ⟨f.1.trans g.1, by simp [f.map_rel_iff, g.map_rel_iff]⟩

And then we have a similar trans with many simp things going on

/-- Composition of `f : α ↪ β` and `g : β ↪ γ`. -/
@[trans, simps (config := { simpRhs := true })]
protected def trans {α β γ} (f : α ↪ β) (g : β ↪ γ) : α ↪ γ :=
  ⟨g ∘ f, g.injective.comp f.injective⟩

I would have guessed that these two would have the same simp tags.

[Yaël Dillies]

Embeddings should use comp, not trans. Only equivalences/isomorphisms use trans.

[Eric Paul]

I see. So both of those trans should have their names changed to comp?

[Antoine Chambert-Loir]

Which is slightly bizarre since ordering relations use trans (and correspond to categorical monomorphisms).

[Yaël Dillies]

It's not bizarre at all if you remember that le_trans : a ≤ b → b ≤ c → a ≤ c, while le_comp would rather be le_comp : b ≤ c → a ≤ b → a ≤ c

[Mitchell Lee]

It's not that bizarre in my opinion, and the reason isn't just the order of the arguments.

We think of the composition of isomorphisms as a transitivity property (and thus call it trans) because we commonly think of isomorphism as a relation (e.g. "the groups $G$ and $H$ are isomorphic"). It is much less common to think of embeddability as a relation, so we don't think of the composition of embeddings as a transitivity property, and we call it comp.

[Kevin Buzzard]

The number of times I've typed e.comp and got a failure is humiliatingly high.

[Antoine Chambert-Loir]

Allow me to rephrase. If trans is used for equiv only, that means the word is restricted to groupoids, while comp is used for categories which are not a priori groupoids. Both cases correspond to the idea of transitivity. But for ordering relations, it is the word trans that is used, while the corresponding category (arrows are increasing pairs) is not a groupoid.

[Antoine Chambert-Loir]

One thing I fail to do with equivalences is defining by transitivity, such as ‘e.trans _?‘ with some known e and the next to be guessed.

[Yaël Dillies]

Antoine Chambert-Loir said:

One thing I fail to do with equivalences is defining by transitivity, such as ‘e.trans _?‘ with some known e and the next to be guessed.

Do you mean e.trans ?_. This Just Works:tm:, right? What does this have to do with the current conversation?

[Jireh Loreaux]

It should work as long as the expected type is known.