Bousfield

📁 Source: Mathlib/CategoryTheory/Abelian/SerreClass/Bousfield.lean

Statistics

Metric	Count
Definitions	0
Theorems isLocalization_isoModSerre_kernel_of_leftAdjoint, isoModSerre_kernel_eq_inverseImage_isomorphisms, isoModSerre_kernel_eq_isLocal_of_rightAdjoint, isoModSerre_kernel_eq_leftBousfield_W_of_rightAdjoint	4
Total	4

CategoryTheory.Abelian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalization_isoModSerre_kernel_of_leftAdjoint 📖	mathematical	—	CategoryTheory.Functor.IsLocalization CategoryTheory.ObjectProperty.isoModSerre CategoryTheory.Functor.kernel CategoryTheory.ObjectProperty.instIsSerreClassInverseImageOfPreservesFiniteLimitsOfPreservesFiniteColimits CategoryTheory.Limits.IsZero CategoryTheory.ObjectProperty.instIsSerreClassIsZero	—	CategoryTheory.ObjectProperty.instIsSerreClassInverseImageOfPreservesFiniteLimitsOfPreservesFiniteColimits CategoryTheory.ObjectProperty.instIsSerreClassIsZero isoModSerre_kernel_eq_inverseImage_isomorphisms CategoryTheory.Adjunction.isLocalization
isoModSerre_kernel_eq_inverseImage_isomorphisms 📖	mathematical	—	CategoryTheory.ObjectProperty.isoModSerre CategoryTheory.Functor.kernel CategoryTheory.ObjectProperty.instIsSerreClassInverseImageOfPreservesFiniteLimitsOfPreservesFiniteColimits CategoryTheory.Limits.IsZero CategoryTheory.ObjectProperty.instIsSerreClassIsZero CategoryTheory.MorphismProperty.inverseImage CategoryTheory.MorphismProperty.isomorphisms	—	CategoryTheory.MorphismProperty.ext CategoryTheory.ObjectProperty.instIsSerreClassInverseImageOfPreservesFiniteLimitsOfPreservesFiniteColimits CategoryTheory.ObjectProperty.instIsSerreClassIsZero CategoryTheory.ObjectProperty.isoModSerre_isInvertedBy_iff le_refl CategoryTheory.Limits.KernelFork.IsLimit.isZero_of_mono CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.comp_zero CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object hasZeroObject CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Limits.CokernelCofork.IsColimit.isZero_of_epi CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.zero_comp CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso
isoModSerre_kernel_eq_isLocal_of_rightAdjoint 📖	mathematical	—	CategoryTheory.ObjectProperty.isoModSerre CategoryTheory.Functor.kernel CategoryTheory.ObjectProperty.instIsSerreClassInverseImageOfPreservesFiniteLimitsOfPreservesFiniteColimits CategoryTheory.Limits.IsZero CategoryTheory.ObjectProperty.instIsSerreClassIsZero CategoryTheory.ObjectProperty.isLocal Set Set.instMembership Set.range CategoryTheory.Functor.obj	—	CategoryTheory.ObjectProperty.instIsSerreClassInverseImageOfPreservesFiniteLimitsOfPreservesFiniteColimits CategoryTheory.ObjectProperty.instIsSerreClassIsZero CategoryTheory.ObjectProperty.isLocal_eq_inverseImage_isomorphisms isoModSerre_kernel_eq_inverseImage_isomorphisms
isoModSerre_kernel_eq_leftBousfield_W_of_rightAdjoint 📖	mathematical	—	CategoryTheory.ObjectProperty.isoModSerre CategoryTheory.Functor.kernel CategoryTheory.ObjectProperty.instIsSerreClassInverseImageOfPreservesFiniteLimitsOfPreservesFiniteColimits CategoryTheory.Limits.IsZero CategoryTheory.ObjectProperty.instIsSerreClassIsZero CategoryTheory.ObjectProperty.isLocal Set Set.instMembership Set.range CategoryTheory.Functor.obj	—	isoModSerre_kernel_eq_isLocal_of_rightAdjoint

---

← Back to Index