Subobject lattices along an equivalence of categories

An equivalence of categories e : C ≌ D induces, for every object X of C, an equivalence MonoOver X ≌ MonoOver (e.functor.obj X) (Mathlib's CategoryTheory.MonoOver.congr), hence an equivalence between the thin skeletons, which are the subobject lattices. Since these lattices are partial orders, that equivalence is an order isomorphism. This file records it as such, so that lattice-theoretic properties of subobjects -- compactness, atoms, chain conditions -- can be transported along equivalences.

Main definitions

• CategoryTheory.Equivalence.subobjectOrderIso: the order isomorphism Subobject X ≃o Subobject (e.functor.obj X) induced by an equivalence e.

Main results

• CategoryTheory.Equivalence.subobjectOrderIso_mk: it sends the subobject represented by a monomorphism f to the one represented by e.functor.map f.

noncomputable def CategoryTheory.Equivalence.subobjectOrderIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : Subobject X ≃o Subobject (e.functor.obj X)

Subobjects along an equivalence. An equivalence of categories e induces an order isomorphism from the subobjects of X to the subobjects of e.functor.obj X.

Equations

• e.subobjectOrderIso X = (CategoryTheory.Subobject.lowerEquivalence (CategoryTheory.MonoOver.congr X e)).toOrderIso

@[simp]

theorem CategoryTheory.Equivalence.subobjectOrderIso_mk {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Y : C} (f : Y ⟶ X) [Mono f] : (e.subobjectOrderIso X) (Subobject.mk f) = Subobject.mk (e.functor.map f)

The induced order isomorphism sends the subobject represented by a monomorphism f to the subobject represented by e.functor.map f.