← all areas

Namespace CategoryTheory 15 theorems

Functor 5 · IsPullback 1 · MonoidalCategory 1 · MonoidalClosed 1 · MorphismProperty 1 · Pseudofunctor 1 · Sheaf 2 · ShortComplex 2 · Under 1

CategoryTheory.Functor 5

• Open chart of the total presheaf from representability over U CategoryTheory.Functor.exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map 0 below · cited by 2 · depth 15
• Corepresentability descends along a faithfully flat base change CategoryTheory.Functor.exists_corepresentableBy_of_faithfullyFlat_of_sheaf_univ 5 below · cited by 1 · depth 35
• Corepresenting algebra base-changes to the S₁-corepresenting algebra CategoryTheory.Functor.nonempty_algEquiv_tensorProduct_right_of_corepresentableBy_of_corepresents_under 0 below · cited by 1 · depth 35
• Descent datum on an algebra corepresenting a functor after base change CategoryTheory.Functor.exists_algEquiv_tensorProduct_descentDatum_of_corepresents_univ 0 below · cited by 1 · depth 36
• Affine descent criterion for corepresentability of a functor CategoryTheory.Functor.exists_corepresentableBy_of_descentDatum_of_bijective_univ 1 below · cited by 1 · depth 36

CategoryTheory.IsPullback 1

• Base change along t is a pullback of π CategoryTheory.IsPullback.fst_pullbackMap_of_comp_eq 0 below · cited by 7 · depth 14

CategoryTheory.MonoidalCategory 1

• Tensor inverses in a braided category are unique up to isomorphism CategoryTheory.MonoidalCategory.nonempty_iso_of_tensor_iso_tensorUnit 0 below · cited by 24 · depth 13

CategoryTheory.MonoidalClosed 1

• Tensor-invertible objects: evaluation and the bidual map are isomorphisms CategoryTheory.MonoidalClosed.isIso_ev_app_and_isIso_curry_braiding_ev_of_tensor_iso_unit 0 below · cited by 2 · depth 16

CategoryTheory.MorphismProperty 1

• Base morphism of a finite wide pullback lies in P CategoryTheory.MorphismProperty.widePullback_base 0 below · cited by 5 · depth 16

CategoryTheory.Pseudofunctor 1

• Effectiveness of a descent datum is local on the base CategoryTheory.Pseudofunctor.DescentData.exists_iso_toDescentData_obj_of_isStackFor_of_forall_exists_iso_pullFunctor_obj 0 below · cited by 1 · depth 19

CategoryTheory.Sheaf 2

• Universe lifting of coefficients preserves injective abelian sheaves CategoryTheory.Sheaf.preservesInjectiveObjects_sheafCompose_uliftFunctor 0 below · cited by 1 · depth 14
• Sheaf isomorphism from a natural family of additive bijections CategoryTheory.Sheaf.exists_iso_of_addEquiv_obj_natural 0 below · cited by 1 · depth 15

CategoryTheory.ShortComplex 2

• A monomorphism and its cokernel form a short exact sequence CategoryTheory.ShortComplex.shortExact_of_mono_cokernel 0 below · cited by 2 · depth 12
• extClass = 0 iff g admits a section CategoryTheory.ShortComplex.ShortExact.extClass_eq_zero_iff_exists_section_g 0 below · cited by 2 · depth 14

CategoryTheory.Under 1

• Base change W⊗_{R_0}H corepresents R₀-algebra maps from H CategoryTheory.Under.exists_finite_faithfullyFlat_equiv_ringHom_comp_algebraMap_eq_of_free 0 below · cited by 1 · depth 36