Theorems · Theorem · category theory
CondensedMod.IsSolid.isIso_solidification_map
∀ {R : Type (u + 1)} {inst : Ring R} {A : CondensedMod R} [self : CondensedMod.IsSolid R A] (X : Profinite),
CategoryTheory.IsIso ((CategoryTheory.yoneda.obj A).map ((Condensed.profiniteSolidification R).app X).op)- Defined in
- Mathlib.Condensed.Solid
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 183 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CondensedMod.IsSolid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functor.objstatement · cited by 19,642
- CategoryTheory.Functorstatement · cited by 16,252
- CategoryTheory.Functor.mapstatement · cited by 8,698
- Oppositestatement · cited by 8,081
- Ringstatement and proof · cited by 7,463
- CategoryTheory.NatTrans.appstatement · cited by 7,406
- TopCat.carrierstatement · cited by 3,184
- Quiver.Hom.opstatement · cited by 1,948
- TopCatstatement · cited by 1,889
- ModuleCatstatement · cited by 1,429
- CategoryTheory.IsIsostatement · cited by 1,156
- CategoryTheory.Presheaf.IsSheafstatement · cited by 991
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.