Proofs of some linearity axioms.

[capn-freako]

A definition of "linear map" along w/ some proofs of a few axioms of linearity.

[Taneb]

Looking at this, I'm not convinced that this is the right design.

• ¬-involutive-≈ᴬ, ¬-involutive-≈ᴮ, -ᴬ‿involutive, and -ᴮ‿involutive are properties of the modules, not of the morphism.
• Furthermore, -ᴬ‿involutive and -ᴮ‿involutive are already implied by the Module bundle. We can create a proof of this by Algebra.Properties.Group.⁻¹-involutive +ᴹ-group.
• Removing those fields makes the LinMap record just a bundle of a function with an IsModuleHomomorphism. I'd personally like to see homomorphism bundles added to the library, but this isn't the way to do it. Without those bundles, I'd pass a function and a proof it's a homomorphism separately into the anonymous module in Algebra.Module.Morphism.Linear.Properties. EDIT: thinking about it, I'd just go for the function-and-structure option here, the bundles are unnecessary.
• I suspect ¬-involutive-≈ lets us prove that equality for the elements of the module in general is decidable (I'm not sure about this). If that's true, I think it'd be worth adding algebraic structures with decidable equality as a thing in the library.
• We really shouldn't postulate things like Extensionality in stdlib. If it's necessary we should pass it as a parameter. In this case it doesn't seem to actually be being used, so it should be OK to remove it.

[JacquesCarette]

I agree with @Taneb 's comments, and added a few more.

This really should be done 'on top of' homomorphism definitions.

[capn-freako]

Thank you, both, for your thoughtful responses!
I'll start working on addressing your concerns immediately.

I'm new to Agda and, particularly, to its standard library.
So, I need to ask a few questions of clarification.
Thanks, in advance, for your patience!

@Taneb ,

1. Can you tell me what you mean by "function-and-structure option"?
2. Where do you think algebraic structures w/ decidable equality should live?

@JacquesCarette ,

I'll respond to your requested changes, individually, to preserve focused context.

Thanks,
-db

[Taneb]

I'm new to Agda and, particularly, to its standard library. So, I need to ask a few questions of clarification. Thanks, in advance, for your patience!

No worries, glad to have y

1. Can you tell me what you mean by "function-and-structure option"?

The LinMap record you've defined contains a function and a bunch of properties of that function. Until now, we've defined records that look like IsFooHomomorphism, parameterized on the function. It'd fit better with the standard library to have a record IsLinearMap (f : A -> B). and pass the function and the proof that it's a linear map as separate arguments. (In addition, note that IsLinearMap should be the same as IsModuleHomomorphism)

2. Where do you think _algebraic structures w/ decidable equality_ should live?

I think this should be a bigger discussion, honestly. I'm going to make another issue about this. (as an aside, I think I was wrong when I said that your ¬-involutive-≈ properties give the module decidable equality. I've looked around and thought a bit, and it's a weaker condition that's called "stability" elsewhere in the library

[MatthewDaggitt]

Thank you for the great first PR, we'd definitely welcome the content! I agree with the comments given by @Taneb and @JacquesCarette above though. Looking forward to seeing the updated version 👍

[capn-freako]

The LinMap record you've defined contains a function and a bunch of properties of that function. Until now, we've defined records that look like IsFooHomomorphism, parameterized on the function. It'd fit better with the standard library to have a record IsLinearMap (f : A -> B). and pass the function and the proof that it's a linear map as separate arguments. (In addition, note that IsLinearMap should be the same as IsModuleHomomorphism)

Ah, okay. So, it sounds like what you're proposing is:

1. Skip my definition of LinMap entirely.
2. Pack my linearity axiom proofs into a module that is predicated upon an IsModuleHomomorphism instance.

Or, were you suggesting that I add my proofs to the existing definition of IsModuleHomomorphism?
If a new module, should it be a Bundle?

Thanks,
-db

[capn-freako]

Okay, @Taneb & @MatthewDaggitt , I think I've addressed all your concerns.
Please, let me know if I've missed something.

Thanks, again, for your helpful guidance!
-db

[capn-freako]

A question, regarding Git protocol: Am I supposed to click the Resolve Conversation button when I think I've addressed the concern, or is it for the requestor to click only when they're satisfied that their concern has actually been addressed?

[MatthewDaggitt]

A question, regarding Git protocol: Am I supposed to click the Resolve Conversation button when I think I've addressed the concern, or is it for the requestor to click only when they're satisfied that their concern has actually been addressed?

I think it's fine either way. If you have doubts about whether you've addressed properly then I'd leave it open, otherwise feel free to hit "Resolve" 👍

[MatthewDaggitt]

You haven't picked the simplest first PR @capn-freako, thank you for sticking it out 😄

The module structure now looks pretty good to me, so I've left some comments about the style.

Just a heads up that there'll probably be one more lot of comments after this round.

[MatthewDaggitt]

Thanks! Here's another round of comments!

[capn-freako]

Hi all,

I'm wondering what I can do, to bring this to closure.
It's kind of a pain, having my master branch blocked by this.
(I know, my bad; should've used a branch; I think I've learned my lesson. ;-) )

