SeedOperations.lean

1 import KomorebiVerification.SeedRankOperations
2 
3 set_option autoImplicit false
4 noncomputable section
5 namespace Komorebi.PaperIRelease.SeedOperations
6 open Komorebi.SeedRankBasics Komorebi.SeedRankOperations
7 universe u v
8 
9 /-- The regular left module is generated by its unit, over any unital semiring. -/
10 theorem regular_generates_one (A : Type u) [Semiring A] : Generates A A {1} := by
11   apply (generates_singleton_iff_surjective A A 1).mpr
12   intro a
13   exact ⟨a, by simp [oneSeedMap]⟩
14 
15 /-- Algebra generators are irrelevant to the regular-module seed rank. -/
16 theorem regular_seedRank (A : Type u) [Semiring A] [Nontrivial A] :
17     seedRank A A = 1 :=
18   (cyclic_iff_seedRank_eq_one A A).mp ⟨1, regular_generates_one A⟩
19 
20 /-- Both cardinal bounds for the same acting algebra on a binary direct sum. -/
21 theorem shared_direct_sum_bounds (A M N : Type u) [Semiring A]
22     [AddCommMonoid M] [Module A M] [AddCommMonoid N] [Module A N] :
23     max (seedRank A M) (seedRank A N) ≤ seedRank A (M × N) ∧
24       seedRank A (M × N) ≤ seedRank A M + seedRank A N := by
25   constructor
26   · apply max_le
27     · exact seedRank_le_of_surjective (LinearMap.fst A M N) (fun m => ⟨(m, 0), rfl⟩)
28     · exact seedRank_le_of_surjective (LinearMap.snd A M N) (fun n => ⟨(0, n), rfl⟩)
29   · exact seedRank_prod_le_add A M N
30 
31 section Annihilator
32 variable {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M]
33 
34 /-- The actual kernel of scalar evaluation at a vector. -/
35 def vectorAnnihilator (s : M) : Ideal A := (oneSeedMap A M s).ker
36 
37 @[simp] theorem mem_vectorAnnihilator (s : M) (a : A) :
38     a ∈ vectorAnnihilator (A := A) s ↔ a • s = 0 := Iff.rfl
39 
40 /-- Right-ideal closure of the left annihilator is exactly annihilation of its cyclic span. -/
41 theorem annihilator_two_sided_iff (s : M) :
42     (∀ a ∈ vectorAnnihilator (A := A) s, ∀ b : A, a * b ∈ vectorAnnihilator (A := A) s) ↔
43       ∀ a ∈ vectorAnnihilator (A := A) s, ∀ m ∈ Submodule.span A {s}, a • m = 0 := by
44   constructor
45   · intro h a ha m hm
46     obtain ⟨b, rfl⟩ := (Submodule.mem_span_singleton.mp hm)
47     rw [smul_smul]
48     exact h a ha b
49   · intro h a ha b
50     change (a * b) • s = 0
51     rw [mul_smul]
52     exact h a ha (b • s) (Submodule.smul_mem _ _ (Submodule.subset_span (by simp)))
53 
54 /-- For a cyclic vector, right-ideal closure is equality with the module annihilator. -/
55 theorem cyclic_annihilator_two_sided_iff (s : M) (hs : Generates A M {s}) :
56     (∀ a ∈ vectorAnnihilator (A := A) s, ∀ b : A, a * b ∈ vectorAnnihilator (A := A) s) ↔
57       ∀ a : A, a ∈ vectorAnnihilator (A := A) s ↔ ∀ m : M, a • m = 0 := by
58   rw [annihilator_two_sided_iff]
59   constructor
60   · intro h a
61     constructor
62     · intro ha m
63       exact h a ha m (by rw [hs]; trivial)
64     · intro ha
65       exact ha s
66   · intro h a ha m _
67     exact (h a).mp ha m
68 
69 
70 /-- The criterion in the standard two-sided-ideal interface. -/
71 theorem annihilator_isTwoSided_iff (s : M) :
72     (vectorAnnihilator (A := A) s).IsTwoSided ↔
73       ∀ a ∈ vectorAnnihilator (A := A) s,
74         ∀ m ∈ Submodule.span A {s}, a • m = 0 := by
75   rw [Ideal.isTwoSided_iff, ← annihilator_two_sided_iff]
76   constructor
77   · intro h a ha b
78     exact h b ha
79   · intro h a b ha
80     exact h a ha b
81 
82 /-- With a cyclic vector, two-sidedness is literal equality to the module annihilator. -/
83 theorem cyclic_annihilator_eq_module_iff (s : M) (hs : Generates A M {s}) :
84     (vectorAnnihilator (A := A) s).IsTwoSided ↔
85       vectorAnnihilator (A := A) s = Module.annihilator A M := by
86   rw [annihilator_isTwoSided_iff, ← annihilator_two_sided_iff,
87     cyclic_annihilator_two_sided_iff s hs]
88   constructor
89   · intro h
90     ext a
91     exact (h a).trans Module.mem_annihilator.symm
92   · intro h a
93     rw [h, Module.mem_annihilator]
94 
95 end Annihilator
96 end Komorebi.PaperIRelease.SeedOperations

Back to source controls