Pretty printer omits notation

Stream: general

[Heather Macbeth]

Why doesn't the pretty printer know about the notation for conjugate linear maps?

notation E ` ≃ₗᵢ⋆[`:25 R:25 `] `:0 E₂:0 :=
  linear_isometry_equiv (@star_ring_aut R _ _ : R →+* R) E E₂

The declaration docs#continuous_linear_map.adjoint is constructed using this notation in the source:

def adjoint : (E →L[𝕜] F) ≃ₗᵢ⋆[𝕜] (F →L[𝕜] E)

but it displays using the less specific semilinear map notation

def adjoint : (E →L[𝕜] F) ≃ₛₗᵢ[↑conj] (F →L[𝕜] E)

both in the docs, and in the infoview

import analysis.inner_product_space.adjoint

#check continuous_linear_map.adjoint

[Eric Wieser]

Does it do better if you remove the notation for conj? (Not that we want to do that)

[Eric Wieser]

(docs#conj is itself notation, which explains why that link doesn't work)

[Heather Macbeth]

No.

import algebra.star.module

variables {𝕜 : Type*} [comm_ring 𝕜] [star_ring 𝕜]
variables {E : Type*} [add_comm_group E] [module 𝕜 E]
variables {F : Type*} [add_comm_group F] [module 𝕜 F]

def adjoint : (E →ₗ[𝕜] F) ≃ₗ⋆[𝕜] (F →ₗ[𝕜] E) := sorry

#check adjoint

[Heather Macbeth]

Infoview check result says

adjoint : (?M_4 →ₗ[?M_1] ?M_7) ≃ₛₗ[↑star_ring_aut] ?M_7 →ₗ[?M_1] ?M_4

[Floris van Doorn]

My first thought was that it might have something to do with the (_ : R →+* R)), but changing it to an explicit coe doesn't help :-(

notation E ` →ₗᵢ⋆[`:25 R:25 `] `:0 E₂:0 := linear_isometry (@coe _ (R →+* R) _ (@star_ring_aut R _ _)) E E₂
def foo {𝕜 E F : Type*} [comm_semiring 𝕜] [star_ring 𝕜] [semi_normed_group E]
  [semi_normed_group E₂] [module 𝕜 E] [module 𝕜 E₂] : E →ₗᵢ⋆[𝕜] E₂ :=
begin
  -- no correct notation
end

[Floris van Doorn]

oh, maybe the problem is the @: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20with.20implicit.20arguments.20.3F/near/200916740

[Heather Macbeth]

Interesting! Do you think the priority fix should work in this case too?

[Floris van Doorn]

The problem is not the other notation. The problem is that for some reason this notation never "fires" in the pretty-printer (commenting the →ₗᵢ and →ₛₗᵢ causes it to just print no notation).

[Heather Macbeth]

If I change star_ring_aut to take R as an explicit argument, to avoid the

@star_ring_aut R _ _

should that then fix it?

[Floris van Doorn]

I don't know, maybe?

[Floris van Doorn]

The coe might also be problematic.

Here is something that does work:

abbreviation my_star_ring_aut (R : Type*) [comm_semiring R] [star_ring R] : R →+* R := ↑(@star_ring_aut R _ _)
notation E ` →ₗᵢ⋆[`:25 R:25 `] `:0 E₂:0 := linear_isometry (my_star_ring_aut R) E E₂

def foo {𝕜 E F : Type*} [comm_semiring 𝕜] [star_ring 𝕜] [semi_normed_group E]
  [semi_normed_group E₂] [module 𝕜 E] [module 𝕜 E₂] : E →ₗᵢ⋆[𝕜] E₂ :=
begin

end

[Floris van Doorn]

Hopefully you can transform that into something that is acceptable.

[Floris van Doorn]

I think that all @ and (_ : ...) notations will break the pretty printer. So you have to somehow specify what you want without them.

[Heather Macbeth]

I tried just making R explicit at branch#star_ring_aut_implicit, let's see what that looks like when it compiles.

[Floris van Doorn]

I don't think that works. I tried inserting these lines in normed_space/linear_isometry and that fails:

abbreviation my_star_ring_aut (R : Type*) [comm_semiring R] [star_ring R] : ring_aut R := star_ring_aut
notation E ` →ₗᵢ⋆[`:25 R:25 `] `:0 E₂:0 := linear_isometry (my_star_ring_aut R : R →+* R) E E₂

def foo {𝕜 E F : Type*} [comm_semiring 𝕜] [star_ring 𝕜] [semi_normed_group E]
  [semi_normed_group E₂] [module 𝕜 E] [module 𝕜 E₂] : E →ₗᵢ⋆[𝕜] E₂ :=
begin
  -- no correct printing
end

[Floris van Doorn]

You need to also get rid of the (_ : _) notation

[Heather Macbeth]

Indeed, you're quite right. But with both changes (making star_ring_aut into star_ring_end, of type R →+* R rather than R ≃+* R, and making the R argument explicit), it seems to work, at least this check works for me locally.

I'll get the branch to compile and then open a PR for a discussion. This amounts to reverting part of the work done in #9640: in that PR (among other things) complex conjugation was upgraded from ring hom to ring equiv. What do you think, @Frédéric Dupuis @Eric Wieser ?

[Heather Macbeth]

#11418 for the change.

[Frédéric Dupuis]

I'm happy with this change.

[Eric Wieser]

I'm fine with changing what conj points to, but I think star_ring_aut should still exist, even if we're changing to nothing using it

[Eric Wieser]

(Keeping it alongside docs#star_ring_equiv is consistent with having docs#star_mul_aut and docs#star_mul_equiv)

[Frédéric Dupuis]

So I'm guessing this @ issue is why the notation for inner products doesn't always show up in the pretty printer, since it is defined as:

class has_inner (𝕜 E : Type*) := (inner : E → E → 𝕜)

and then we usually define notation for it as:

local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y

Is there a way to make 𝕜 explicit? I tried playing around a bit with the definition to no avail.

[Floris van Doorn]

class has_inner (𝕜 E : Type*) := (inner ( ) : E → E → 𝕜) makes both 𝕜 and E explicit.
The other option is to write an alias:

class has_inner (𝕜 E : Type*) := (inner' : E → E → 𝕜)
def inner (𝕜 : Type*) {E : Type*} [has_inner 𝕜 E] (x y : E) : 𝕜 :=
has_inner.inner' x y