Stream: Beginner Questions

Topic: defining module homomorphisms

Charles Staats (Aug 07 2022 at 02:51):

I'm trying to define a homomorphism between modules over a ring as a special case of abelian group homomorphisms. I'm trying to imitate the definition of abelian_group_hom in https://isabelle.in.tum.de/library/HOL/HOL-Algebra/outline.pdf (page 127), but it's not going so well.

Here's my non-working version:

locale module_hom = R?: cring + M?: module R M + N?: module R N + φ?: abelian_group_hom
  for M (structure) and N (structure) +
  assumes "⟦m ∈ carrier M; r ∈ carrier R⟧ ⟹ r ⊙⇩N (φ.h m) = φ.h (r ⊙⇩M m)"

Can someone help me fix this mess?

Wenda Li (Aug 07 2022 at 15:34):

If not so sure, I usually prefer to write down all the locale arguments explicitly. The following snippet at least compiles:

locale module_hom = R?: cring R + M?: module R M + N?: module R N
    + φ:abelian_group_hom M N h
    for R and M and N and h +
  assumes "⟦m ∈ carrier M; r ∈ carrier R⟧ ⟹ r ⊙⇘N⇙ (h m) = h (r ⊙⇘M⇙ m)"

Charles Staats (Aug 07 2022 at 20:08):

Thanks! What do the slanted arrows ⇘N⇙ mean, and how do they differ from ⇩N (which was represented in the editor as an N in the subscript)?

Wenda Li (Aug 08 2022 at 03:21):

X⇘N⇙ has a special meaning: it means the operation X on some structure (record) N. In contrast, X⇩N as a whole is a variable name (i.e., just like ordinary strings).

Last updated: Apr 20 2024 at 08:16 UTC