naming challenge

Stream: general

[Floris van Doorn]

How should I (re)name this concept?

/--
An element `a : α` is `regular` (name subject to change) if `x ↦ a + x` is order-reflecting.
We will make a separate version of lemmas that require `[contravariant_class α α (+) (≤)]` with
`regular` assumptions instead. These can then be easily instantiated to specific types, like
`ennreal`, where we can replace the assumption `regular x` by `x ≠ ∞`.
-/
def regular {α} [has_le α] [has_add α] (a : α) : Prop :=
∀ ⦃x y⦄, a + x ≤ a + y → x ≤ y

[Kalle Kytölä]

How about cancellable? Or add_le_cancellable (if the relation is ≤ and operation is +)? Or rel_cancellable (if the same name is to be used for many relations)?

I am not very familiar yet with the naming conventions, but I thought having various suggestions to consider can hardly hurt :grinning_face_with_smiling_eyes:.

[Kalle Kytölä]

The term "regular" would of course be following a time-honored tradition in math naming conventions for just about anything... By which I mean: I hope mathlib will not adopt it in this case! :smile:

[Floris van Doorn]

I think I'll go for add_le_cancellable. Thanks for the suggestions.

[Floris van Doorn]

@Eric Wieser pointed out in #8503 that lean actually already has a notion of docs#is_left_regular (added by @Damiano Testa). Interestingly, that definition doesn't have@[to_additive]. We could try to make these definitions more closely connected, for example by calling the both is_[left|right]_[mul|add]_[le_]_cancellable or both is_[left|right]_[mul|add]_[le_]_regular

[Damiano Testa]

(deleted)

[Damiano Testa]

I like the idea of connecting the two notions: it is a common trick to prove injectivity by showing strict monotonicity!

As for the name, I chose regular because I was thinking of using this for regular elements and regular sequences in commutative algebra. For this same reason, it had not occurred to me to do the same for additive. Also, at the time of the PR I was less "Lean-mature" and was not aware of the to_additive attribute.

In fact, following up on a comment by Eric, it seems to make sense to define co(ntra)variant as ∀ (m), analogue_of_mul_le_cancellable_with_explicit_m_input.

[Anne Baanen]

Anyone have a nice idea how to give these two definitions distinct, but not too long, names in #8514?

/-- Given `P 0`, `P 1`, and `P (p ^ k)` for positive prime powers, and a way to extend `P a` and
`P b` to `P (a * b)` when `a, b` are coprime, you can define `P` for all natural numbers. -/
@[elab_as_eliminator]
def rec_on_coprime' {P : ℕ → Sort*} (hp : ∀ p n : ℕ, prime p → 0 < n → P (p ^ n))
  (h0 : P 0) (h1 : P 1) (h : ∀ a b, coprime a b → P a → P b → P (a * b)) : ∀ a, P a :=
