Documentation

Mathlib.Topology.Category.LightProfinite.Injective

Injectivity of light profinite spaces #

This file establishes that non-empty light profinite sets are injective in the category of profinite sets, and thus also in the category of light profinite sets. This is used in the proof that the null sequence module is internally projective in light condensed abelian groups.

Main results #

The main result is Profinite.injective_of_light, which provides an instance of Injective (lightToProfinite.obj S) for a non-empty light profinite set S. We deduce the instance LightProfinite.injective that every light profinite set is an injective object in the category LightProfinite. The proof uses an inductive extension argument along a presentation of S as sequential limit of finite discrete spaces. The key lemma is exists_lift_of_finite_of_mono_of_epi.

References #

source
theorem Profinite.exists_lift_of_finite_of_injective_of_surjective {X : Type u_1} {Y : Type u_2} {S : Type u_3} {T : Type u_4} [TopologicalSpace X] [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [T2Space Y] [TotallyDisconnectedSpace Y] [TopologicalSpace S] [T2Space S] [Finite S] [TopologicalSpace T] [T2Space T] (f : X → Y) (hf : Continuous f) (f_inj : Function.Injective f) (f' : S → T) (f'_surj : Function.Surjective f') (g : X → S) (hg : Continuous g) (g' : Y → T) (hg' : Continuous g') (h_comm : g' ∘ f = f' ∘ g) :
∃ (k : Y → S), Continuous k ∧ f' ∘ k = g' ∧ k ∘ f = g

This is the key statement for the inductive proof of injectivity of light profinite spaces. Given a commutative square

X >-f->  Y
|g       |g'
v        v
S -f'->> T

where Y is profinite, S is finite, f is injective and f' is surjective, there exists a diagonal map k : Y → S making the diagram commute.

source
theorem Profinite.exists_lift_of_finite_of_mono_of_epi {X Y S T : Profinite} [Finite ↑S.toTop] (f : X ⟶ Y) [CategoryTheory.Mono f] (f' : S ⟶ T) [CategoryTheory.Epi f'] (g : X ⟶ S) (g' : Y ⟶ T) (h_comm : CategoryTheory.CategoryStruct.comp f g' = CategoryTheory.CategoryStruct.comp g f') :
∃ (k : Y ⟶ S), CategoryTheory.CategoryStruct.comp k f' = g' ∧ CategoryTheory.CategoryStruct.comp f k = g

A categorically stated version of exists_lift_of_finite_of_injective_of_surjective in the category Profinite.

source
instance Profinite.injective_of_finite (S : Profinite) [Nonempty ↑S.toTop] [Finite ↑S.toTop] :
CategoryTheory.Injective S

Finite sets are injective objects in Profinite.

source
instance Profinite.injective_of_light (S : LightProfinite) [Nonempty ↑S.toTop] :
CategoryTheory.Injective (lightToProfinite.obj S)

A nonempty light profinite space is injective in Profinite.

source
instance LightProfinite.injective (S : LightProfinite) [Nonempty ↑S.toTop] :
CategoryTheory.Injective S