Codilatations and ordinary localizations

From Arnaud Mayeux, Dilatations of categories, via their Lean formalization, https://arxiv.org/abs/2608.09305, and rndmx/DilCat at commit 604559654c948566675da3f7709b8ad3126bd487 (Apache-2.0).

Section 4 : Codilatations of categories

Codilatations are defined via dilatations and opposite categories, exactly as in the paper.

structure CategoryTheory.Dilatations.Cosieve {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : Type (max u₁ v₁)

Definition 2.1 (dual notion). A cosieve from X: a collection of morphisms out of X, stable under postcomposition.

• arrows ⦃Y : C⦄ : (X ⟶ Y) → Prop

  the underlying collection of morphisms out of X

• upward_closed {Y Z : C} {f : X ⟶ Y} : self.arrows f → ∀ (g : Y ⟶ Z), self.arrows (CategoryStruct.comp f g)

  stability by postcomposition

def CategoryTheory.Dilatations.Cosieve.generate {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (E : ⦃Y : C⦄ → (X ⟶ Y) → Prop) : Cosieve X

Definition 2.1. The cosieve generated by a collection E of morphisms out of X (denoted CoSC_E in the paper): f is generated iff f = e ≫ h for some e ∈ E.

Equations

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

def CategoryTheory.Dilatations.Cosieve.toSieveOp {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (V : Cosieve X) : Sieve (Opposite.op X)

Fact 4.2. A cosieve from X is the same data as a sieve over op X in Cᵒᵖ.

Equations

• V.toSieveOp = { arrows := fun {x : Cᵒᵖ} (f : x ⟶ Opposite.op X) => V.arrows f.unop, downward_closed := ⋯ }

def CategoryTheory.Dilatations.Sieve.toCosieveUnop {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve (Opposite.op X)) : Cosieve X

Fact 4.2, converse direction.

Equations

• CategoryTheory.Dilatations.Sieve.toCosieveUnop S = { arrows := fun {x : C} (f : X ⟶ x) => S.arrows f.op, upward_closed := ⋯ }

def CategoryTheory.Dilatations.Cosieve.equivSieveOp {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : Cosieve X ≃ Sieve (Opposite.op X)

Fact 4.2, as an explicit equivalence : a cosieve from X is a sieve over op X.

Equations

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

theorem CategoryTheory.Dilatations.Cosieve.generate_toSieveOp {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (E : ⦃Y : C⦄ → (X ⟶ Y) → Prop) : (generate E).toSieveOp = Sieve.generate fun {Y' : Cᵒᵖ} (g : Y' ⟶ Opposite.op X) => E g.unop

Fact 4.4. CoSC_E = SCᵒᵖ_E: the cosieve generated by E equals (under Fact 4.2's identification) the sieve generated by E's image under .op in Cᵒᵖ.

structure CategoryTheory.Dilatations.Cocenter (C : Type u) [Category.{v, u} C] : Type (max (u + 1) v)

A cocenter {[Vᵢ,dᵢ]}_{i∈I} in C (Definition 4.1): dᵢ a morphism, Vᵢ a cosieve from dom(dᵢ). Following Fact 4.2 (a cosieve from X is the same data as a sieve over op X in Cᵒᵖ), Vᵢ is recorded directly as a Sieve in Cᵒᵖ over op (dom dᵢ).

• I : Type u

  Indices of the denominator morphisms and their numerator cosieves.

• nonempty : Nonempty self.I
• dom : self.I → C

  Domain of each denominator morphism.

• cod : self.I → C

  Codomain of each denominator morphism.

• mor (i : self.I) : self.dom i ⟶ self.cod i

  Morphisms used as denominators in the dual construction.

• V (i : self.I) : Sieve (Opposite.op (self.dom i))

  Permitted numerators, stable under postcomposition.

def CategoryTheory.Dilatations.Cocenter.toCenterOp {C : Type u} [Category.{v, u} C] (co : Cocenter C) : Center Cᵒᵖ

The center on Cᵒᵖ obtained by regarding {[Vᵢ,dᵢ]}_{i∈I} as {[Vᵢ,(dᵢ)ᵒᵖ]}_{i∈I} (Fact 4.2).

Equations

• co.toCenterOp = { I := co.I, nonempty := ⋯, dom := fun (i : co.I) => Opposite.op (co.cod i), cod := fun (i : co.I) => Opposite.op (co.dom i), mor := fun (i : co.I) => (co.mor i).op, N := co.V }

def CategoryTheory.Dilatations.Cocenter.toCenter {C : Type u} [Category.{v, u} C] (co : Cocenter C) : Center C

The underlying {dᵢ}-only center on C. IsSigmaRegular/ImageCenterMorphismProperty only depend on I/dom/cod/mor (never on the sieve component), so any placeholder sieve works here.

Equations

• co.toCenter = { I := co.I, nonempty := ⋯, dom := co.dom, cod := co.cod, mor := co.mor, N := fun (x : co.I) => ⊤ }

def CategoryTheory.Dilatations.Codila {C : Type u} [Category.{v, u} C] (co : Cocenter C) : Type u

Definition 4.3. The codilatation of C with cocenter {[Vᵢ,dᵢ]}_{i∈I}: C[{Vᵢ∘(dᵢ)⁻¹}_{i∈I}] := (Cᵒᵖ[{(dᵢ)⁻¹∘Vᵢ}_{i∈I}])ᵒᵖ.

Equations

• CategoryTheory.Dilatations.Codila co = (CategoryTheory.Dilatations.Dila co.toCenterOp)ᵒᵖ

@[instance_reducible]

instance CategoryTheory.Dilatations.instCategoryCodila {C : Type u} [Category.{v, u} C] (co : Cocenter C) : Category.{max u v, u} (Codila co)

Equations

• CategoryTheory.Dilatations.instCategoryCodila co = id inferInstance

theorem CategoryTheory.Dilatations.MorphismProperty.op_Q_faithful {D : Type u} [Category.{v, u} D] (W : MorphismProperty D) (hW : W.Q.Faithful) : W.op.Q.Faithful

General fact used to transport faithfulness of .Q across Cᵒᵖ: if W.Q is faithful, so is (W.op).Q. Proved via the universal property of (W.op).Localization (Prop 2.8 / Localization.Construction.lift), not via raw combinatorics — (W.Q).op is faithful for free (.op preserves faithfulness), it inverts W.op (since .op preserves isomorphisms), so it factors uniquely through (W.op).Q, and faithful_of_comp_faithful finishes it.

def CategoryTheory.Dilatations.Cocenter.Upsilon {C : Type u} [Category.{v, u} C] (co : Cocenter C) : Functor C (Codila co)

Proposition 4.5 (i). The canonical functor Υ : C ⥤ Codila co, obtained by taking the rightOp of Θ : Cᵒᵖ ⥤ Dila (co.toCenterOp) (Proposition 3.1).

Equations

• co.Upsilon = (CategoryTheory.Dilatations.CatToDila co.toCenterOp).rightOp

instance CategoryTheory.Dilatations.Codila.faithful_to_loc_op {C : Type u} [Category.{v, u} C] (co : Cocenter C) : (DilaToLoc co.toCenterOp).op.Faithful

Proposition 4.5 (ii). The canonical faithful functor Codila co ⥤ (Cᵒᵖ[{(dᵢ)⁻¹}])ᵒᵖ (which identifies with C[{dᵢ}⁻¹], e.g. via the explicit description of fractions — Fact 4.4 — matching the paper's own aside).

theorem CategoryTheory.Dilatations.ImageCenterMorphismProperty_toCenter_Upsilon {C : Type u} [Category.{v, u} C] (co : Cocenter C) : ImageCenterMorphismProperty co.toCenter co.Upsilon = (ImageCenterMorphismProperty co.toCenterOp (CatToDila co.toCenterOp)).op

Cocenter.Upsilon's ImageCenterMorphismProperty (relative to co.toCenter) is exactly the .op of Θ's (relative to co.toCenterOp), matching how Upsilon = (CatToDila (co.toCenterOp)).rightOp is built.

theorem CategoryTheory.Dilatations.Cocenter.Upsilon_isSigmaRegular {C : Type u} [Category.{v, u} C] (co : Cocenter C) : IsSigmaRegular co.toCenter co.Upsilon

Proposition 4.5 (iii). Υ belongs to Cat ^ {{dᵢ}-reg}_C (i.e. is {dᵢ}-regular).

theorem CategoryTheory.Dilatations.Cocenter.comp_Upsilon_op {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v', u} D] (co : Cocenter C) (G : Functor (Codila co) D) : (co.Upsilon.comp G).op = (CatToDila co.toCenterOp).comp G.rightOp

Cocenter.Upsilon post-composed with any G corresponds, on the nose after taking .op, to Θ post-composed with G.rightOp. This is the key bridge letting factorizations through Codila co be transported to (and from) factorizations through Dila (co.toCenterOp).

theorem CategoryTheory.Dilatations.ImageCenterMorphismProperty_toCenterOp_op {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v', u} D] (co : Cocenter C) (F : Functor C D) : ImageCenterMorphismProperty co.toCenterOp F.op = (ImageCenterMorphismProperty co.toCenter F).op

ImageCenterMorphismProperty for (co.toCenterOp, F.op) is exactly the .op of ImageCenterMorphismProperty for (co.toCenter, F).

theorem CategoryTheory.Dilatations.IsSigmaRegular_toCenterOp_op {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v', u} D] (co : Cocenter C) (F : Functor C D) (hF : IsSigmaRegular co.toCenter F) : IsSigmaRegular co.toCenterOp F.op

If F : C ⥤ D is {dᵢ}-regular, so is F.op : Cᵒᵖ ⥤ Dᵒᵖ (relative to co.toCenterOp).

theorem CategoryTheory.Dilatations.Cocenter.represents {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v', u} D] (co : Cocenter C) (F : Functor C D) (hfaith : IsSigmaRegular co.toCenter F) : (∃! G : Functor (Codila co) D, co.Upsilon.comp G = F) ↔ ∀ (i : co.I), Sieve.functorPushforward F.op (co.V i) ≤ Sieve.generate (Presieve.singleton (F.op.map (co.toCenterOp.mor i)))

Proposition 4.5 (iv). Υ represents the covariant functor Cat ^ {{dᵢ}-reg}_C → Set, (C --F--> D) ↦ {∗} if CoS ^ D_{F(Vᵢ)} ⊂ CoS ^ D_{F(dᵢ)} for all i, else ∅.

§5.1 : Universal property of localizations, recovered from the universal property of

dilatations

By Fact 2.15, the dilatation for a center whose sieves are all the trivial one Nᵢ = S ^ C_{Idcod(dᵢ)} = ⊤ is the plain localization C[{dᵢ}⁻¹]. Given that identification, this section shows Dila_universal_property (Theorem 3.10) recovers Proposition 2.8 (the universal property of plain localizations) as a special case : a functor inverting every dᵢ factors uniquely through this dilatation.

theorem CategoryTheory.Dilatations.Sieve.generate_singleton_eq_top_of_isIso {D : Type u_1} [Category.{u_2, u_1} D] {X Y : D} (g : X ⟶ Y) [IsIso g] : Sieve.generate (Presieve.singleton g) = ⊤

The sieve generated by a single isomorphism is the top sieve.

def CategoryTheory.Dilatations.Center.ofMorphisms {C : Type u} [Category.{v, u} C] {I : Type u} (hI : Nonempty I) (dom cod : I → C) (mor : (i : I) → dom i ⟶ cod i) : Center C

The center built from an arbitrary indexed family of morphisms {dᵢ}_{i∈I}, using the trivial choice of sieves Nᵢ = S ^ C_{Idcod(dᵢ)} = ⊤ — matching the hypothesis of Fact 2.15.

Equations

• CategoryTheory.Dilatations.Center.ofMorphisms hI dom cod mor = { I := I, nonempty := hI, dom := dom, cod := cod, mor := mor, N := fun (x : I) => ⊤ }

theorem CategoryTheory.Dilatations.Center.ofMorphisms_universal_property {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v', u} D] {I : Type u} (hI : Nonempty I) (dom cod : I → C) (mor : (i : I) → dom i ⟶ cod i) (F : Functor C D) (hF : ∀ (i : I), IsIso (F.map (mor i))) : ∃! G : Functor (Dila (ofMorphisms hI dom cod mor)) D, (CatToDila (ofMorphisms hI dom cod mor)).comp G = F

§5.1. The universal property of dilatations recovers the universal property of localizations (Proposition 2.8, matching Fact 2.15's identification of this dilatation with C[{dᵢ}⁻¹]): any F : C ⥤ D inverting every generator dᵢ = mor i factors uniquely through Dila (Center.ofMorphisms hI dom cod mor).

theorem CategoryTheory.Dilatations.CatToDila_ofMorphisms_isIso {C : Type u} [Category.{v, u} C] {I : Type u} (hI : Nonempty I) (dom cod : I → C) (mor : (i : I) → dom i ⟶ cod i) (i : I) : IsIso ((CatToDila (Center.ofMorphisms hI dom cod mor)).map (mor i))

Fact 2.15, isomorphism-witness. With all sieves trivial, Θ(dᵢ) already has an explicit inverse fraction inside the dilatation : n/dᵢ at n := 𝟙 (cod i) (valid since N i = ⊤), with Prop_3_3's epi-ness closing the other triangle identity.

theorem CategoryTheory.Dilatations.CatToDila_ofMorphisms_isInvertedBy {C : Type u} [Category.{v, u} C] {I : Type u} (hI : Nonempty I) (dom cod : I → C) (mor : (i : I) → dom i ⟶ cod i) : (CenterMorphismProperty (Center.ofMorphisms hI dom cod mor)).IsInvertedBy (CatToDila (Center.ofMorphisms hI dom cod mor))

noncomputable def CategoryTheory.Dilatations.Fact215Inv {C : Type u} [Category.{v, u} C] {I : Type u} (hI : Nonempty I) (dom cod : I → C) (mor : (i : I) → dom i ⟶ cod i) : Functor (CenterMorphismProperty (Center.ofMorphisms hI dom cod mor)).Localization (Dila (Center.ofMorphisms hI dom cod mor))

The inverse to DilaToLoc (Center.ofMorphisms ...), built via the raw localization's own universal property (Localization.Construction.lift), now that CatToDila inverts every generator (CatToDila_ofMorphisms_isInvertedBy).

Equations

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

theorem CategoryTheory.Dilatations.Fact215Inv_fac {C : Type u} [Category.{v, u} C] {I : Type u} (hI : Nonempty I) (dom cod : I → C) (mor : (i : I) → dom i ⟶ cod i) : (CenterMorphismProperty (Center.ofMorphisms hI dom cod mor)).Q.comp (Fact215Inv hI dom cod mor) = CatToDila (Center.ofMorphisms hI dom cod mor)

noncomputable def CategoryTheory.Dilatations.localizationIso {C : Type u} [Category.{v, u} C] {I : Type u} (hI : Nonempty I) (dom cod : I → C) (mor : (i : I) → dom i ⟶ cod i) : ↧(Dila (Center.ofMorphisms hI dom cod mor)) ≅ ↧(CenterMorphismProperty (Center.ofMorphisms hI dom cod mor)).Localization

Fact 2.15. Dila (Center.ofMorphisms hI dom cod mor) (dilatation with all sieves trivial) is isomorphic to the plain localization C[{morᵢ}⁻¹].

Equations

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