Zulip Chat Archive

Stream: new members

Topic: Is there an easy way to get obvious instances on structures?

Scott Carnahan (Dec 12 2023 at 16:36):

I have been using the following structure with no problems:

import Mathlib.Algebra.Module.LinearMap
import Mathlib.RingTheory.HahnSeries

structure VertexOperator (R : Type*) (V : Type*) [CommRing R] [AddCommGroup V] [Module R V] where
  toMap : V →ₗ[R] HahnSeries  V

but building up to instance [CommRing R] [AddCommGroup V] [Module R V] : Module R (VertexOperator R V) took about 100 lines of code with lots of ext, intro and simp to deal with the various fields. It seems that linear maps already have an R-module structure, but my use of structure means this fact is obscured. Is there an easier way to get an R-module action?

Eric Wieser (Dec 12 2023 at 16:40):

You want to end up using docs#Function.Injective.addCommGroup and docs#Function.Injective.module

Eric Wieser (Dec 12 2023 at 16:40):

Though the easiest option by far is abbrev VertexOperator := V →ₗ[R] HahnSeries ℤ V

Scott Carnahan (Dec 12 2023 at 16:41):

Are there downsides to abbrev?

Eric Wieser (Dec 12 2023 at 16:41):

Whether that's a good idea depends on whether there are behaviors that make sense for VertexOperator R V which do not make sense for V →ₗ[R] HahnSeries ℤ V

Eric Wieser (Dec 12 2023 at 16:41):

For instance, we can't use it for abbrev Polynomial := Finsupp ... because we want * to mean different things on polynomials (convolutive) and supported functions (pointwise)

Scott Carnahan (Dec 12 2023 at 16:42):

I see. Thanks!

Eric Wieser (Dec 12 2023 at 16:42):

Actually, here you could use docs#Equiv.module

Last updated: Dec 20 2023 at 11:08 UTC