rec_on_prime_pow h0 h1 $ λ a p n hp' hpa ha,
  h (p ^ n) a ((prime.coprime_pow_of_not_dvd hp' hpa).symm)
  (if h : n = 0 then eq.rec h1 h.symm else hp p n hp' $ nat.pos_of_ne_zero h) ha

/-- Given `P 0`, `P (p ^ k)` for all prime powers, and a way to extend `P a` and `P b` to
`P (a * b)` when `a, b` are coprime, you can define `P` for all natural numbers. -/
@[elab_as_eliminator]
def rec_on_coprime {P : ℕ → Sort*} (h0 : P 0) (hp : ∀ p n : ℕ, prime p → P (p ^ n))
  (h : ∀ a b, coprime a b → P a → P b → P (a * b)) : ∀ a, P a :=
rec_on_coprime' (λ p n h _, hp p n h) h0 (hp 2 0 prime_two) h

[Eric Wieser]

Swapping the order of the arguments in the first one so that hp comes after h1 would make it easier to tell what the difference is!

[Eric Wieser]

rec_on_prime_coprime and rec_on_pos_prime_coprime?

[Floris van Doorn]

Anyone have any ideas to name the following linear maps?

def name_me1 (L : E →L[𝕜] E' →L[𝕜] F) : E →L[𝕜] (E'' →L[𝕜] E') →L[𝕜] (E'' →L[𝕜] F) :=
(continuous_linear_map.compL 𝕜 E'' E' F).comp L

def name_me2 (L : E →L[𝕜] E' →L[𝕜] F) : (E'' →L[𝕜] E) →L[𝕜] E' →L[𝕜] (E'' →L[𝕜] F) :=
(precompR E'' (flip L)).flip

[Eric Wieser]

Can you include the simps lemma they generate too?

[Floris van Doorn]

(ᾰ : E) : ⇑(name_me1 E'' L) ᾰ = ⇑(compL 𝕜 E'' E' F) (⇑L ᾰ)
(ᾰ : E) (f : E'' →L[𝕜] E') : ⇑(⇑(name_me1 E'' L) ᾰ) f = (⇑L ᾰ).comp f
(ᾰ : E) (f : E'' →L[𝕜] E') (ᾰ_1 : E'') : ⇑(⇑(⇑(name_me1 E'' L) ᾰ) f) ᾰ_1 = ⇑(⇑L ᾰ) (⇑f ᾰ_1)

[Floris van Doorn]

I'm thinking of something like precompose_right / precompose_left, since we're precomposing the function E'' →L[𝕜] E' on the right/left argument.

[Moritz Doll]

Maybe compL₂ for the first one to be consistent with docs#linear_map.compl₂ ? your second map should correspond to docs#linear_map.compr₂

[Floris van Doorn]

Those are indeed very close, my maps have the second linear map bundled.
flip (name_me1 L) f is basically the same as linear_map.compl₂ L f (up to continuity and semilinearity).

[Moritz Doll]

I think it would be a good idea if the API of bilinear maps and continuous bilinear maps would be as close as possible, but I also think that the bundled definitions are better then linear_map.compl₂ L f (btw please change your linear map from L to B, it is really confusing with the L from the clm notation).

[Moritz Doll]

but there is already diverging notation with continuous_linear_map.compL and linear_map.lcomp.

[Moritz Doll]

(deleted)

[Eric Wieser]

Sometimes I wonder if we're shooting ourselves in the foot with this heavy point-free approach, and would do better to just write \lam a f x, L a (f x) and use some linearity tactic to find the linearity proof automatically.

[Patrick Massot]

Indeed all this doesn't exist on paper, and we certainly want to keep it that way on paper.

[Floris van Doorn]

This sounds like some abstract nonsense that does exist in cartesian closed categories (possibly with some extra structure).

[Eric Rodriguez]

/poll What statement would people expect for the name equiv.subtype_congr?
{α} {p q : α → Prop} (e : {x // p x} ≃ {x // q x}) (f : {x // ¬p x} ≃ {x // ¬q x}) : perm α
(e : α₁ ≃ α₂) (p : α₂ → Prop) : {a₁ // (p ∘ e) a₁} ≃ {a₂ // p a₂}

[Eric Rodriguez]

answer: docs#equiv.subtype_congr
bonus: what would you call the other? (I'm making the one of these that isn't in mathlib already and not sure what name to give it if not that)

[Eric Wieser]

docs#equiv.subtype_equiv is one of the other ones

[Eric Wieser]

I think the current equiv.subtype_congr should be called equiv.subtype_piecewise?

[Eric Rodriguez]

I was rewriting option 3 as I didn't think of it, d'ah!

[Eric Wieser]

Or maybe even just equiv.piecewise

[Eric Rodriguez]

oh, I think my proof is nicer so I'll PR that (no non-terminal simps :]) I currently don't have a good computer though, so I will refactor the names when I get to a good computer

[Gabriel Ebner]

Option 1 looks like a perm.subtype_piecewise to me. I would expect equiv.subtype_piecewise to be {α β} {p : α → Prop} {q : β → Prop} (e : { a // p a } ≃ { b // q b }) (f : { a // ¬ p a } ≃ { b // ¬ q b }) : α ≃ β.

[Eric Rodriguez]

oh, and option 2 is docs#equiv.subtype_equiv_of_subtype

[Eric Rodriguez]

#14125

[Eric Rodriguez]

Eric Rodriguez said:

oh, and option 2 is docs#equiv.subtype_equiv_of_subtype

what should this be called? I don't like this name but not sure what a better one would be

[Yaël Dillies]

I rarely see stuff in the equiv.subty namespace :stuck_out_tongue:

[Chris Hughes]

Eric Wieser said:

Sometimes I wonder if we're shooting ourselves in the foot with this heavy point-free approach, and would do better to just write \lam a f x, L a (f x) and use some linearity tactic to find the linearity proof automatically.

I worked on this a little bit recently. If you use every bound variable exactly once then the map will be linear. I have some very untidy code taking lambda terms and turning them into terms using linear composition and swap, which swaps the arguments of a bilinear map.

[Yaël Dillies]

You can replace "exactly once", by "at most once", right? not for linearity, but for affine maps yes

[Chris Hughes]

Chris Hughes said:

Eric Wieser said:

Sometimes I wonder if we're shooting ourselves in the foot with this heavy point-free approach, and would do better to just write \lam a f x, L a (f x) and use some linearity tactic to find the linearity proof automatically.

I worked on this a little bit recently. If you use every bound variable exactly once then the map will be linear. I have some very untidy code taking lambda terms and turning them into terms using linear composition and swap.

I wonder how much Lean 4 will help us with this. I also want to be able to write down functors with lambda calculus, but making sure I end up with a term I can actually use.

[Eric Wieser]

I would have thought we could just copy the design of continuity

[Eric Wieser]

Which would mean using docs#is_linear_map a lot more

[Chris Hughes]

Eric Wieser said:

I would have thought we could just copy the design of continuity

I'm not at all sure that this is the same problem. You don't need to have a library of tagged lemmas, the condition is that every bound variable is used exactly once; this never changes. The linearity of the functions is part of the type, there's no need for a search for lemmas. And I don't think it can be solved just by applying lemmas. I'm not sure what lemma you would apply first to prove linearity of something like \la f g x y, g y (f x).

[Eric Wieser]

I'm thinking of a more general case like showing \la p, matrix.trace (f p.1 + g p.2) is linear

[Chris Hughes]

Okay. I think that you need a combination of both. The method I had in mind would prove that \la p1 p2, trace (add (f p1) (g p2)) is linear if trace, add, f and g were all bundled linear maps. But you need something else to figure out addition is bilinear and to case split on p.

[Chris Hughes]

So I guess you need something like continuity, but because the category of modules is monoidal closed you can add more things that continuity won't do currently like proving linearity of \la f g x y g y (f x)

[Eric Wieser]

Not really a case split on p, just noting that prod.fst is a linear map

[Chris Hughes]

It's a bit more complicated than that because p appears twice in the term which usually means the map isn't linear but somehow this one works and to be honest I'm not sure exactly what the general rule is that this is a special case of that means it's linear despite p appearing twice.

[Eric Wieser]

Isn't it just the rule that f x + g x is linear in x if both f and g are?

[Yaël Dillies]

Isn't the rule "appears exactly once per summand"?

[Eric Wieser]

My thinking was that the above would be found in the same way that docs#continuous.add is found today

[Eric Wieser]

There's no need for a notion of summands

[Chris Hughes]

Yaël Dillies said:

Isn't the rule "appears exactly once per summand"?

It works I guess because addition is actually linear rather than bilinear. There's a map of type (A →ₗ[R] B) → (A →ₗ[R] C) → (A →ₗ[R] B × C), called linear_map.prod. So if there was a version of add with type A × A →ₗ[R] A, you could rewrite \la p, trace (f p.1 + g p.2) as \la p, trace (add (linear_map.prod (f.comp prod.fst) (g.comp prod.snd) p)) and that can be proven linear using the rule about using every bound variable exactly once.

[Chris Hughes]

So I would prefer to use a rewrite rule instead of something similar to continuous_add to rewrite addition in terms of bundled linear maps, because this allows the more powerful automation to be used afterwards. The earlier example of \lam a f x, L a (f x) probably can't be proven linear using the same approach as the continuity tactic, linearity is really a harder problem than continuity because the space of linear maps is a vector space.