|
| 1 | +/- |
| 2 | +Copyright (c) 2024 Dagur Asgeirsson. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Dagur Asgeirsson |
| 5 | +-/ |
| 6 | +import Mathlib.Topology.Category.LightProfinite.IsLight |
| 7 | +import Mathlib.Topology.Category.Profinite.Limits |
| 8 | +/-! |
| 9 | +
|
| 10 | +# Explicit limits and colimits |
| 11 | +
|
| 12 | +This file collects some constructions of explicit limits and colimits in `LightProfinite`, |
| 13 | +which may be useful due to their definitional properties. |
| 14 | +
|
| 15 | +## Main definitions |
| 16 | +
|
| 17 | +* `LightProfinite.pullback`: Explicit pullback, defined in the "usual" way as a subset of the |
| 18 | + product. |
| 19 | +
|
| 20 | +* `LightProfinite.finiteCoproduct`: Explicit finite coproducts, defined as a disjoint union. |
| 21 | +
|
| 22 | +-/ |
| 23 | + |
| 24 | +universe u w |
| 25 | + |
| 26 | +open CategoryTheory Profinite TopologicalSpace Limits |
| 27 | + |
| 28 | +namespace LightProfinite |
| 29 | + |
| 30 | +section Pullback |
| 31 | + |
| 32 | +instance {X Y B : Profinite.{u}} (f : X ⟶ B) (g : Y ⟶ B) [X.IsLight] [Y.IsLight] : |
| 33 | + (Profinite.pullback f g).IsLight := by |
| 34 | + let i : Profinite.pullback f g ⟶ Profinite.of (X × Y) := ⟨fun x ↦ x.val, continuous_induced_dom⟩ |
| 35 | + have : Mono i := by |
| 36 | + rw [Profinite.mono_iff_injective] |
| 37 | + exact Subtype.val_injective |
| 38 | + exact isLight_of_mono i |
| 39 | + |
| 40 | +variable {X Y B : LightProfinite.{u}} (f : X ⟶ B) (g : Y ⟶ B) |
| 41 | + |
| 42 | +/-- |
| 43 | +The "explicit" pullback of two morphisms `f, g` in `LightProfinite`, whose underlying profinite set |
| 44 | +is the set of pairs `(x, y)` such that `f x = g y`, with the topology induced by the product. |
| 45 | +-/ |
| 46 | +noncomputable def pullback : LightProfinite.{u} := |
| 47 | + ofIsLight (Profinite.pullback (lightToProfinite.map f) (lightToProfinite.map g)) |
| 48 | + |
| 49 | +/-- The projection from the pullback to the first component. -/ |
| 50 | +def pullback.fst : pullback f g ⟶ X where |
| 51 | + toFun := fun ⟨⟨x, _⟩, _⟩ ↦ x |
| 52 | + continuous_toFun := Continuous.comp continuous_fst continuous_subtype_val |
| 53 | + |
| 54 | +/-- The projection from the pullback to the second component. -/ |
| 55 | +def pullback.snd : pullback f g ⟶ Y where |
| 56 | + toFun := fun ⟨⟨_, y⟩, _⟩ ↦ y |
| 57 | + continuous_toFun := Continuous.comp continuous_snd continuous_subtype_val |
| 58 | + |
| 59 | +@[reassoc] |
| 60 | +lemma pullback.condition : pullback.fst f g ≫ f = pullback.snd f g ≫ g := by |
| 61 | + ext ⟨_, h⟩ |
| 62 | + exact h |
| 63 | + |
| 64 | +/-- |
| 65 | +Construct a morphism to the explicit pullback given morphisms to the factors |
| 66 | +which are compatible with the maps to the base. |
| 67 | +This is essentially the universal property of the pullback. |
| 68 | +-/ |
| 69 | +def pullback.lift {Z : LightProfinite.{u}} (a : Z ⟶ X) (b : Z ⟶ Y) (w : a ≫ f = b ≫ g) : |
| 70 | + Z ⟶ pullback f g where |
| 71 | + toFun := fun z ↦ ⟨⟨a z, b z⟩, by apply_fun (· z) at w; exact w⟩ |
| 72 | + continuous_toFun := by |
| 73 | + apply Continuous.subtype_mk |
| 74 | + rw [continuous_prod_mk] |
| 75 | + exact ⟨a.continuous, b.continuous⟩ |
| 76 | + |
| 77 | +@[reassoc (attr := simp)] |
| 78 | +lemma pullback.lift_fst {Z : LightProfinite.{u}} (a : Z ⟶ X) (b : Z ⟶ Y) (w : a ≫ f = b ≫ g) : |
| 79 | + pullback.lift f g a b w ≫ pullback.fst f g = a := rfl |
| 80 | + |
| 81 | +@[reassoc (attr := simp)] |
| 82 | +lemma pullback.lift_snd {Z : LightProfinite.{u}} (a : Z ⟶ X) (b : Z ⟶ Y) (w : a ≫ f = b ≫ g) : |
| 83 | + pullback.lift f g a b w ≫ pullback.snd f g = b := rfl |
| 84 | + |
| 85 | +lemma pullback.hom_ext {Z : LightProfinite.{u}} (a b : Z ⟶ pullback f g) |
| 86 | + (hfst : a ≫ pullback.fst f g = b ≫ pullback.fst f g) |
| 87 | + (hsnd : a ≫ pullback.snd f g = b ≫ pullback.snd f g) : a = b := by |
| 88 | + ext z |
| 89 | + apply_fun (· z) at hfst hsnd |
| 90 | + apply Subtype.ext |
| 91 | + apply Prod.ext |
| 92 | + · exact hfst |
| 93 | + · exact hsnd |
| 94 | + |
| 95 | +/-- The pullback cone whose cone point is the explicit pullback. -/ |
| 96 | +@[simps! pt π] |
| 97 | +noncomputable def pullback.cone : Limits.PullbackCone f g := |
| 98 | + Limits.PullbackCone.mk (pullback.fst f g) (pullback.snd f g) (pullback.condition f g) |
| 99 | + |
| 100 | +/-- The explicit pullback cone is a limit cone. -/ |
| 101 | +@[simps! lift] |
| 102 | +def pullback.isLimit : Limits.IsLimit (pullback.cone f g) := |
| 103 | + Limits.PullbackCone.isLimitAux _ |
| 104 | + (fun s ↦ pullback.lift f g s.fst s.snd s.condition) |
| 105 | + (fun _ ↦ pullback.lift_fst _ _ _ _ _) |
| 106 | + (fun _ ↦ pullback.lift_snd _ _ _ _ _) |
| 107 | + (fun _ _ hm ↦ pullback.hom_ext _ _ _ _ (hm .left) (hm .right)) |
| 108 | + |
| 109 | +end Pullback |
| 110 | + |
| 111 | +section FiniteCoproduct |
| 112 | + |
| 113 | +instance {α : Type w} [Finite α] (X : α → Profinite.{max u w}) [∀ a, (X a).IsLight] : |
| 114 | + (Profinite.finiteCoproduct X).IsLight where |
| 115 | + countable_clopens := by |
| 116 | + refine @Function.Surjective.countable ((a : α) → Clopens (X a)) _ inferInstance |
| 117 | + (fun f ↦ ⟨⋃ (a : α), Sigma.mk a '' (f a).1, ?_⟩) ?_ |
| 118 | + · apply isClopen_iUnion_of_finite |
| 119 | + intro i |
| 120 | + exact ⟨isClosedMap_sigmaMk _ (f i).2.1, isOpenMap_sigmaMk _ (f i).2.2⟩ |
| 121 | + · intro ⟨s, ⟨hsc, hso⟩⟩ |
| 122 | + rw [isOpen_sigma_iff] at hso |
| 123 | + rw [isClosed_sigma_iff] at hsc |
| 124 | + refine ⟨fun i ↦ ⟨_, ⟨hsc i, hso i⟩⟩, ?_⟩ |
| 125 | + simp only [Subtype.mk.injEq] |
| 126 | + ext ⟨i, xi⟩ |
| 127 | + refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩ |
| 128 | + · simp only [Clopens.coe_mk, Set.mem_iUnion] at hx |
| 129 | + obtain ⟨_, _, hj, hxj⟩ := hx |
| 130 | + simpa [hxj] using hj |
| 131 | + · simp only [Clopens.coe_mk, Set.mem_iUnion] |
| 132 | + refine ⟨i, xi, (by simpa using hx), rfl⟩ |
| 133 | + |
| 134 | +variable {α : Type w} [Finite α] (X : α → LightProfinite.{max u w}) |
| 135 | + |
| 136 | +/-- |
| 137 | +The "explicit" coproduct of a finite family of objects in `LightProfinite`, whose underlying |
| 138 | +profinite set is the disjoint union with its usual topology. |
| 139 | +-/ |
| 140 | +noncomputable |
| 141 | +def finiteCoproduct : LightProfinite := |
| 142 | + ofIsLight (Profinite.finiteCoproduct.{u, w} fun a ↦ (X a).toProfinite) |
| 143 | + |
| 144 | +/-- The inclusion of one of the factors into the explicit finite coproduct. -/ |
| 145 | +def finiteCoproduct.ι (a : α) : X a ⟶ finiteCoproduct X where |
| 146 | + toFun := (⟨a, ·⟩) |
| 147 | + continuous_toFun := continuous_sigmaMk (σ := fun a ↦ (X a).toProfinite) |
| 148 | + |
| 149 | +/-- |
| 150 | +To construct a morphism from the explicit finite coproduct, it suffices to |
| 151 | +specify a morphism from each of its factors. This is the universal property of the coproduct. |
| 152 | +-/ |
| 153 | +def finiteCoproduct.desc {B : LightProfinite.{max u w}} (e : (a : α) → (X a ⟶ B)) : |
| 154 | + finiteCoproduct X ⟶ B where |
| 155 | + toFun := fun ⟨a, x⟩ ↦ e a x |
| 156 | + continuous_toFun := by |
| 157 | + apply continuous_sigma |
| 158 | + intro a |
| 159 | + exact (e a).continuous |
| 160 | + |
| 161 | +@[reassoc (attr := simp)] |
| 162 | +lemma finiteCoproduct.ι_desc {B : LightProfinite.{max u w}} (e : (a : α) → (X a ⟶ B)) (a : α) : |
| 163 | + finiteCoproduct.ι X a ≫ finiteCoproduct.desc X e = e a := rfl |
| 164 | + |
| 165 | +lemma finiteCoproduct.hom_ext {B : LightProfinite.{max u w}} (f g : finiteCoproduct X ⟶ B) |
| 166 | + (h : ∀ a : α, finiteCoproduct.ι X a ≫ f = finiteCoproduct.ι X a ≫ g) : f = g := by |
| 167 | + ext ⟨a, x⟩ |
| 168 | + specialize h a |
| 169 | + apply_fun (· x) at h |
| 170 | + exact h |
| 171 | + |
| 172 | +/-- The coproduct cocone associated to the explicit finite coproduct. -/ |
| 173 | +noncomputable abbrev finiteCoproduct.cofan : Limits.Cofan X := |
| 174 | + Cofan.mk (finiteCoproduct X) (finiteCoproduct.ι X) |
| 175 | + |
| 176 | +/-- The explicit finite coproduct cocone is a colimit cocone. -/ |
| 177 | +def finiteCoproduct.isColimit : Limits.IsColimit (finiteCoproduct.cofan X) := |
| 178 | + mkCofanColimit _ |
| 179 | + (fun s ↦ desc _ fun a ↦ s.inj a) |
| 180 | + (fun s a ↦ ι_desc _ _ _) |
| 181 | + fun s m hm ↦ finiteCoproduct.hom_ext _ _ _ fun a ↦ |
| 182 | + (by ext t; exact congrFun (congrArg DFunLike.coe (hm a)) t) |
| 183 | + |
| 184 | +end FiniteCoproduct |
| 185 | + |
| 186 | +section HasPreserves |
| 187 | + |
| 188 | +instance (n : ℕ) (F : Discrete (Fin n) ⥤ LightProfinite) : |
| 189 | + HasColimit (Discrete.functor (F.obj ∘ Discrete.mk) : Discrete (Fin n) ⥤ LightProfinite) where |
| 190 | + exists_colimit := ⟨⟨finiteCoproduct.cofan _, finiteCoproduct.isColimit _⟩⟩ |
| 191 | + |
| 192 | +instance : HasFiniteCoproducts LightProfinite where |
| 193 | + out _ := { has_colimit := fun _ ↦ hasColimitOfIso Discrete.natIsoFunctor } |
| 194 | + |
| 195 | +instance {X Y B : LightProfinite} (f : X ⟶ B) (g : Y ⟶ B) : HasLimit (cospan f g) where |
| 196 | + exists_limit := ⟨⟨pullback.cone f g, pullback.isLimit f g⟩⟩ |
| 197 | + |
| 198 | +instance : HasPullbacks LightProfinite where |
| 199 | + has_limit F := hasLimitOfIso (diagramIsoCospan F).symm |
| 200 | + |
| 201 | +noncomputable |
| 202 | +instance : PreservesFiniteCoproducts lightToProfinite := by |
| 203 | + refine ⟨fun J hJ ↦ ⟨fun {F} ↦ ?_⟩⟩ |
| 204 | + suffices PreservesColimit (Discrete.functor (F.obj ∘ Discrete.mk)) lightToProfinite by |
| 205 | + exact preservesColimitOfIsoDiagram _ Discrete.natIsoFunctor.symm |
| 206 | + apply preservesColimitOfPreservesColimitCocone (finiteCoproduct.isColimit _) |
| 207 | + exact Profinite.finiteCoproduct.isColimit _ |
| 208 | + |
| 209 | +noncomputable |
| 210 | +instance : PreservesLimitsOfShape WalkingCospan lightToProfinite := by |
| 211 | + suffices ∀ {X Y B} (f : X ⟶ B) (g : Y ⟶ B), PreservesLimit (cospan f g) lightToProfinite from |
| 212 | + ⟨fun {F} ↦ preservesLimitOfIsoDiagram _ (diagramIsoCospan F).symm⟩ |
| 213 | + intro _ _ _ f g |
| 214 | + apply preservesLimitOfPreservesLimitCone (pullback.isLimit f g) |
| 215 | + exact (isLimitMapConePullbackConeEquiv lightToProfinite (pullback.condition f g)).symm |
| 216 | + (Profinite.pullback.isLimit _ _) |
| 217 | + |
| 218 | +instance (X : LightProfinite) : Unique (X ⟶ (FintypeCat.of PUnit.{u+1}).toLightProfinite) := |
| 219 | + ⟨⟨⟨fun _ ↦ PUnit.unit, continuous_const⟩⟩, fun _ ↦ rfl⟩ |
| 220 | + |
| 221 | +/-- A one-element space is terminal in `LightProfinite` -/ |
| 222 | +def isTerminalPUnit : IsTerminal ((FintypeCat.of PUnit.{u+1}).toLightProfinite) := |
| 223 | + Limits.IsTerminal.ofUnique _ |
| 224 | + |
| 225 | +instance : HasTerminal LightProfinite.{u} := |
| 226 | + Limits.hasTerminal_of_unique (FintypeCat.of PUnit.{u+1}).toLightProfinite |
| 227 | + |
| 228 | +/-- The isomorphism from an arbitrary terminal object of `LightProfinite` to a one-element space. -/ |
| 229 | +noncomputable def terminalIsoPUnit : |
| 230 | + ⊤_ LightProfinite.{u} ≅ (FintypeCat.of PUnit.{u+1}).toLightProfinite := |
| 231 | + terminalIsTerminal.uniqueUpToIso LightProfinite.isTerminalPUnit |
| 232 | + |
| 233 | +noncomputable instance : PreservesFiniteCoproducts LightProfinite.toTopCat.{u} where |
| 234 | + preserves _ _ := (inferInstance : |
| 235 | + PreservesColimitsOfShape _ (LightProfinite.lightToProfinite.{u} ⋙ Profinite.toTopCat.{u})) |
| 236 | + |
| 237 | +noncomputable instance : PreservesLimitsOfShape WalkingCospan LightProfinite.toTopCat.{u} := |
| 238 | + (inferInstance : PreservesLimitsOfShape WalkingCospan |
| 239 | + (LightProfinite.lightToProfinite.{u} ⋙ Profinite.toTopCat.{u})) |
| 240 | + |
| 241 | +end HasPreserves |
| 242 | + |
| 243 | +end LightProfinite |
0 commit comments