Noetherian objects detected by finitely many functors

A mono-preserving functor carries a chain of subobjects to a chain. If finitely many such functors jointly reflect isomorphisms, and every image of an object is Noetherian, the original object is Noetherian: choose a stabilization index in every target, take their finite supremum, and reflect that the resulting chain step is an isomorphism.

In the other direction, a chain of subobjects in a target object stabilizes if it lifts to subobjects of one Noetherian source object. This requires a fixed ambient object for the whole chain, not merely Noetherianity of each term.

The targets are allowed to depend on the index. This is essential for geometric applications: restriction to the members Uᵢ of an open cover lands in the different categories Coh Uᵢ.

Main results

• isNoetherianObject_of_finite_jointlyReflectsIsomorphisms — finite-family detection.
• isNoetherianObject_of_liftedSubobjectChains — transfer from anchored chain lifts.
• anchored_chain_of_pointwise_lifts_iso — build an anchored chain from pointwise lifts when the functor preserves binary joins of subobjects.
• isNoetherianObject_of_reflectsIsomorphisms — the one-functor specialization.

theorem CategoryTheory.isNoetherianObject_of_finite_jointlyReflectsIsomorphisms {ι : Type w} [Finite ι] {A : Type u₁} [Category.{v₁, u₁} A] {B : ι → Type u₂} [(i : ι) → Category.{v₂, u₂} (B i)] (F : (i : ι) → Functor A (B i)) [∀ (i : ι), (F i).PreservesMonomorphisms] {X : A} (hX : ∀ (i : ι), IsNoetherianObject ((F i).obj X)) (hreflect : ∀ {Y Z : A} (f : Y ⟶ Z), (∀ (i : ι), IsIso ((F i).map f)) → IsIso f) : IsNoetherianObject X

A finite family of mono-preserving functors which jointly reflects isomorphisms detects Noetherian objects.

The family may have dependent target categories. The reflection hypothesis is stated pointwise in the form consumed by the proof; Mathlib's JointlyReflectIsomorphisms also supports dependent targets.

theorem CategoryTheory.isNoetherianObject_of_liftedSubobjectChains {A : Type u₁} [Category.{v₁, u₁} A] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor A D) [G.PreservesMonomorphisms] (Y : D) (hlift : ∀ (c : ℕ →o Subobject Y), ∃ (X : A) (e : G.obj X ≅ Y) (d : ℕ →o Subobject X), IsNoetherianObject X ∧ ∀ (n : ℕ), (Subobject.map e.hom).obj (Subobject.mapFunctor G (d n)) = c n) : IsNoetherianObject Y

A mono-preserving functor transfers Noetherianity to a target object if every increasing chain of its subobjects lifts, up to an isomorphism of the ambient object, to a chain of subobjects of one Noetherian source object. The source object may depend on the chain. No isomorphism reflection is needed: stabilization is carried forward by the functor.

theorem CategoryTheory.anchored_chain_of_pointwise_lifts {A : Type u₁} [Category.{v₁, u₁} A] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasImages A] [Limits.HasBinaryCoproducts A] [Limits.HasImages D] [Limits.HasBinaryCoproducts D] (G : Functor A D) [G.PreservesMonomorphisms] (X : A) (hjoin : ∀ (p q : Subobject X), Subobject.mapFunctor G (p ⊔ q) = Subobject.mapFunctor G p ⊔ Subobject.mapFunctor G q) (c : ℕ →o Subobject (G.obj X)) (hpt : ∀ (n : ℕ), ∃ (p : Subobject X), Subobject.mapFunctor G p = c n) : ∃ (d : ℕ →o Subobject X), ∀ (n : ℕ), Subobject.mapFunctor G (d n) = c n

Pointwise lifts of an increasing target-subobject chain can be made increasing in one source ambient object by taking successive binary joins. Preservation of these joins is an explicit hypothesis; preservation of monomorphisms alone does not supply it.

theorem CategoryTheory.anchored_chain_of_pointwise_lifts_iso {A : Type u₁} [Category.{v₁, u₁} A] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasImages A] [Limits.HasBinaryCoproducts A] [Limits.HasImages D] [Limits.HasBinaryCoproducts D] (G : Functor A D) [G.PreservesMonomorphisms] (X : A) {Y : D} (e : G.obj X ≅ Y) (hjoin : ∀ (p q : Subobject X), Subobject.mapFunctor G (p ⊔ q) = Subobject.mapFunctor G p ⊔ Subobject.mapFunctor G q) (c : ℕ →o Subobject Y) (hpt : ∀ (n : ℕ), ∃ (p : Subobject X), (Subobject.map e.hom).obj (Subobject.mapFunctor G p) = c n) : ∃ (d : ℕ →o Subobject X), ∀ (n : ℕ), (Subobject.map e.hom).obj (Subobject.mapFunctor G (d n)) = c n

The pointwise-to-anchored construction when the target ambient object is identified with the functor image by an isomorphism.

theorem CategoryTheory.isNoetherianObject_of_reflectsIsomorphisms {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (F : Functor A B) [F.PreservesMonomorphisms] [F.ReflectsIsomorphisms] {X : A} [IsNoetherianObject (F.obj X)] : IsNoetherianObject X

A mono-preserving, isomorphism-reflecting functor detects Noetherian objects.