Documentation

LeanPool.Dilatations.CategoryCounterexample

A category extension that is not a dilatation #

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).

Fact 5.2 : the "sub-algebra" characterization of ring dilatations fails for categories #

A concrete counterexample : a category C with two objects X, Y and two parallel non-identity arrows a, b : X ⟶ Y (else trivial/empty Hom-sets), Γ := {b}, and a category D (with Hom_D(X,Y) = {b, a, a ∘ b⁻¹ ∘ a}, finite) through which C → C[Γ⁻¹] factors faithfully — such that D is not isomorphic (as a C-category) to any dilatation of C.

inductive CategoryTheory.Dilatations.Fact52.Obj :

The two objects of C.

X : Obj
Y : Obj

Instances For

inductive CategoryTheory.Dilatations.Fact52.CHom :

Obj → Obj → Type

Hom_C(X,X) = {id}, Hom_C(Y,Y) = {id}, Hom_C(Y,X) = ∅, Hom_C(X,Y) = {a, b}.

Instances For

def CategoryTheory.Dilatations.Fact52.CHom.comp {P Q R : Obj} :

CHom P Q → CHom Q R → CHom P R

Composition in C — well-defined since Hom_C(Y,X) = ∅ leaves nothing nontrivial to compose beyond identities.

Equations

Instances For

@[instance_reducible]

instance CategoryTheory.Dilatations.Fact52.instCategoryStructObj :

CategoryStruct.{0, 0} Obj

Equations

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

@[instance_reducible]

instance CategoryTheory.Dilatations.Fact52.instCategoryObj :

Category.{0, 0} Obj

Equations

