AtomicMultiset.lean

1 import Mathlib.Data.Multiset.Sort
2 import Mathlib.Algebra.BigOperators.Group.Multiset.Basic
3 import Mathlib.Data.Quot
4 import Mathlib.Tactic
5 
6 /-! The block-multiset part of Paper XI, Theorem 2.5.
7 An atom is an isomorphism class. A block retains its strictly positive monodromy
8 length. Mapping atoms does not discard lengths, multiplicities, or repetitions.
9 This module contains no local-Weil or Langlands-classification existence axiom. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.AtomicMultiset
13 
14 @[ext] structure Block (A : Type*) where
15   atom : A
16   length : ℕ
17   length_pos : 0 < length
18 
19 variable {A B C : Type*}
20 
21 def blockMap (f : A → B) (b : Block A) : Block B :=
22   ⟨f b.atom, b.length, b.length_pos⟩
23 
24 @[simp] theorem blockMap_atom (f : A → B) (b : Block A) :
25     (blockMap f b).atom = f b.atom := rfl
26 
27 @[simp] theorem blockMap_length (f : A → B) (b : Block A) :
28     (blockMap f b).length = b.length := rfl
29 
30 @[simp] theorem blockMap_id (b : Block A) : blockMap id b = b := by
31   cases b; rfl
32 
33 @[simp] theorem blockMap_comp (g : B → C) (f : A → B) (b : Block A) :
34     blockMap g (blockMap f b) = blockMap (g ∘ f) b := rfl
35 
36 def extend (f : A → B) : Multiset (Block A) →+ Multiset (Block B) where
37   toFun s := s.map (blockMap f)
38   map_zero' := Multiset.map_zero _
39   map_add' := Multiset.map_add _
40 
41 @[simp] theorem extend_singleton (f : A → B) (b : Block A) :
42     extend f {b} = {blockMap f b} := rfl
43 
44 @[simp] theorem extend_cons (f : A → B) (b : Block A) (s : Multiset (Block A)) :
45     extend f (b ::ₘ s) = blockMap f b ::ₘ extend f s := Multiset.map_cons _ _ _
46 
47 @[simp] theorem extend_card (f : A → B) (s : Multiset (Block A)) :
48     (extend f s).card = s.card := Multiset.card_map _ _
49 
50 @[simp] theorem extend_id (s : Multiset (Block A)) : extend id s = s := by
51   change s.map (blockMap id) = s
52   simp only [show blockMap (id : A → A) = id from funext blockMap_id, Multiset.map_id]
53 
54 @[simp] theorem extend_comp (g : B → C) (f : A → B) (s : Multiset (Block A)) :
55     extend g (extend f s) = extend (g ∘ f) s := by
56   exact Multiset.map_map _ _ _
57 
58 /-- There is only one additive extension with the declared value on every block. -/
59 theorem extend_unique (f : A → B) (F : Multiset (Block A) →+ Multiset (Block B))
60     (hF : ∀ b, F {b} = {blockMap f b}) : F = extend f := by
61   apply DFunLike.ext
62   intro s
63   induction s using Multiset.induction_on with
64   | empty => simp
65   | @cons b s ih =>
66       have hs : b ::ₘ s = ({b} : Multiset (Block A)) + s := rfl
67       rw [hs, map_add, map_add, hF, ih, extend_singleton]
68 
69 /-- Equal-sized repeated atoms cannot be lost if the atomic assignment is injective. -/
70 theorem extend_injective (f : A → B) (hf : Function.Injective f) :
71     Function.Injective (extend f) := by
72   apply Multiset.map_injective
73   intro b c h
74   apply Block.ext
75   · apply hf
76     exact congrArg Block.atom h
77   · exact congrArg (fun x : Block B => x.length) h
78 
79 /-- An inverse atomic assignment gives an inverse on all finite block multisets. -/
80 def extendEquiv (e : A ≃ B) : Multiset (Block A) ≃+ Multiset (Block B) where
81   toFun := extend e
82   invFun := extend e.symm
83   left_inv s := by
84     rw [extend_comp]
85     have h : (e.symm ∘ e : A → A) = id := by funext a; exact e.symm_apply_apply a
86     rw [h, extend_id]
87   right_inv s := by
88     rw [extend_comp]
89     have h : (e ∘ e.symm : B → B) = id := by funext a; exact e.apply_symm_apply a
90     rw [h, extend_id]
91   map_add' := (extend e).map_add
92 
93 /-- Weighted total dimension: the chain length multiplies the atom dimension. -/
94 def dimension (dim : A → ℕ) (s : Multiset (Block A)) : ℕ :=
95   (s.map (fun b => b.length * dim b.atom)).sum
96 
97 theorem dimension_extend (f : A → B) (dA : A → ℕ) (dB : B → ℕ)
98     (hdim : ∀ a, dB (f a) = dA a) (s : Multiset (Block A)) :
99     dimension dB (extend f s) = dimension dA s := by
100   simp only [dimension, extend, AddMonoidHom.coe_mk, ZeroHom.coe_mk, Multiset.map_map]
101   congr 1
102   apply Multiset.map_congr rfl
103   intro b _
104   exact congrArg (b.length * ·) (hdim b.atom)
105 
106 /-- The atom map descends along the given isomorphism relations. -/
107 def descend {sA : Setoid A} {sB : Setoid B} (f : A → B)
108     (hf : ∀ a a', sA.r a a' → sB.r (f a) (f a')) :
109     Quotient sA → Quotient sB := Quotient.map f hf
110 
111 @[simp] theorem descend_mk {sA : Setoid A} {sB : Setoid B} (f : A → B)
112     (hf : ∀ a a', sA.r a a' → sB.r (f a) (f a')) (a : A) :
113     descend f hf (Quotient.mk sA a) = Quotient.mk sB (f a) := rfl
114 
115 /-- Atomwise twisting commutes with block assembly when it commutes on atoms. -/
116 theorem extend_natural (f : A → B) (tA : A → A) (tB : B → B)
117     (hf : ∀ a, f (tA a) = tB (f a)) (s : Multiset (Block A)) :
118     extend f (extend tA s) = extend tB (extend f s) := by
119   rw [extend_comp, extend_comp]
120   rw [show f ∘ tA = tB ∘ f from funext hf]
121 
122 end PaperXI.AtomicMultiset

Back to source controls