FiniteTargets.lean

1 import RealizationBoundaries.ProductTopology
2 
3 /-!
4 # All finite targets extend uniquely to the ambient product
5 
6 The extension is built from the actual integer quotient. Continuity is a theorem,
7 not a condition imposed on the original abstract homomorphism.
8 -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace RealizationBoundaries
12 
13 variable (W : Submodule ℚ TailSpace)
14 variable (F : Type*) [AddGroup F] [Finite F]
15 
16 theorem finite_target_kills_ncard (f : preimage W →+ F) :
17     multiples W (Nat.card F) ≤ f.ker := by
18   let : Fintype F := Fintype.ofFinite F
19   simpa only [Nat.card_eq_fintype_card] using finite_target_kills_multiples W F f
20 
21 /-- The finite factor obtained from the exact quotient equivalence. -/
22 def finiteTargetFactor (f : preimage W →+ F) : DivisorCoordinates (Nat.card F) →+ F :=
23   (QuotientAddGroup.lift (multiples W (Nat.card F)) f (finite_target_kills_ncard W F f)).comp
24     (integerQuotientEquiv W (Nat.card_pos)).symm.toAddMonoidHom
25 
26 @[simp] theorem finiteTargetFactor_coordinate (f : preimage W →+ F) (x : preimage W) :
27     finiteTargetFactor W F f (coordinateMap W (Nat.card F) x) = f x := by
28   change (QuotientAddGroup.lift (multiples W (Nat.card F)) f (finite_target_kills_ncard W F f))
29     ((integerQuotientEquiv W Nat.card_pos).symm (coordinateMap W (Nat.card F) x)) = f x
30   have hi : (integerQuotientEquiv W Nat.card_pos).symm (coordinateMap W (Nat.card F) x) =
31       QuotientAddGroup.mk x := by
32     apply (integerQuotientEquiv W Nat.card_pos).injective
33     rw [AddEquiv.apply_symm_apply]
34     exact (integerQuotientEquiv_mk W Nat.card_pos x).symm
35   rw [hi]
36   rfl
37 
38 /-- A finite-target map on H_W extends to the same fixed infinite product P. -/
39 def finiteTargetExtension (f : preimage W →+ F) : Ambient →+ F :=
40   (finiteTargetFactor W F f).comp (ambientCoordinates (Nat.card F))
41 
42 @[simp] theorem finiteTargetExtension_subtype (f : preimage W →+ F) (x : preimage W) :
43     finiteTargetExtension W F f x.val = f x :=
44   finiteTargetFactor_coordinate W F f x
45 
46 /-- The extension factors through finitely many discrete coordinates. -/
47 theorem finiteTargetExtension_continuous [TopologicalSpace F] (f : preimage W →+ F) :
48     Continuous (finiteTargetExtension W F f) := by
49   let := divisorCoordinates_discrete (m := Nat.card F) Nat.card_pos
50   exact (continuous_of_discreteTopology : Continuous (finiteTargetFactor W F f)).comp
51     (ambientCoordinates_continuous (Nat.card F))
52 
53 /-- Continuity of every abstract finite-target homomorphism in the induced topology. -/
54 theorem finiteTarget_continuous [TopologicalSpace F] (f : preimage W →+ F) : Continuous f := by
55   have h := (finiteTargetExtension_continuous W F f).comp
56     (continuous_subtype_val : Continuous (fun x : preimage W => x.val))
57   simpa only [Function.comp_def, finiteTargetExtension_subtype] using h
58 
59 /-- Uniqueness is with respect to continuous ambient maps, as required by completion. -/
60 theorem finiteTargetExtension_unique [TopologicalSpace F] [T2Space F]
61     (f : preimage W →+ F) (g : Ambient →+ F) (hg : Continuous g)
62     (heq : ∀ x : preimage W, g x.val = f x) : g = finiteTargetExtension W F f := by
63   apply DFunLike.ext'
64   apply (preimage_denseRange W).equalizer hg (finiteTargetExtension_continuous W F f)
65   funext x
66   exact (heq x).trans (finiteTargetExtension_subtype W F f x).symm
67 
68 /-- Extension commutes with every homomorphism of finite target groups. -/
69 theorem finiteTargetExtension_natural (E : Type*) [AddGroup E] [Finite E]
70     (f : preimage W →+ F) (g : F →+ E) :
71     finiteTargetExtension W E (g.comp f) = g.comp (finiteTargetExtension W F f) := by
72   let : TopologicalSpace F := ⊥
73   let : DiscreteTopology F := ⟨rfl⟩
74   let : TopologicalSpace E := ⊥
75   let : DiscreteTopology E := ⟨rfl⟩
76   symm
77   apply finiteTargetExtension_unique W E
78   · exact (continuous_of_discreteTopology : Continuous g).comp
79       (finiteTargetExtension_continuous W F f)
80   · intro x
81     simp
82 
83 /-- Precise finite-target universal property, without identifying unequal Hom types. -/
84 def finiteTargetHomEquiv [TopologicalSpace F] [DiscreteTopology F] :
85     (Ambient →ₜ+ F) ≃ (preimage W →+ F) where
86   toFun g := g.toAddMonoidHom.comp (preimage W).subtype
87   invFun f := { toAddMonoidHom := finiteTargetExtension W F f,
88                 continuous_toFun := finiteTargetExtension_continuous W F f }
89   left_inv g := by
90     apply ContinuousAddMonoidHom.ext
91     intro x
92     exact DFunLike.congr_fun (finiteTargetExtension_unique W F
93       (g.toAddMonoidHom.comp (preimage W).subtype) g.toAddMonoidHom g.continuous_toFun
94       (fun _ => rfl)).symm x
95   right_inv f := by
96     ext x
97     exact finiteTargetExtension_subtype W F f x
98 
99 end RealizationBoundaries

Back to source controls