CategoryTheory.Dilatations.Fact52.instCategoryObj = { toCategoryStruct := CategoryTheory.Dilatations.Fact52.instCategoryStructObj, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

@[reducible, inline]

abbrev CategoryTheory.Dilatations.Fact52.D0 :

The target groupoid for separating a, b, a ∘ b⁻¹ ∘ a in C[Γ⁻¹]: the one-object groupoid on Multiplicative ℤ (Quiver.SingleObj, already fully instanced in mathlib).

Equations

CategoryTheory.Dilatations.Fact52.D0 = CategoryTheory.SingleObj (Multiplicative ℤ)

Instances For

def CategoryTheory.Dilatations.Fact52.FSepMap {P Q : Obj} :

CHom P Q → (SingleObj.star (Multiplicative ℤ) ⟶ SingleObj.star (Multiplicative ℤ))

The morphism part of FSep, sending a ↦ 1, b ↦ 0 (as elements of Multiplicative ℤ, i.e. ofAdd 1/ofAdd 0).

Equations

Instances For

def CategoryTheory.Dilatations.Fact52.FSep :

The functor F : C ⥤ D0 sending a ↦ ofAdd 1, b ↦ 1 (both automatically invertible, since D0 is a groupoid).

Equations

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

Instances For

def CategoryTheory.Dilatations.Fact52.Gamma :

MorphismProperty Obj

Γ = {b} as a MorphismProperty Obj.

Equations

CategoryTheory.Dilatations.Fact52.Gamma f = (⟨P, ⟨Q, f⟩⟩ = ⟨CategoryTheory.Dilatations.Fact52.Obj.X, ⟨CategoryTheory.Dilatations.Fact52.Obj.Y, CategoryTheory.Dilatations.Fact52.CHom.b ⟩⟩)

Instances For

theorem CategoryTheory.Dilatations.Fact52.Gamma_b :

theorem CategoryTheory.Dilatations.Fact52.FSep_inverts_Gamma :

Gamma.IsInvertedBy FSep

F inverts Γ, trivially — D0 is a groupoid, so every morphism is invertible.

noncomputable def CategoryTheory.Dilatations.Fact52.FSep' :

Functor Gamma.Localization D0

The unique extension of FSep along Γ.Q (universal property of localization).

Equations

CategoryTheory.Dilatations.Fact52.FSep' = CategoryTheory.Localization.Construction.lift CategoryTheory.Dilatations.Fact52.FSep CategoryTheory.Dilatations.Fact52.FSep_inverts_Gamma

Instances For

theorem CategoryTheory.Dilatations.Fact52.FSep'_fac :

Gamma.Q.comp FSep' = FSep

instance CategoryTheory.Dilatations.Fact52.instIsIsoLocalizationObjGammaMapQB :

IsIso (Gamma.Q.map CHom.b)

noncomputable def CategoryTheory.Dilatations.Fact52.cMor :

Gamma.Q.obj Obj.X ⟶ Gamma.Q.obj Obj.Y

The composite a ∘ b⁻¹ ∘ a in C[Γ⁻¹].

Equations

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

Instances For

theorem CategoryTheory.Dilatations.Fact52.FSep'_map_b :

FSep'.map (Gamma.Q.map CHom.b) = Multiplicative.ofAdd 0

theorem CategoryTheory.Dilatations.Fact52.FSep'_map_a :

FSep'.map (Gamma.Q.map CHom.a) = Multiplicative.ofAdd 1

theorem CategoryTheory.Dilatations.Fact52.FSep'_map_cMor :

FSep'.map cMor = Multiplicative.ofAdd 2

theorem CategoryTheory.Dilatations.Fact52.pairwise_distinct :

Gamma.Q.map CHom.b ≠ Gamma.Q.map CHom.a ∧ Gamma.Q.map CHom.b ≠ cMor ∧ Gamma.Q.map CHom.a ≠ cMor

b, a, a ∘ b⁻¹ ∘ a are pairwise distinct morphisms X ⟶ Y in C[Γ⁻¹].

inductive CategoryTheory.Dilatations.Fact52.DObj :

The two objects of D.

X : DObj
Y : DObj

Instances For

inductive CategoryTheory.Dilatations.Fact52.DHom :

DObj → DObj → Type

Hom_D(X,X)={id}, Hom_D(Y,Y)={id}, Hom_D(Y,X)=∅, Hom_D(X,Y)={b,a,c}.

Instances For

@[instance_reducible]

instance CategoryTheory.Dilatations.Fact52.instCategoryStructDObj :

CategoryStruct.{0, 0} DObj

Equations

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

@[instance_reducible]

instance CategoryTheory.Dilatations.Fact52.instCategoryDObj :

Category.{0, 0} DObj

Equations

CategoryTheory.Dilatations.Fact52.instCategoryDObj = { toCategoryStruct := CategoryTheory.Dilatations.Fact52.instCategoryStructDObj, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

def CategoryTheory.Dilatations.Fact52.CtoDObj :

The object part of C → D.

Equations

Instances For

def CategoryTheory.Dilatations.Fact52.CtoDMap {P Q : Obj} :

CHom P Q → DHom (CtoDObj P) (CtoDObj Q)

The morphism part of C → D (identity-on-objects, a ↦ a, b ↦ b).

Equations

Instances For

def CategoryTheory.Dilatations.Fact52.CtoD :

Functor Obj DObj

Fact 5.2, setup. The canonical (identity-on-objects) functor C → D.

Equations

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

Instances For

noncomputable def CategoryTheory.Dilatations.Fact52.DtoLocMap {P Q : DObj} :

DHom P Q → (DtoLocObj P ⟶ DtoLocObj Q)

The morphism part of D → C[Γ⁻¹], sending b ↦ Γ.Q(b), a ↦ Γ.Q(a), c ↦ a ∘ b⁻¹ ∘ a.

Equations

Instances For

noncomputable def CategoryTheory.Dilatations.Fact52.DtoLoc :

Functor DObj Gamma.Localization

Fact 5.2, setup. The canonical functor D → C[Γ⁻¹].

Equations

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

Instances For

theorem CategoryTheory.Dilatations.Fact52.CHom.idX_eq :

idX = CategoryStruct.id Obj.X

theorem CategoryTheory.Dilatations.Fact52.CHom.idY_eq :

idY = CategoryStruct.id Obj.Y

theorem CategoryTheory.Dilatations.Fact52.CtoD_comp_DtoLoc :

CtoD.comp DtoLoc = Gamma.Q

The triangle C → D → C[Γ⁻¹] commutes with C → C[Γ⁻¹].

theorem CategoryTheory.Dilatations.Fact52.DtoLoc_faithful :

DtoLoc.Faithful

Fact 5.2, (ii). D → C[Γ⁻¹] is faithful.

theorem CategoryTheory.Dilatations.Fact52.Q_map_a_ne_map_b (W : MorphismProperty Obj) :

W.Q.map CHom.a ≠ W.Q.map CHom.b

General separation fact. For any W : MorphismProperty Obj, a and b remain distinct after localizing at W — via the same FSep/groupoid-separation trick as pairwise_distinct, since FSep (landing in a groupoid) inverts every W, not just Γ.

theorem CategoryTheory.Dilatations.Fact52.CatToDila_a_ne_b (Z : Center Obj) :

(CatToDila Z).map CHom.a ≠ (CatToDila Z).map CHom.b

Θ(a) ≠ Θ(b) in any dilatation Dila Z, unconditionally — via Fact_2_14/ CatToDila_comp_DilaToLoc transporting Q_map_a_ne_map_b back along DilaToLoc Z.

theorem CategoryTheory.Dilatations.Fact52.Center.dom_cod_cases (Z : Center Obj) (i : Z.I) :

Z.dom i = Obj.X ∧ Z.cod i = Obj.X ∨ Z.dom i = Obj.Y ∧ Z.cod i = Obj.Y ∨ Z.dom i = Obj.X ∧ Z.cod i = Obj.Y

Every generator index of a center on Obj has domain/codomain (X,X), (Y,Y), or (X,Y) (the (Y,X) case is vacuous, Hom_C(Y,X) = ∅).

theorem CategoryTheory.Dilatations.Fact52.CHom.eq_id {P : Obj} (f : CHom P P) :

f = CategoryStruct.id P

The only endomorphism of any object in Obj is the identity.

theorem CategoryTheory.Dilatations.Fact52.CHom.eq_a_or_b (f : CHom Obj.X Obj.Y) :

f = a ∨ f = b

Hom_Obj(X,Y) = {a, b}.

theorem CategoryTheory.Dilatations.Fact52.false_of_hnq_selfmor {P Q X' : Obj} (hPQ : P = Q) (m : X' ⟶ Q) (f : P ⟶ Q) (hnq : ∀ (x : X' ⟶ P), m ≠ CategoryStruct.comp x f) :

If Z.dom i = Z.cod i (an identity-shaped generator), every witness trivially factors through Z.mor i, so such a generator index can never witness ¬ GoodCenter. All objects here are free variables of the lemma (not the compound Z.dom i/Z.cod i), so the subst below is unproblematic; the caller instantiates P, Q at Z.dom i, Z.cod i directly.

theorem CategoryTheory.Dilatations.Fact52.false_of_hnq_case3 {P Q X' : Obj} (hP : P = Obj.X) (hQ : Q = Obj.Y) {D : Type u_1} [Category.{u_2, u_1} D] (Θ : Functor Obj D) (N : Sieve Q) (gen : P ⟶ Q) (m : X' ⟶ Q) (hm : N.arrows m) (hnq : ∀ (x : X' ⟶ P), m ≠ CategoryStruct.comp x gen) (frac : {X'' : Obj} → (m' : X'' ⟶ Q) → N.arrows m' → (Θ.obj X'' ⟶ Θ.obj P)) (hfrac_comp : ∀ {X'' : Obj} (m' : X'' ⟶ Q) (hm' : N.arrows m'), CategoryStruct.comp (frac m' hm') (Θ.map gen) = Θ.map m') (hYX : ∀ (a : Θ.obj Obj.Y ⟶ Θ.obj Obj.X), False) (hendX : ∀ (e' : Θ.obj Obj.X ⟶ Θ.obj Obj.X), e' ≠ CategoryStruct.id (Θ.obj Obj.X) → False) (hab_ne : Θ.map CHom.a ≠ Θ.map CHom.b) :

A witness m in the sieve N that doesn't factor through gen forces a contradiction. Parametrized over free objects P, Q so cases m needs no dependent-elimination gymnastics.

def CategoryTheory.Dilatations.Fact52.GoodCenter (Z : Center Obj) :

The case-(ii) hypothesis, phrased directly as the factorization property needed by fractionInDilatation_eq_of_factors: every sieve-witness m ∈ Z.N i factors through the generator Z.mor i itself. For Z.mor i = a this forces (given Hom_C's rigidity) N_a ⊆ {a}; for Z.mor i = b, N_b ⊆ {b}; for Z.mor i ∈ {idX, idY} it holds unconditionally (composing with an identity is free), matching the paper's case (ii) exactly.

Equations

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

Instances For

theorem CategoryTheory.Dilatations.Fact52.false_of_not_good {Z : Center Obj} (e : DObj ≌ Dila Z) (heq : CtoD.comp e.functor = CatToDila Z) (hbad : ¬GoodCenter Z) :

Case (i). If Z is not "good", CtoD cannot be equivalent to CatToDila Z compatibly with the maps from C.

theorem CategoryTheory.Dilatations.Fact52.exists_C_mor_of_good {Z : Center Obj} (hGood : GoodCenter Z) {X Y : GeneratedCategory Z} (f : X ⟶ Y) :

∃ (c : (Localization.Construction.objEquiv (CenterMorphismProperty Z)).symm X ⟶ (Localization.Construction.objEquiv (CenterMorphismProperty Z)).symm Y), (GeneratedToDila Z).map f = (CatToDila Z).map c

Case (ii), core step. Under GoodCenter Z, every morphism of the generated category (hence, via GeneratedToDila_full, every morphism of Dila Z) between the images of two objects of Obj is Θ applied to some morphism of Obj. This collapses every fraction edge back to an original edge using fractionInDilatation_eq_of_factors, driven by the factorization GoodCenter Z supplies.

theorem CategoryTheory.Dilatations.Fact52.CatToDila_full_of_good {Z : Center Obj} (hGood : GoodCenter Z) (P Q : Obj) (φ : (CatToDila Z).obj P ⟶ (CatToDila Z).obj Q) :

∃ (c : P ⟶ Q), φ = (CatToDila Z).map c

Case (ii). Under GoodCenter Z, CatToDila Z is "full onto its generators": every morphism (CatToDila Z).obj P ⟶ (CatToDila Z).obj Q is Θ of an actual morphism of Obj.

theorem CategoryTheory.Dilatations.Fact52.no_realizing_center :

¬∃ (Z : Center Obj) (e : DObj ≌ Dila Z), CtoD.comp e.functor = CatToDila Z