Characterization of internal projectivity in light condensed modules

This file gives an explicit condition on light condensed modules over a ring R to be internally projective, namely the following:

internallyProjective_iff_tensor_condition: P : LightCondMod R is internally projective if and only if, for all A B : LightCondMod R, for all epimorphisms e : A ⟶ B, for all S : LightProfinite and all morphisms g : P ⊗ R[S] ⟶ B, there exists a S' : LightProfinite with a surjeciton π : S' ⟶ S and a morphism g' : P ⊗ R[S'] ⟶ A, making the diagram

P ⊗ R[S'] ⟶ A
  |          |
  v          v
P ⊗ R[S]  ⟶ B

commute.

We also provide the analogous characterization with the tensor product commuted the other way around (see internallyProjective_iff_tensor_condition'), and the special cases when P is the free condensed module on a condensed set (free_internallyProjective_iff_tensor_condition, free_internallyProjective_iff_tensor_condition') and when P is the free condensed module on a light profinite set (free_lightProfinite_internallyProjective_iff_tensor_condition/ free_lightProfinite_internallyProjective_iff_tensor_condition').

noncomputable def LightCondensed.ihomPoints (R : Type u) [CommRing R] (A B : LightCondMod R) (S : LightProfinite) : ↑(((CategoryTheory.ihom A).obj B).val.obj (Opposite.op S)) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorObj A ((free R).obj S.toCondensed) ⟶ B)

The S-valued points of the internal hom A ⟶[LightCondMod R] B are in bijection with morpisms A ⊗ R[S] ⟶ B.

Equations

• One or more equations did not get rendered due to their size.

theorem LightCondensed.ihomPoints_apply (R : Type u) [CommRing R] (A B : LightCondMod R) (S : LightProfinite) (x : ↑(((CategoryTheory.ihom A).obj B).val.obj (Opposite.op S))) : (ihomPoints R A B S) x = CategoryTheory.MonoidalClosed.uncurry (((freeForgetAdjunction R).homEquiv ((CategoryTheory.coherentTopology LightProfinite).yoneda.obj S) ((CategoryTheory.ihom A).obj B)).symm ((CategoryTheory.coherentTopology LightProfinite).yonedaEquiv.symm x))

theorem LightCondensed.ihomPoints_symm_apply (R : Type u) [CommRing R] (A B : LightCondMod R) (S : LightProfinite) (x : CategoryTheory.MonoidalCategoryStruct.tensorObj A ((free R).obj S.toCondensed) ⟶ B) : (ihomPoints R A B S).symm x = (CategoryTheory.coherentTopology LightProfinite).yonedaEquiv (((freeForgetAdjunction R).homEquiv ((CategoryTheory.coherentTopology LightProfinite).yoneda.obj S) ((CategoryTheory.ihom A).obj B)) (CategoryTheory.MonoidalClosed.curry x))

theorem LightCondensed.ihom_map_val_app (R : Type u) [CommRing R] (A B P : LightCondMod R) (S : LightProfinite) (e : A ⟶ B) (x : ↑(((CategoryTheory.ihom P).obj A).val.obj (Opposite.op S))) : (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.ihom P).map e).val.app (Opposite.op S))) x = (ihomPoints R P B S).symm (CategoryTheory.CategoryStruct.comp ((ihomPoints R P A S) x) e)

theorem LightCondensed.ihomPoints_symm_comp (R : Type u) [CommRing R] (B P : LightCondMod R) (S S' : LightProfinite) (π : S ⟶ S') (f : CategoryTheory.MonoidalCategoryStruct.tensorObj P ((free R).obj S'.toCondensed) ⟶ B) : (ihomPoints R P B S).symm (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P ((free R).map (lightProfiniteToLightCondSet.map π))) f) = (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.ihom P).obj B).val.map π.op)) ((ihomPoints R P B S').symm f)

theorem LightCondensed.internallyProjective_iff_tensor_condition (R : Type u) [CommRing R] (P : LightCondMod R) : CategoryTheory.InternallyProjective P ↔ ∀ {A B : LightCondMod R} (e : A ⟶ B) [CategoryTheory.Epi e] (S : LightProfinite) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj P ((free R).obj S.toCondensed) ⟶ B), ∃ (S' : LightProfinite) (π : S' ⟶ S) (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)) (g' : CategoryTheory.MonoidalCategoryStruct.tensorObj P ((free R).obj S'.toCondensed) ⟶ A), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P ((lightProfiniteToLightCondSet.comp (free R)).map π)) g = CategoryTheory.CategoryStruct.comp g' e

P : LightCondMod R is internally projective if and only if, for all A B : LightCondMod R, for all epimorphisms e : A ⟶ B, for all S : LightProfinite and all morphisms g : P ⊗ R[S] ⟶ B, there exists a S' : LightProfinite with a surjeciton π : S' ⟶ S and a morphism g' : P ⊗ R[S'] ⟶ A, making the diagram

