Subobjects along a functor, and the order isomorphism from an equivalence

Mathlib maps subobjects along a morphism (Subobject.map) and along an isomorphism of objects (Subobject.mapIsoToOrderIso), both inside a single category. It does not map them along a functor, so an equivalence of categories does not yet carry subobject lattices to subobject lattices.

This file supplies that. mapFunctor pushes a subobject forward along any mono-preserving functor, and mapEquivalence upgrades it to an order isomorphism when the functor is half of an equivalence. For abelian categories, a functor preserving monos, epis, and binary coproducts also carries binary joins of subobjects to binary joins. Preserving monos and epis likewise allows the image of a lifted arrow into a fixed target to lift its image subobject in the abelian setting.

Why an order isomorphism and not just a monotone map

The consumers are chain conditions and filtrations. A monotone map carries a chain to a chain, but it does not carry a strictly increasing chain to a strictly increasing one, and it need not carry the bottom and top to the bottom and top. An order isomorphism does all three, which is what makes it possible to transport a Harder–Narasimhan filtration along an equivalence.

The shape of the proofs

For the equivalence results, the proofs reduce a subobject to a representing mono, then compare explicit morphisms using the unit isomorphism. Image preservation uses the epi--mono image factorization and balancedness instead.

def CategoryTheory.Subobject.mapFunctor {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (F : Functor A B) [F.PreservesMonomorphisms] {X : A} : Subobject X → Subobject (F.obj X)

A subobject pushed forward along a mono-preserving functor.

Equations

• CategoryTheory.Subobject.mapFunctor F = CategoryTheory.Subobject.lift (fun (x : A) (f : x ⟶ X) (x_1 : CategoryTheory.Mono f) => CategoryTheory.Subobject.mk (F.map f)) ⋯

@[simp]

theorem CategoryTheory.Subobject.mapFunctor_mk {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (F : Functor A B) [F.PreservesMonomorphisms] {X A₁ : A} (f : A₁ ⟶ X) [Mono f] : mapFunctor F (mk f) = mk (F.map f)

theorem CategoryTheory.Subobject.mapFunctor_eq_mk_arrow {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (F : Functor A B) [F.PreservesMonomorphisms] {X : A} (P : Subobject X) : mapFunctor F P = mk (F.map P.arrow)

theorem CategoryTheory.Subobject.mapFunctor_monotone {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (F : Functor A B) [F.PreservesMonomorphisms] {X : A} : Monotone (mapFunctor F)

theorem CategoryTheory.Subobject.mapFunctor_sup {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (F : Functor A B) [F.PreservesMonomorphisms] [Abelian A] [Abelian B] [F.PreservesEpimorphisms] [Limits.PreservesColimitsOfShape (Discrete Limits.WalkingPair) F] {X : A} (P Q : Subobject X) : mapFunctor F (P ⊔ Q) = mapFunctor F P ⊔ mapFunctor F Q

A functor between abelian categories that preserves monomorphisms, epimorphisms, and binary coproducts carries binary joins of subobjects to binary joins. The join is the image of the map from the coproduct.

theorem CategoryTheory.Subobject.mapFunctor_id {A : Type u₁} [Category.{v₁, u₁} A] {X : A} (P : Subobject X) : mapFunctor (Functor.id A) P = P

Pushing forward along the identity does nothing.

theorem CategoryTheory.Subobject.mapFunctor_comp {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (F : Functor A B) [F.PreservesMonomorphisms] (G : Functor B A) [G.PreservesMonomorphisms] [(F.comp G).PreservesMonomorphisms] {X : A} (P : Subobject X) : mapFunctor (F.comp G) P = mapFunctor G (mapFunctor F P)

Pushing forward along a composite is pushing forward twice. It holds by definition.

theorem CategoryTheory.Subobject.mapFunctor_map_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (F : Functor A B) [F.PreservesMonomorphisms] {X Y : A} (i : X ≅ Y) (P : Subobject X) : mapFunctor F ((map i.hom).obj P) = (map (F.map i.hom)).obj (mapFunctor F P)

Pushing forward commutes with rewriting the ambient object along an isomorphism.

theorem CategoryTheory.Subobject.map_inv_map_hom {A : Type u₁} [Category.{v₁, u₁} A] {X Y : A} (i : X ≅ Y) (P : Subobject X) : (map i.inv).obj ((map i.hom).obj P) = P

Mapping along an isomorphism and back is the identity. Stated as a lemma rather than reached by rw [← map_comp], whose motive is not type correct here: Subobject.map carries a Mono instance argument that changes under the rewrite.

theorem CategoryTheory.Subobject.map_hom_map_inv {A : Type u₁} [Category.{v₁, u₁} A] {X Y : A} (i : X ≅ Y) (Q : Subobject Y) : (map i.hom).obj ((map i.inv).obj Q) = Q

theorem CategoryTheory.Subobject.mapFunctor_image {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] [Limits.HasImages A] [Limits.HasEqualizers A] [Limits.HasImages B] [Limits.HasEqualizers B] [Balanced B] (G : Functor A B) [G.PreservesMonomorphisms] [G.PreservesEpimorphisms] {X Y : A} (f : X ⟶ Y) : mapFunctor G (Limits.imageSubobject f) = Limits.imageSubobject (G.map f)

Between categories with images and equalizers, with balanced target, a functor preserving monomorphisms and epimorphisms carries the image subobject of an arrow to the image subobject of the mapped arrow.

def CategoryTheory.Subobject.FixedTargetArrowExtension {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (G : Functor A B) (X : A) : Prop

Every arrow into G.obj X extends from a source object into the fixed source target X, up to an isomorphism on the arrow's domain. This is an explicit input for localization arguments, not an automatic consequence of essential surjectivity on objects.

Equations

• CategoryTheory.Subobject.FixedTargetArrowExtension G X = ∀ {Z : B} (β : Z ⟶ G.obj X), ∃ (Y : A) (f : Y ⟶ X) (e : Z ≅ G.obj Y), β = CategoryTheory.CategoryStruct.comp e.hom (G.map f)

def CategoryTheory.Subobject.FixedTargetMonoExtension {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (G : Functor A B) (X : A) : Prop

Only monomorphisms into G.obj X need extend in order to lift subobjects. Unlike extension of all arrows, this does not force every object of B into the essential image of G.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Subobject.mapFunctor_surjective_of_fixedTargetMonoExtension {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] [Limits.HasImages A] [Limits.HasEqualizers A] [Limits.HasImages B] [Limits.HasEqualizers B] [Balanced B] (G : Functor A B) [G.PreservesMonomorphisms] [G.PreservesEpimorphisms] (X : A) (hExt : FixedTargetMonoExtension G X) : Function.Surjective (mapFunctor G)

Fixed-target mono extension yields pointwise lifting of subobjects by taking the image of each extended monomorphism.

theorem CategoryTheory.Subobject.mapFunctor_surjective_of_fixedTargetArrowExtension {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] [Limits.HasImages A] [Limits.HasEqualizers A] [Limits.HasImages B] [Limits.HasEqualizers B] [Balanced B] (G : Functor A B) [G.PreservesMonomorphisms] [G.PreservesEpimorphisms] (X : A) (hExt : FixedTargetArrowExtension G X) : Function.Surjective (mapFunctor G)

All-arrow extension is a stronger, geometry-facing sufficient condition for lifting subobjects.

def CategoryTheory.Subobject.unitAt {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (e : A ≌ B) (X : A) : X ≅ e.inverse.obj (e.functor.obj X)

The unit of an equivalence at X, with both endpoints spelled out.

e.unitIso.app X has type (𝟭 A).obj X ≅ (e.functor ⋙ e.inverse).obj X. That is definitionally what is wanted but not syntactically, and the difference defeats rw on Subobject.map, whose statements are dependent in the ambient object. Naming the isomorphism with its endpoints spelled out is what makes the rewrites below go through.

Equations

• CategoryTheory.Subobject.unitAt e X = e.unitIso.app X

theorem CategoryTheory.Subobject.unitAt_naturality {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (e : A ≌ B) {X Y : A} (f : X ⟶ Y) : CategoryStruct.comp f (unitAt e Y).hom = CategoryStruct.comp (unitAt e X).hom (e.inverse.map (e.functor.map f))

theorem CategoryTheory.Subobject.mapFunctor_inverse_functor {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (e : A ≌ B) [e.functor.PreservesMonomorphisms] [e.inverse.PreservesMonomorphisms] {X : A} (P : Subobject X) : mapFunctor e.inverse (mapFunctor e.functor P) = (map (unitAt e X).hom).obj P

The round trip through an equivalence is the unit isomorphism.

This is the one step with content: naturality of the unit rewrites the round trip as composition with a unit component, and that component is invertible, so the two subobjects agree.

def CategoryTheory.Subobject.mapEquivalence {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (e : A ≌ B) [e.functor.PreservesMonomorphisms] [e.inverse.PreservesMonomorphisms] (X : A) : Subobject X ≃o Subobject (e.functor.obj X)

The order isomorphism on subobjects induced by an equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Subobject.mapEquivalence_apply {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (e : A ≌ B) [e.functor.PreservesMonomorphisms] [e.inverse.PreservesMonomorphisms] (X : A) (P : Subobject X) : (mapEquivalence e X) P = mapFunctor e.functor P

noncomputable def CategoryTheory.Subobject.mapFunctorIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (F : Functor A B) [F.PreservesMonomorphisms] {X : A} (P : Subobject X) : underlying.obj (mapFunctor F P) ≅ F.obj (underlying.obj P)

The underlying object of a pushed-forward subobject is the image of the underlying object.

mapFunctor F P is only propositionally mk (F.map P.arrow), so this is an isoOfEqMk rather than a definitional equality.

Equations

• CategoryTheory.Subobject.mapFunctorIso F P = (CategoryTheory.Subobject.mapFunctor F P).isoOfEqMk (F.map P.arrow) ⋯

@[simp]

theorem CategoryTheory.Subobject.mapFunctorIso_hom_arrow {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (F : Functor A B) [F.PreservesMonomorphisms] {X : A} (P : Subobject X) : CategoryStruct.comp (mapFunctorIso F P).hom (F.map P.arrow) = (mapFunctor F P).arrow

@[simp]

theorem CategoryTheory.Subobject.mapFunctorIso_hom_arrow_assoc {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (F : Functor A B) [F.PreservesMonomorphisms] {X : A} (P : Subobject X) {Z : B} (h : F.obj X ⟶ Z) : CategoryStruct.comp (mapFunctorIso F P).hom (CategoryStruct.comp (F.map P.arrow) h) = CategoryStruct.comp (mapFunctor F P).arrow h

theorem CategoryTheory.Subobject.ofLE_mapFunctor {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (F : Functor A B) [F.PreservesMonomorphisms] {X : A} {P Q : Subobject X} (h : P ≤ Q) : CategoryStruct.comp ((mapFunctor F P).ofLE (mapFunctor F Q) ⋯) (mapFunctorIso F Q).hom = CategoryStruct.comp (mapFunctorIso F P).hom (F.map (P.ofLE Q h))

The chain step transports. Both sides are maps into a subobject, so it is enough to compose with its arrow, which is a mono.

noncomputable def CategoryTheory.Subobject.cokernelOfLEMapFunctorIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian A] [Abelian B] (F : Functor A B) [F.PreservesZeroMorphisms] [F.PreservesMonomorphisms] [Limits.PreservesFiniteColimits F] {X : A} {P Q : Subobject X} (h : P ≤ Q) : Limits.cokernel ((mapFunctor F P).ofLE (mapFunctor F Q) ⋯) ≅ F.obj (Limits.cokernel (P.ofLE Q h))

The successive quotient transports.

This is what a Harder–Narasimhan filtration needs beyond the order isomorphism: its factors are cokernels of chain steps, and they must be identified with the images of the original factors. The square of ofLE_mapFunctor is an isomorphism square, so the cokernels agree; then F preserving finite colimits moves the cokernel inside.

Equations

• One or more equations did not get rendered due to their size.