    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of linear maps.
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    import Algebra.Module.Properties            as ModuleProperties
    import Algebra.Module.Morphism.Structures   as MorphismStructures

    open import Algebra using (CommutativeRing)
    open import Algebra.Module using (Module)
    open import Level using (Level)

    module Algebra.Module.Morphism.ModuleHomomorphism
      {r ℓr m ℓm : Level}
      {ring      : CommutativeRing r ℓr}
      (modA modB  : Module ring m ℓm)
      (open Module modA using () renaming (Carrierᴹ to A; rawModule to rawModA))
      (open Module modB using () renaming (Carrierᴹ to B; rawModule to rawModB))
      {f : A → B}
      (open MorphismStructures.ModuleMorphisms rawModA rawModB)
      (isModuleHomomorphism : IsModuleHomomorphism f)
      where

    open import Axiom.DoubleNegationElimination using (DoubleNegationElimination)
    open import Data.Product.Base using (∃₂; _×_; _,_)
    open import Relation.Binary.Reasoning.MultiSetoid
    open import Relation.Nullary          using (¬_)
    open import Relation.Nullary.Negation using (contraposition)

    module A = Module modA
    module B = Module modB
    module PA = ModuleProperties modA
    module PB = ModuleProperties modB
    open CommutativeRing ring renaming (Carrier to S)

    open IsModuleHomomorphism isModuleHomomorphism

    -- Some of the lemmas below only hold for continously scalable,
    -- non-trivial functions, i.e., f x = f (s y) and f ≠ const 0.
    -- This is a handy abbreviation for that rather verbose term.
    NonTrivial : A → Set (r Level.⊔ m Level.⊔ ℓm)
    NonTrivial x = ∃₂ λ s y → (s A.*ₗ x A.≈ᴹ y) × (f y B.≉ᴹ B.0ᴹ)

    x≈0⇒fx≈0 : ∀ {x} → x A.≈ᴹ A.0ᴹ → f x B.≈ᴹ B.0ᴹ
    x≈0⇒fx≈0 {x} x≈0 = begin⟨ B.≈ᴹ-setoid ⟩
      f x    ≈⟨ ⟦⟧-cong x≈0 ⟩
      f A.0ᴹ ≈⟨ 0ᴹ-homo ⟩
      B.0ᴹ   ∎

    fx≉0⇒x≉0 : ∀ {x} → f x B.≉ᴹ B.0ᴹ → x A.≉ᴹ A.0ᴹ
    fx≉0⇒x≉0 = contraposition x≈0⇒fx≈0

    -- Zero is a unique output of non-trivial (i.e. - ≉ `const 0`) linear map.
    x≉0⇒f[x]≉0 : ∀ {x} → NonTrivial x → x A.≉ᴹ A.0ᴹ → f x B.≉ᴹ B.0ᴹ
    x≉0⇒f[x]≉0 {x} (s , y , s·x≈y , fy≉0) x≉0 =
      PB.x*y≉0⇒y≉0 ( λ s·fx≈0 → fy≉0 ( begin⟨ B.≈ᴹ-setoid ⟩
                       f y          ≈⟨ ⟦⟧-cong (A.≈ᴹ-sym s·x≈y) ⟩
                       f (s A.*ₗ x) ≈⟨ *ₗ-homo s x ⟩
                       s B.*ₗ f x   ≈⟨ s·fx≈0 ⟩
                       B.0ᴹ         ∎ )
                   )

    -- f is odd (i.e. - f (-x) ≈ - (f x)).
    fx+f[-x]≈0 : (x : A) → f x B.+ᴹ f (A.-ᴹ x) B.≈ᴹ B.0ᴹ
    fx+f[-x]≈0 x = begin⟨ B.≈ᴹ-setoid ⟩
      f x B.+ᴹ f (A.-ᴹ x) ≈⟨ B.≈ᴹ-sym (+ᴹ-homo x (A.-ᴹ x)) ⟩
      f (x A.+ᴹ (A.-ᴹ x)) ≈⟨ ⟦⟧-cong (A.-ᴹ‿inverseʳ x) ⟩
      f A.0ᴹ              ≈⟨ 0ᴹ-homo ⟩
      B.0ᴹ                ∎

    f[-x]≈-fx : (x : A) → f (A.-ᴹ x) B.≈ᴹ B.-ᴹ f x
    f[-x]≈-fx x = B.uniqueʳ‿-ᴹ (f x) (f (A.-ᴹ x)) (fx+f[-x]≈0 x)

    -- A non-trivial linear function is injective.
    fx≈fy⇒fx-fy≈0 : ∀ {x y} → f x B.≈ᴹ f y → f x B.+ᴹ (B.-ᴹ f y) B.≈ᴹ B.0ᴹ
    fx≈fy⇒fx-fy≈0 {x} {y} fx≈fy = begin⟨ B.≈ᴹ-setoid ⟩
      f x B.+ᴹ (B.-ᴹ f y) ≈⟨ B.+ᴹ-congˡ (B.-ᴹ‿cong (B.≈ᴹ-sym fx≈fy)) ⟩
      f x B.+ᴹ (B.-ᴹ f x) ≈⟨ B.-ᴹ‿inverseʳ (f x) ⟩
      B.0ᴹ                ∎

    fx≈fy⇒f[x-y]≈0 : ∀ {x y} → f x B.≈ᴹ f y → f (x A.+ᴹ (A.-ᴹ y)) B.≈ᴹ B.0ᴹ
    fx≈fy⇒f[x-y]≈0 {x} {y} fx≈fy = begin⟨ B.≈ᴹ-setoid ⟩
      f (x A.+ᴹ (A.-ᴹ y)) ≈⟨ +ᴹ-homo x (A.-ᴹ y) ⟩
      f x B.+ᴹ f (A.-ᴹ y) ≈⟨ B.+ᴹ-congˡ (f[-x]≈-fx y) ⟩
      f x B.+ᴹ (B.-ᴹ f y) ≈⟨ fx≈fy⇒fx-fy≈0 fx≈fy ⟩
      B.0ᴹ                ∎

    module _ {dne : DoubleNegationElimination _} where

      fx≈0⇒x≈0 : ∀ {x} → NonTrivial x → f x B.≈ᴹ B.0ᴹ → x A.≈ᴹ A.0ᴹ
      fx≈0⇒x≈0 {x} (s , y , s·x≈y , fy≉0) fx≈0 =
        dne ¬x≉0
        where
        ¬x≉0 : ¬ (x A.≉ᴹ A.0ᴹ)
        ¬x≉0 = λ x≉0 → x≉0⇒f[x]≉0 (s , y , s·x≈y , fy≉0) x≉0 fx≈0

      inj-lm : ∀ {x y} →
               (∃₂ λ s z → ((s A.*ₗ (x A.+ᴹ A.-ᴹ y) A.≈ᴹ z) × (f z B.≉ᴹ B.0ᴹ))) →
               f x B.≈ᴹ f y → x A.≈ᴹ y
      inj-lm {x} {y} (s , z , s·[x-y]≈z , fz≉0) fx≈fy =
        begin⟨ A.≈ᴹ-setoid ⟩
        x             ≈⟨ x≈--y ⟩
        A.-ᴹ (A.-ᴹ y) ≈⟨ PA.-ᴹ-involutive y ⟩
        y             ∎
        where
        x-y≈0 : x A.+ᴹ (A.-ᴹ y) A.≈ᴹ A.0ᴹ
        x-y≈0 = fx≈0⇒x≈0 (s , z , s·[x-y]≈z , fz≉0) (fx≈fy⇒f[x-y]≈0 fx≈fy)
        x≈--y : x A.≈ᴹ A.-ᴹ (A.-ᴹ y)
        x≈--y = A.uniqueʳ‿-ᴹ (A.-ᴹ y) x
          ( begin⟨ A.≈ᴹ-setoid ⟩
            A.-ᴹ y A.+ᴹ x ≈⟨ A.+ᴹ-comm (A.-ᴹ y) x ⟩
            x A.+ᴹ A.-ᴹ y ≈⟨ x-y≈0 ⟩
            A.0ᴹ          ∎
          )