P ⊗ R[S'] ⟶ A
  |          |
  v          v
P ⊗ R[S]  ⟶ B

commute.

theorem LightCondensed.internallyProjective_iff_tensor_condition' (R : Type u) [CommRing R] (P : LightCondMod R) : CategoryTheory.InternallyProjective P ↔ ∀ {A B : LightCondMod R} (e : A ⟶ B) [CategoryTheory.Epi e] (S : LightProfinite) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj ((free R).obj S.toCondensed) P ⟶ B), ∃ (S' : LightProfinite) (π : S' ⟶ S) (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)) (g' : CategoryTheory.MonoidalCategoryStruct.tensorObj ((free R).obj S'.toCondensed) P ⟶ A), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((lightProfiniteToLightCondSet.comp (free R)).map π) P) g = CategoryTheory.CategoryStruct.comp g' e

P : LightCondMod R is internally projective if and only if, for all A B : LightCondMod R, for all epimorphisms e : A ⟶ B, for all S : LightProfinite and all morphisms g : R[S] ⊗ P ⟶ B, there exists a S' : LightProfinite with a surjeciton π : S' ⟶ S and a morphism g' : R[S'] ⊗ P ⟶ A, making the diagram

R[S'] ⊗ P ⟶ A
  |          |
  v          v
R[S] ⊗ P  ⟶ B

commute.

theorem LightCondensed.free_internallyProjective_iff_tensor_condition (R : Type u) [CommRing R] (P : LightCondSet) : CategoryTheory.InternallyProjective ((free R).obj P) ↔ ∀ {A B : LightCondMod R} (e : A ⟶ B) [CategoryTheory.Epi e] (S : LightProfinite) (g : (free R).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj P S.toCondensed) ⟶ B), ∃ (S' : LightProfinite) (π : S' ⟶ S) (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)) (g' : (free R).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj P S'.toCondensed) ⟶ A), CategoryTheory.CategoryStruct.comp ((free R).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (lightProfiniteToLightCondSet.map π))) g = CategoryTheory.CategoryStruct.comp g' e

Given a P : LightCondSet, the light free light condensed module R[P] is internally projective if and only if, for all A B : LightCondMod R, for all epimorphisms e : A ⟶ B, for all S : LightProfinite and all morphisms g : R[P × S] ⟶ B, there exists a S' : LightProfinite with a surjeciton π : S' ⟶ S and a morphism g' : R[P × S'] ⟶ A, making the diagram

R[P × S'] ⟶ A
  |          |
  v          v
R[P × S]  ⟶ B

commute.

theorem LightCondensed.free_internallyProjective_iff_tensor_condition' (R : Type u) [CommRing R] (P : LightCondSet) : CategoryTheory.InternallyProjective ((free R).obj P) ↔ ∀ {A B : LightCondMod R} (e : A ⟶ B) [CategoryTheory.Epi e] (S : LightProfinite) (g : (free R).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj S.toCondensed P) ⟶ B), ∃ (S' : LightProfinite) (π : S' ⟶ S) (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)) (g' : (free R).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj S'.toCondensed P) ⟶ A), CategoryTheory.CategoryStruct.comp ((free R).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight (lightProfiniteToLightCondSet.map π) P)) g = CategoryTheory.CategoryStruct.comp g' e

Given a P : LightCondSet, the light free light condensed module R[P] is internally projective if and only if, for all A B : LightCondMod R, for all epimorphisms e : A ⟶ B, for all S : LightProfinite and all morphisms g : R[S × P] ⟶ B, there exists a S' : LightProfinite with a surjeciton π : S' ⟶ S and a morphism g' : R[S' × P] ⟶ A, making the diagram

R[S' × P] ⟶ A
  |          |
  v          v
R[S × P]  ⟶ B

commute.

theorem LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition (R : Type u) [CommRing R] (P : LightProfinite) : CategoryTheory.InternallyProjective ((free R).obj P.toCondensed) ↔ ∀ {A B : LightCondMod R} (e : A ⟶ B) [CategoryTheory.Epi e] (S : LightProfinite) (g : (free R).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj P S).toCondensed ⟶ B), ∃ (S' : LightProfinite) (π : S' ⟶ S) (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)) (g' : (free R).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj P S').toCondensed ⟶ A), CategoryTheory.CategoryStruct.comp ((free R).map (lightProfiniteToLightCondSet.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P π))) g = CategoryTheory.CategoryStruct.comp g' e

Given a P : LightProfinite, the light free light condensed module R[P] is internally projective if and only if, for all A B : LightCondMod R, for all epimorphisms e : A ⟶ B, for all S : LightProfinite and all morphisms g : R[P × S] ⟶ B, there exists a S' : LightProfinite with a surjeciton π : S' ⟶ S and a morphism g' : R[P × S'] ⟶ A, making the diagram

R[P × S'] ⟶ A
  |          |
  v          v
R[P × S]  ⟶ B

commute.

theorem LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition' (R : Type u) [CommRing R] (P : LightProfinite) : CategoryTheory.InternallyProjective ((free R).obj P.toCondensed) ↔ ∀ {A B : LightCondMod R} (e : A ⟶ B) [CategoryTheory.Epi e] (S : LightProfinite) (g : (free R).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj S P).toCondensed ⟶ B), ∃ (S' : LightProfinite) (π : S' ⟶ S) (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)) (g' : (free R).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj S' P).toCondensed ⟶ A), CategoryTheory.CategoryStruct.comp ((free R).map (lightProfiniteToLightCondSet.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight π P))) g = CategoryTheory.CategoryStruct.comp g' e

Given a P : LightProfinite, the light free light condensed module R[P] is internally projective if and only if, for all A B : LightCondMod R, for all epimorphisms e : A ⟶ B, for all S : LightProfinite and all morphisms g : R[S × P] ⟶ B, there exists a S' : LightProfinite with a surjeciton π : S' ⟶ S and a morphism g' : R[S' × P] ⟶ A, making the diagram

R[S' × P] ⟶ A
  |          |
  v          v
R[S × P]  ⟶ B

commute.