Theorems · Theorem · category theory

LightCondensed.internallyProjective_iff_tensor_condition

∀ (R : Type u) [inst : 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 ((LightCondensed.free R).obj S.toCondensed) ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)),
          ∃ g',
            CategoryTheory.CategoryStruct.comp
                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P
                  ((lightProfiniteToLightCondSet.comp (LightCondensed.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 surjection π : S' ⟶ S and a morphism g' : P ⊗ R[S'] ⟶ A, making the diagram `` P ⊗ R[S'] --> A | | v v P ⊗ R[S] --> B `` commute.

Defined in

Mathlib.Condensed.Light.InternallyProjective

Cited by

2 results in Mathlib

Foundations

Depth 133 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing