GrammarFactorization.lean

1 import PaperIRelease.GrammarAlgebra
2 import KomorebiVerification.SeedRankOperations
3 
4 set_option autoImplicit false
5 set_option linter.unusedVariables false
6 set_option linter.unnecessarySimpa false
7 set_option linter.style.haveILetI false
8 
9 noncomputable section
10 
11 namespace Komorebi.PaperIRelease.GrammarAlgebra
12 
13 universe u
14 variable {K V E M : Type u} [Field K] [Fintype V]
15 variable [AddCommGroup M] [Module K M]
16 variable {G : Grammar K V E}
17 
18 /-- The algebraic hull is unchanged when the constructed grammar action is replaced by its image. -/
19 theorem CollapsedRealization.span_imageAlgebra_eq (X : CollapsedRealization G M) (S : Set M) :
20     letI : Module (Algebra G) M := Module.compHom M X.action.toRingHom
21     letI : Module X.action.range M := Module.compHom M X.action.range.val.toRingHom
22     (Submodule.span (Algebra G) S : Set M) = Submodule.span X.action.range S := by
23   letI : Module (Algebra G) M := Module.compHom M X.action.toRingHom
24   letI : Module X.action.range M := Module.compHom M X.action.range.val.toRingHom
25   ext x
26   constructor
27   · intro hx
28     induction hx using Submodule.span_induction with
29     | mem x hx => exact Submodule.subset_span hx
30     | zero => exact Submodule.zero_mem _
31     | add x y hx hy ihx ihy => exact Submodule.add_mem _ ihx ihy
32     | smul a x hx ih =>
33         exact Submodule.smul_mem _ (X.action.rangeRestrict a) ih
34   · intro hx
35     induction hx using Submodule.span_induction with
36     | mem x hx => exact Submodule.subset_span hx
37     | zero => exact Submodule.zero_mem _
38     | add x y hx hy ihx ihy => exact Submodule.add_mem _ ihx ihy
39     | smul a x hx ih =>
40         obtain ⟨b, hb⟩ := a.property
41         have h := Submodule.smul_mem (Submodule.span (Algebra G) S) b ih
42         change (X.action b) x ∈ Submodule.span (Algebra G) S at h
43         change (a : Module.End K M) x ∈ Submodule.span (Algebra G) S
44         have he : X.action b = (a : Module.End K M) := hb
45         rw [he] at h
46         exact h
47 
48 /-- PSC-I-P-ACTION-FACTORIZATION: seed rank is preserved by passage to the realized image algebra. -/
49 theorem CollapsedRealization.seedRank_imageAlgebra_eq (X : CollapsedRealization G M) :
50     letI : Module (Algebra G) M := Module.compHom M X.action.toRingHom
51     letI : Module X.action.range M := Module.compHom M X.action.range.val.toRingHom
52     SeedRankBasics.seedRank (Algebra G) M = SeedRankBasics.seedRank X.action.range M := by
53   letI : Module (Algebra G) M := Module.compHom M X.action.toRingHom
54   let f : M →ₛₗ[X.action.toRingHom] M :=
55     { toFun := id
56       map_add' := fun _ _ => rfl
57       map_smul' := fun _ _ => rfl }
58   exact SeedRankOperations.seedRank_imageAlgebra_eq X.action f Function.bijective_id
59 
60 end Komorebi.PaperIRelease.GrammarAlgebra

Back to source controls