AdditiveCocycleBridge.lean

1 import KomorebiSpace.NonabelianExtensionFibers
2 import KomorebiSpace.SectionObstruction
3 import Mathlib.Algebra.Group.TypeTags.Hom
4 
5 set_option autoImplicit false
6 
7 /-!
8 # The additive extension obstruction is recovered by the nonabelian model
9 
10 This bridge uses the actual earlier view system and section types. It compares
11 vanishing criteria, not the entire abelian quotient with a group on a general
12 nonabelian orbit set.
13 -/
14 universe u v w
15 namespace KomorebiSpace
16 open CategoryTheory
17 namespace AdditiveViewSystem
18 variable {V : Type u} [Category.{v} V]
19 variable {A : V → Type w} [∀ a, AddCommGroup (A a)]
20 variable (F : AdditiveViewSystem V A)
21 
22 /-- The same restriction maps with multiplicative type tags. -/
23 def multiplicativeViews : GroupViewSystem V (fun v => Multiplicative (A v)) where
24   pull := fun f => (F.pull f).toMultiplicative
25   pull_id := by intro v x; exact congrArg Multiplicative.ofAdd (F.pull_id v x.toAdd)
26   pull_comp := by intro v w z f g x; exact congrArg Multiplicative.ofAdd (F.pull_comp f g x.toAdd)
27 
28 /-- Trivial cocycles recover the previous coherent additive sections. -/
29 def multiplicativeAmbientEquiv : F.views.Ambient ≃
30     (F.multiplicativeViews.twistedViews F.multiplicativeViews.trivial).Ambient where
31   toFun x := ⟨fun v => Multiplicative.ofAdd (x.val v), by
32     intro v w f
33     change 1 * Multiplicative.ofAdd (F.pull f (x.val w)) = Multiplicative.ofAdd (x.val v)
34     rw [one_mul]
35     exact congrArg Multiplicative.ofAdd (x.property v w f)⟩
36   invFun x := ⟨fun v => (x.val v).toAdd, by
37     intro v w f
38     have he := x.property v w f
39     change 1 * Multiplicative.ofAdd (F.pull f (x.val w).toAdd) = x.val v at he
40     rw [one_mul] at he
41     exact congrArg Multiplicative.toAdd he⟩
42   left_inv _ := rfl
43   right_inv _ := rfl
44 
45 def multiplicativePartial (U : Set V) (s : F.views.Partial U) :
46     (F.multiplicativeViews.twistedViews F.multiplicativeViews.trivial).Partial U :=
47   ⟨fun v => Multiplicative.ofAdd (s.val v), by
48     intro v w f
49     change 1 * Multiplicative.ofAdd (F.pull f (s.val w)) = Multiplicative.ofAdd (s.val v)
50     rw [one_mul]
51     exact congrArg Multiplicative.ofAdd (s.property v w f)⟩
52 
53 def multiplicativeExtensionsEquiv (U : Set V) (s : F.views.Partial U) :
54     F.views.Extensions U s ≃
55     (F.multiplicativeViews.twistedViews F.multiplicativeViews.trivial).Extensions U
56       (F.multiplicativePartial U s) where
57   toFun x := ⟨F.multiplicativeAmbientEquiv x.val, by
58     apply ViewSystem.Partial.ext
59     intro v
60     change Multiplicative.ofAdd (x.val.val v.val) = Multiplicative.ofAdd (s.val v)
61     exact congrArg Multiplicative.ofAdd
62       (congrArg (fun t : F.views.Partial U => t.val v) x.property)⟩
63   invFun x := ⟨F.multiplicativeAmbientEquiv.symm x.val, by
64     apply ViewSystem.Partial.ext
65     intro v
66     have he := congrArg
67       (fun t : (F.multiplicativeViews.twistedViews F.multiplicativeViews.trivial).Partial U => t.val v)
68       x.property
69     exact congrArg Multiplicative.toAdd he⟩
70   left_inv _ := rfl
71   right_inv _ := rfl
72 
73 /-- The normalized multiplicative edge is exactly the old additive differential. -/
74 theorem normalization_is_additive_defect (q : ∀ v, A v) {v w : V} (f : v ⟶ w) :
75     ((F.multiplicativeViews.normalize F.multiplicativeViews.trivial
76       (fun a => Multiplicative.ofAdd (q a))).edge f).toAdd = F.differential q v w f := by
77   rw [GroupViewSystem.normalize_edge]
78   change -q v + 0 + F.pull f (q w) = F.pull f (q w) - q v
79   abel
80 
81 /-- Neutrality in the orbit model agrees with vanishing of the original quotient obstruction. -/
82 theorem orbit_neutral_iff_additive_zero (U : Set V) (s : F.views.Partial U) :
83     F.multiplicativeViews.extensionOrbit F.multiplicativeViews.trivial U
84       (F.multiplicativePartial U s) = F.multiplicativeViews.neutralClass U ↔
85       F.extensionClass U s = 0 := by
86   rw [GroupViewSystem.extensionOrbit_neutral_iff, F.extensionClass_zero_iff]
87   constructor
88   · rintro ⟨x⟩; exact ⟨(F.multiplicativeExtensionsEquiv U s).symm x⟩
89   · rintro ⟨x⟩; exact ⟨F.multiplicativeExtensionsEquiv U s x⟩
90 
91 end AdditiveViewSystem
92 end KomorebiSpace

Back to source controls