Commit 2025-03-02 21:26 05ddc5f9

View on Github →

feat(CategoryTheory/Abelian): the inverse image of a Serre class by an exact functor (#22342) We also define the (essential) image of a property of objects by a functor. Functor.essImage is also made an ObjectProperty instead of a Set.

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

modified theorem AlgebraicGeometry.mem_Spec_essImage

Modified Mathlib/CategoryTheory/Abelian/SerreClass/Basic.lean

Modified Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

Modified Mathlib/CategoryTheory/Adjunction/Reflective.lean

modified theorem CategoryTheory.Functor.essImage.counit_isIso

modified theorem CategoryTheory.Functor.essImage.unit_isIso

modified def CategoryTheory.unitCompPartialBijective

modified theorem CategoryTheory.unitCompPartialBijective_symm_apply

Modified Mathlib/CategoryTheory/Closed/Ideal.lean

modified theorem CategoryTheory.ExponentialIdeal.mk'

Modified Mathlib/CategoryTheory/EssentialImage.lean

modified def CategoryTheory.Functor.essImage.getIso

modified theorem CategoryTheory.Functor.essImage.ofIso

modified theorem CategoryTheory.Functor.essImage.ofNatIso

modified def CategoryTheory.Functor.essImage.witness

modified def CategoryTheory.Functor.essImage

modified theorem CategoryTheory.Functor.obj_mem_essImage

Modified Mathlib/CategoryTheory/ObjectProperty/Basic.lean

added def CategoryTheory.ObjectProperty.inverseImage

added def CategoryTheory.ObjectProperty.map

added theorem CategoryTheory.ObjectProperty.prop_inverseImage_iff

added theorem CategoryTheory.ObjectProperty.prop_map_iff

added theorem CategoryTheory.ObjectProperty.prop_map_obj

Modified Mathlib/CategoryTheory/ObjectProperty/ClosedUnderIsomorphisms.lean

Modified Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean

Modified Mathlib/CategoryTheory/ObjectProperty/EpiMono.lean

Modified Mathlib/CategoryTheory/ObjectProperty/Extensions.lean

Modified Mathlib/CategoryTheory/Sites/ConstantSheaf.lean

Modified Mathlib/Condensed/Discrete/Characterization.lean

Modified Mathlib/Condensed/Discrete/Module.lean