Semi(bi)linear maps with invertible ring_hom

Stream: maths

[Moritz]

Hi,
I've run into another funny problem with the refactorization of bilinear_forms (I sketch it for linear maps): the type V →ₛₗ[J.to_ring_hom] K, where J is a ring_equiv is not a generalization of V →ₗ[K] K, the later is defined as V →ₛₗ[ring_hom.id] K not V →ₛₗ[ring_equiv.id.to_ring_hom] K. I certainly don't want to change the definition of a linear map and adding another hypothesis to each instance, where I need invertibility (to be precise I need J x = 0 iff x = 0) doesn't look great either. As anyone a good idea how to resolve this?
(sorry for spamming zulip with lots of stupid questions)

[Yaël Dillies]

Seems like @Anne Baanen might have an answer for you.

[Anne Baanen]

Not a stupid question at all! I don't think there are easy options apart from changing the definition of linear maps or adding parameters. I'd advise to use an extra instance parameter, probably docs#ring_hom_inv_pair.

[Anne Baanen]

The ring_hom_inv_pair class is already used for semilinear maps and it has an instance for the identity function, suggesting it can be applied to linear maps without too much work.

[Yakov Pechersky]

Do we have global instances of [ring_hom_inv_pair J.to_ring_hom J.symm.to_ring_hom]?

[Eric Wieser]

No, but we have it as a def

[Eric Wieser]

As a global instance it would defeat the point of the mechanism

[Eric Wieser]

Which is to allow conj to be its own inverse

[Heather Macbeth]

@Moritz Could you give more detail, or an example? I'm guessing your question will be related to the semilinear map mechanism, but I can't tell exactly what you're asking.

[Heather Macbeth]

I don't understand this statement:

Moritz said:

the type V →ₛₗ[J.to_ring_hom] K, where J is a ring_equiv is not a generalization of V →ₗ[K] K, the later is defined as V →ₛₗ[ring_hom.id] K not V →ₛₗ[ring_equiv.id.to_ring_hom] K.

[Heather Macbeth]

Because ring_hom.id is definitionally equal to the coercion of ring_equiv.refl:

import data.equiv.ring
variables {R : Type*} [ring R]

example : ring_hom.id R = ring_equiv.refl R := rfl

[Moritz]

Heather Macbeth said:

Because ring_hom.id is definitionally equal to the coercion of ring_equiv.refl:

import data.equiv.ring
variables {R : Type*} [ring R]

example : ring_hom.id R = ring_equiv.refl R := rfl

Ah thanks, I see. So it might only be problem with type-inference.
#check @ortho_smul_right _ _ _ _ _ _ (ring_equiv.refl R) B₁ does type-check.
my example was

lemma is_compl_span_singleton_orthogonal {B : V →ₗ[K] V →ₗ[K] K}
  {x : V} (hx : ¬ B.is_ortho x x) : is_compl (K ∙ x) (B.orthogonal $ K ∙ x) :=
{ inf_le_bot := eq_bot_iff.1 $ span_singleton_inf_orthogonal_eq_bot hx,
  top_le_sup := eq_top_iff.1 $ span_singleton_sup_orthogonal_eq_top hx }

and now with explicit annotations it works:

lemma is_compl_span_singleton_orthogonal {B : V →ₗ[K] V →ₗ[K] K}
  {x : V} (hx : ¬ B.is_ortho x x) : is_compl (K ∙ x) (B.orthogonal $ K ∙ x) :=
{ inf_le_bot := eq_bot_iff.1 $
    (@span_singleton_inf_orthogonal_eq_bot _ _ _ _ _ (ring_equiv.refl K) B x hx),
  top_le_sup := eq_top_iff.1 $ span_singleton_sup_orthogonal_eq_top hx }

but it looks rather ugly.

[Moritz]

(nb: span_singleton_inf_orthogonal_eq_bot is defined only for bilinear forms)

[Heather Macbeth]

I think to understand this example I would need to know how you phrased span_singleton_inf_orthogonal_eq_bot with the new bilinear form definition. But yes, the idea sounds correct!

[Moritz]

its just

lemma span_singleton_inf_orthogonal_eq_bot
  {B : V →ₗ[K] V →ₛₗ[J.to_ring_hom] K} {x : V} (hx : ¬ B.is_ortho x x) :
  (K ∙ x) ⊓ B.orthogonal (K ∙ x) = ⊥ := ..

[Heather Macbeth]

Can I ask why you are generalizing from bilinear forms to V →ₗ[K] V →ₛₗ[J.to_ring_hom] K rather than the full semibilinear case?

[Heather Macbeth]

You might find it easier to do just V →ₗ[K] V →ₗ[K] Kto start with.

[Moritz]

The only use-cases I have in mind are sesquilinear and bilinear forms, but you are correct that is possible to do this in the complete semibilinear case

[Heather Macbeth]

Often, in formalization, the more general case (if it's the "correct" generality ...) is easier than a specialization.

[Moritz]

here it is slightly more involved because sometimes it matters whether the ring_hom is invertible (which started this discussion). doing the full semibilinear case would make some lemmas more symmetric.

[Heather Macbeth]

I see, so you would need to be placing docs#ring_hom_inv_pair hypotheses in certain places, which is technically difficult.

[Heather Macbeth]

I'd be happy to help with that generalization later, if you get it working just for V →ₗ[K] V →ₗ[K] K or M →ₗ[R] M →ₗ⋆[R] R (or your variant V →ₗ[K] V →ₛₗ[J.to_ring_hom] K) for now.

[Moritz]

I made a PR: https://github.com/leanprover-community/mathlib/pull/10992 I think we should find a better way to deal with the issue discussed above, but for now I think it is ok.