GrammarIdeal.lean

1 import PaperIRelease.GrammarEquivalence
2 import Mathlib.RingTheory.TwoSidedIdeal.Basic
3 import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
4 
5 /-!
6 Literal two-sided-ideal specialization.  The path algebra uses its standard
7 vertex/arrow presentation.  The final algebra is identified with the quotient
8 of that algebra by an arbitrary two-sided ideal, with the comparison maps and
9 their inverse identities proved from the quotient universal properties.
10 -/
11 
12 set_option autoImplicit false
13 set_option maxHeartbeats 4000000
14 set_option linter.unusedVariables false
15 set_option linter.unnecessarySimpa false
16 set_option linter.unusedSimpArgs false
17 
18 noncomputable section
19 
20 namespace Komorebi.PaperIRelease.GrammarAlgebra
21 
22 open CategoryTheory
23 universe u
24 variable {K V E : Type u} [Field K] [Fintype V]
25 
26 def freeGrammar (s t : E → V) : Grammar K V E where
27   source := s
28   target := t
29   equations := fun _ _ => False
30 
31 /-- The finite-vertex path algebra, in its standard generators-and-relations presentation. -/
32 abbrev PathAlgebra (s t : E → V) := Algebra (freeGrammar (K := K) s t)
33 
34 variable (s t : E → V)
35 variable (I : TwoSidedIdeal (PathAlgebra (K := K) s t))
36 
37 /-- All representatives of ideal relations are imposed in the free presentation. -/
38 def idealGrammar : Grammar K V E where
39   source := s
40   target := t
41   equations x y := I.ringCon (quotient (freeGrammar s t) x) (quotient (freeGrammar s t) y)
42 
43 abbrev IdealQuotient := RingQuot (fun x y : PathAlgebra (K := K) s t => I.ringCon x y)
44 
45 def idealQuotientMap : PathAlgebra (K := K) s t →ₐ[K] IdealQuotient s t I :=
46   RingQuot.mkAlgHom K _
47 
48 def freeToIdeal : Free K V E →ₐ[K] IdealQuotient s t I :=
49   (idealQuotientMap s t I).comp (quotient (freeGrammar s t))
50 
51 theorem freeToIdeal_respects {x y : Free K V E} (h : Relation (idealGrammar s t I) x y) :
52     freeToIdeal s t I x = freeToIdeal s t I y := by
53   cases h with
54   | vertex_idempotent v =>
55       exact congrArg (idealQuotientMap s t I)
56         (RingQuot.mkAlgHom_rel K (Relation.vertex_idempotent (G := freeGrammar s t) v))
57   | vertex_orthogonal v w h =>
58       exact congrArg (idealQuotientMap s t I)
59         (RingQuot.mkAlgHom_rel K (Relation.vertex_orthogonal (G := freeGrammar s t) v w h))
60   | vertex_complete =>
61       exact congrArg (idealQuotientMap s t I)
62         (RingQuot.mkAlgHom_rel K (Relation.vertex_complete (G := freeGrammar s t)))
63   | arrow_corner a =>
64       exact congrArg (idealQuotientMap s t I)
65         (RingQuot.mkAlgHom_rel K (Relation.arrow_corner (G := freeGrammar s t) a))
66   | declared h =>
67       exact RingQuot.mkAlgHom_rel K (s := fun x y : PathAlgebra (K := K) s t => I.ringCon x y) h
68 
69 def presentedToIdeal : Algebra (idealGrammar s t I) →ₐ[K] IdealQuotient s t I :=
70   RingQuot.liftAlgHom K ⟨freeToIdeal s t I, fun _ _ h => freeToIdeal_respects s t I h⟩
71 
72 @[simp] theorem presentedToIdeal_quotient (x : Free K V E) :
73     presentedToIdeal s t I (quotient (idealGrammar s t I) x) = freeToIdeal s t I x :=
74   RingQuot.liftAlgHom_mkAlgHom_apply K _ _ x
75 
76 theorem base_respects {x y : Free K V E} (h : Relation (freeGrammar s t) x y) :
77     quotient (idealGrammar s t I) x = quotient (idealGrammar s t I) y := by
78   apply RingQuot.mkAlgHom_rel
79   cases h with
80   | vertex_idempotent v => exact Relation.vertex_idempotent v
81   | vertex_orthogonal v w h => exact Relation.vertex_orthogonal v w h
82   | vertex_complete => exact Relation.vertex_complete
83   | arrow_corner a => exact Relation.arrow_corner a
84   | declared h => exact h.elim
85 
86 def baseToPresented : PathAlgebra (K := K) s t →ₐ[K] Algebra (idealGrammar s t I) :=
87   RingQuot.liftAlgHom K ⟨quotient (idealGrammar s t I), fun _ _ h => base_respects s t I h⟩
88 
89 @[simp] theorem baseToPresented_quotient (x : Free K V E) :
90     baseToPresented s t I (quotient (freeGrammar s t) x) = quotient (idealGrammar s t I) x :=
91   RingQuot.liftAlgHom_mkAlgHom_apply K _ _ x
92 
93 theorem baseToPresented_respects {x y : PathAlgebra (K := K) s t} (h : I.ringCon x y) :
94     baseToPresented s t I x = baseToPresented s t I y := by
95   obtain ⟨x, rfl⟩ := RingQuot.mkAlgHom_surjective K (Relation (freeGrammar s t)) x
96   obtain ⟨y, rfl⟩ := RingQuot.mkAlgHom_surjective K (Relation (freeGrammar s t)) y
97   change baseToPresented s t I (quotient (freeGrammar s t) x) =
98     baseToPresented s t I (quotient (freeGrammar s t) y)
99   rw [baseToPresented_quotient, baseToPresented_quotient]
100   exact declared_relation (idealGrammar s t I) h
101 
102 def idealToPresented : IdealQuotient s t I →ₐ[K] Algebra (idealGrammar s t I) :=
103   RingQuot.liftAlgHom K ⟨baseToPresented s t I, fun _ _ h => baseToPresented_respects s t I h⟩
104 
105 @[simp] theorem idealToPresented_quotient (x : PathAlgebra (K := K) s t) :
106     idealToPresented s t I (idealQuotientMap s t I x) = baseToPresented s t I x :=
107   RingQuot.liftAlgHom_mkAlgHom_apply K _ _ x
108 
109 /-- The iterated quotient and the single generator presentation are actually isomorphic. -/
110 def idealPresentationEquiv : Algebra (idealGrammar s t I) ≃ₐ[K] IdealQuotient s t I :=
111   AlgEquiv.ofAlgHom (presentedToIdeal s t I) (idealToPresented s t I)
112     (by
113       apply RingQuot.ringQuot_ext'
114       apply RingQuot.ringQuot_ext'
115       apply AlgHom.ext
116       intro x
117       change presentedToIdeal s t I
118         (idealToPresented s t I (idealQuotientMap s t I (quotient (freeGrammar s t) x))) =
119         idealQuotientMap s t I (quotient (freeGrammar s t) x)
120       rw [idealToPresented_quotient, baseToPresented_quotient, presentedToIdeal_quotient]
121       rfl)
122     (by
123       apply RingQuot.ringQuot_ext'
124       apply AlgHom.ext
125       intro x
126       change idealToPresented s t I (presentedToIdeal s t I (quotient (idealGrammar s t I) x)) =
127         quotient (idealGrammar s t I) x
128       rw [presentedToIdeal_quotient]
129       change idealToPresented s t I (idealQuotientMap s t I (quotient (freeGrammar s t) x)) = _
130       rw [idealToPresented_quotient, baseToPresented_quotient])
131 
132 /-- The manuscript's actual quotient by a two-sided ideal, with a genuine module category target. -/
133 def typedIdealModuleEquivalence :
134     TypedRealization (G := idealGrammar s t I) ≌ ModuleCat.{u} (IdealQuotient s t I) :=
135   typedModuleEquivalence.trans
136     (ModuleCat.restrictScalarsEquivalenceOfRingEquiv (idealPresentationEquiv s t I).symm.toRingEquiv)
137 
138 end Komorebi.PaperIRelease.GrammarAlgebra

Back to source controls