Also, I've got a third PR waiting in the wings. (It's dependent upon both this one and my second.)
It completes a "trifecta" that I agreed to do, in this working group I'm participating in, which will provide a denotation for Data.Vec in terms of linear maps between abstract vector spaces.
I've been told by the group leader that it will be quite useful towards our common aims.
And I'd like to get it available to the rest, without asking them to work from my fork of the standard library.

Anything I can do, to help close this?

Thanks,
-db
:)

[MatthewDaggitt]

A friend suggested that the large number of commits coming in through this PR may be an impediment to its acceptance.
Would you all prefer that I squash those?
(I'm somewhere in the Journeyman phase of my Git learning and never quite sure when it's appropriate to squash commits.)

Your friend is right in that the commit history is messy and we don't want to add it to the main branch, but don't worry, we will squash all the commits down automatically when it's merged in!

Anything I can do, to help close this?

Apologies for the delay, I'm back from travelling and will try and be more prompt to replying to it now. Once the latest round of comments are addressed should be pretty close to being ready to merge in 👍 Thanks for your patience!

[capn-freako]

Completed my responses to Matthew's comments.
Will push code changes shortly.

[capn-freako]

But, doesn't it need to apply to, at least, a semimodule?
That is, isn't left zero a (semi)module-centric concept?

[MatthewDaggitt]

A few more minor comments.

[MatthewDaggitt]

Okay so once the module parameters change is made, this is ready 👍

[capn-freako]

Thanks, Matthew!

Changes have been pushed.

[MatthewDaggitt]

Merged in. Thanks for the great PR @capn-freako, and for your patience!

[capn-freako]

Thanks, Matthew!

And thank you, all, for your helpful guidance and patience during my first attempt to contribute. :)

[Taneb]

Revisiting this, I don't think this PR should have been merged.

In particular, the module Algebra.Module.Morphism.ModuleHomomorphism has
several glaring issues:

• None of the properties listed rely on right multiplication; the module should have been parameterized on LeftModule
• NonTrivial is equivalent to the more standard property of "not being in the kernel of f" i.e. f x B.≉ᴹ B.0ᴹ (see proof)
• The conditions of x≉0⇒f[x]≉0 are unnecessarily strong; the consequent is implied by NonTrivial x as it is equivalent to not being in the kernel
• fx+f[-x]≈0 and f[-x]≈-fx do not talk about scalar multiplication at all; they are more properly properties of group homomorphisms (that could potentially be re-exported in a module for properties of module homomorphisms)
• fx≈fy⇒fx-fy≈0 does not refer to f at all; it is righly a property of groups.
• fx≈fy⇒f[x-y]≈0 is again a property of group homomorphisms
• fx≈0⇒x≈0 makes two contradictory assumptions, and thus is trivial and can be proven by ex falso quodlibet.
• inj-lm also makes two contradictory assumptions. The first argument suggests that x - y is not in the kernel, and the second suggests that it is in the kernel.

For the other additions:

• Algebra.Module.Properties should have been Algebra.Module.Properties.Module, and could have been defined simpler using public renaming imports
• Algebra.Module.Properties.Semimodule again doesn't use right multiplication, so it could have been defined over LeftSemimodule. In addition, the definitions aren't that generally useful.

NotInKernel : A → Set ℓm
NotInKernel x = f x B.≉ᴹ B.0ᴹ

NotInKernel⇒NonTrivial : ∀ x → NotInKernel x → NonTrivial x
NotInKernel⇒NonTrivial x x∉K = 1# , x , A.*ₗ-identityˡ x , x∉K

NonTrivial⇒NotInKernel : ∀ x → NonTrivial x → NotInKernel x
NonTrivial⇒NotInKernel x (s , y , s*x≈y , y∉K) x∈K = y∉K y∈K
  where
    y∈K : f y B.≈ᴹ B.0ᴹ
    y∈K = begin⟨ B.≈ᴹ-setoid ⟩
      f y ≈˘⟨ ⟦⟧-cong s*x≈y ⟩
      f (s A.*ₗ x) ≈⟨ *ₗ-homo s x ⟩
      s B.*ₗ f x ≈⟨ B.*ₗ-congˡ x∈K ⟩
      s B.*ₗ B.0ᴹ ≈⟨ B.*ₗ-zeroʳ s ⟩
      B.0ᴹ ∎

[JacquesCarette]

Luckily, this is so new that I don't think anything relies on it yet. So fixing it shouldn't be a big deal, as there's nothing to deprecate!

[JacquesCarette]

(or am I wrong and this made it out in 1.7?)

[Taneb]

@JacquesCarette you were correct, this is not in any released branch

[JacquesCarette]

That helps a lot - fix away! I agree with all the suggestions you made.

[MatthewDaggitt]

Yup, @Taneb if you have a PR going to fix these then great. Otherwise can you open an issue under the v2.0 milestone with the above comments in so that they don't get missed?