Zulip Chat Archive

Stream: maths

Topic: Semi(bi)linear maps with invertible ring_hom


Moritz (Dec 22 2021 at 11:43):

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 (Dec 22 2021 at 12:30):

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

Anne Baanen (Dec 22 2021 at 13:50):

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 (Dec 22 2021 at 13:51):

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 (Dec 22 2021 at 14:03):

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

Eric Wieser (Dec 22 2021 at 14:13):

No, but we have it as a def

Eric Wieser (Dec 22 2021 at 14:14):

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

Eric Wieser (Dec 22 2021 at 14:14):

Which is to allow conj to be its own inverse

Heather Macbeth (Dec 22 2021 at 15:47):

@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 (Dec 22 2021 at 15:54):

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 (Dec 22 2021 at 15:55):

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 (Dec 22 2021 at 16:23):

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 (Dec 22 2021 at 16:24):

(nb: span_singleton_inf_orthogonal_eq_bot is defined only for bilinear forms)

Heather Macbeth (Dec 22 2021 at 16:32):

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 (Dec 22 2021 at 16:34):

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 (Dec 22 2021 at 16:35):

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 (Dec 22 2021 at 16:37):

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

Moritz (Dec 22 2021 at 16:45):

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 (Dec 22 2021 at 16:47):

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

Moritz (Dec 22 2021 at 16:50):

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 (Dec 22 2021 at 16:51):

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

Heather Macbeth (Dec 22 2021 at 16:54):

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 (Dec 23 2021 at 12:32):

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.


Last updated: Dec 20 2023 at 11:08 UTC