------------------------------------------------------------------------
-- 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ᴹ ∎
)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4