Construction and universal property of categorical dilatations

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

theorem CategoryTheory.Dilatations.transported_comp {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (hX : X = X') (hY : Y = Y') (hZ : Z = Z') (f : X' ⟶ Y') (g : Y' ⟶ Z') : CategoryStruct.comp (CategoryStruct.comp (eqToHom hX) (CategoryStruct.comp f (eqToHom ⋯))) (CategoryStruct.comp (eqToHom hY) (CategoryStruct.comp g (eqToHom ⋯))) = CategoryStruct.comp (eqToHom hX) (CategoryStruct.comp (CategoryStruct.comp f g) (eqToHom ⋯))

Transporting the endpoints of two composable morphisms respects composition.

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

Definition 2.9. A center {[Nᵢ,dᵢ]}ᵢ∈I in C.

• I : Type u

  Indices of the denominator morphisms and their numerator sieves.

• 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 by which the corresponding numerators may be divided.

• N (i : self.I) : Sieve (self.cod i)

  Permitted numerators, stable under precomposition.

def CategoryTheory.Dilatations.IsCenterMor {C : Type u} [Category.{v, u} C] (Z : Center C) (f : (X : C) × (Y : C) × (X ⟶ Y)) : Prop

Whether a dependent morphism is one of the chosen denominators.

Equations

• CategoryTheory.Dilatations.IsCenterMor Z f = ∃ (i : Z.I), f = ⟨Z.dom i, ⟨Z.cod i, Z.mor i⟩⟩

def CategoryTheory.Dilatations.CenterMorphismProperty {C : Type u} [Category.{v, u} C] (Z : Center C) : MorphismProperty C

The MorphismProperty corresponding to IsCenterMor.

Equations

• CategoryTheory.Dilatations.CenterMorphismProperty Z f = CategoryTheory.Dilatations.IsCenterMor Z ⟨X, ⟨Y, f⟩⟩

def CategoryTheory.Dilatations.CenterLocalization {C : Type u} [Category.{v, u} C] (Z : Center C) : Type u

The localized category obtained by formally inverting the morphisms in CenterMorphismProperty.

Equations

• CategoryTheory.Dilatations.CenterLocalization Z = (CategoryTheory.Dilatations.CenterMorphismProperty Z).Localization

def CategoryTheory.Dilatations.LocalizationFunctor {C : Type u} [Category.{v, u} C] (Z : Center C) : Functor C (CenterMorphismProperty Z).Localization

The canonical functor from C to the localization.

Equations

• CategoryTheory.Dilatations.LocalizationFunctor Z = (CategoryTheory.Dilatations.CenterMorphismProperty Z).Q

def CategoryTheory.Dilatations.CenterSievePair {C : Type u} [Category.{v, u} C] (Z : Center C) : Type (max u v)

A chosen denominator together with a permitted numerator.

Equations

• CategoryTheory.Dilatations.CenterSievePair Z = ((i : Z.I) × (X : C) × { f : X ⟶ Z.cod i // (Z.N i).arrows f })

def CategoryTheory.Dilatations.localizationQuiver {C : Type u} [Category.{v, u} C] (Z : Center C) : Type u

The quiver obtained by adjoining formal inverses of the chosen denominators.

Equations

• CategoryTheory.Dilatations.localizationQuiver Z = CategoryTheory.Localization.Construction.LocQuiver (CategoryTheory.Dilatations.CenterMorphismProperty Z)

def CategoryTheory.Dilatations.inverseInPath {C : Type u} [Category.{v, u} C] (Z : Center C) (p : CenterSievePair Z) : Localization.Construction.ιPaths (CenterMorphismProperty Z) (Z.cod p.fst) ⟶ Localization.Construction.ιPaths (CenterMorphismProperty Z) (Z.dom p.fst)

The formal inverse of the denominator attached to a numerator.

Equations

• CategoryTheory.Dilatations.inverseInPath Z p = CategoryTheory.Localization.Construction.ψ₂ (CategoryTheory.Dilatations.CenterMorphismProperty Z) (Z.mor p.fst) ⋯

def CategoryTheory.Dilatations.fractionInPath {C : Type u} [Category.{v, u} C] (Z : Center C) (p : CenterSievePair Z) : Localization.Construction.ιPaths (CenterMorphismProperty Z) p.snd.fst ⟶ Localization.Construction.ιPaths (CenterMorphismProperty Z) (Z.dom p.fst)

The path consisting of a numerator followed by its formal denominator inverse.

Equations

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

def CategoryTheory.Dilatations.fractionInLocalization {C : Type u} [Category.{v, u} C] (Z : Center C) (p : CenterSievePair Z) : (Localization.Construction.objEquiv (CenterMorphismProperty Z)) p.snd.fst ⟶ (Localization.Construction.objEquiv (CenterMorphismProperty Z)) (Z.dom p.fst)

A permitted fraction evaluated in the ambient localization.

Equations

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

def CategoryTheory.Dilatations.IsPairMor {C : Type u} [Category.{v, u} C] (Z : Center C) (f : (X : (CenterMorphismProperty Z).Localization) × (Y : (CenterMorphismProperty Z).Localization) × (X ⟶ Y)) : Prop

Whether a localization morphism is represented by one permitted fraction.

Equations

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

structure CategoryTheory.Dilatations.PairMorWitness {C : Type u} [Category.{v, u} C] (Z : Center C) {X Y : (CenterMorphismProperty Z).Localization} (f : X ⟶ Y) : Type (max u v)

Data exhibiting a localization morphism as a permitted fraction.

• p : CenterSievePair Z

  The chosen denominator and numerator representing the morphism.

• eq : ⟨X, ⟨Y, f⟩⟩ = ⟨(Localization.Construction.objEquiv (CenterMorphismProperty Z)) self.p.snd.fst, ⟨(Localization.Construction.objEquiv (CenterMorphismProperty Z)) (Z.dom self.p.fst), (Quotient.functor (Localization.Construction.relations (CenterMorphismProperty Z))).map (fractionInPath Z self.p)⟩⟩

def CategoryTheory.Dilatations.FractionMorphismProperty {C : Type u} [Category.{v, u} C] (Z : Center C) : MorphismProperty (CenterMorphismProperty Z).Localization

The localization morphisms represented by single permitted fractions.

Equations

• CategoryTheory.Dilatations.FractionMorphismProperty Z f = CategoryTheory.Dilatations.IsPairMor Z ⟨X, ⟨Y, f⟩⟩

structure CategoryTheory.Dilatations.OriginalWitness {C : Type u} [Category.{v, u} C] (Z : Center C) {X Y : (CenterMorphismProperty Z).Localization} (f : X ⟶ Y) : Type v

Data exhibiting a localization morphism as the image of a base morphism.

• g : (Localization.Construction.objEquiv (CenterMorphismProperty Z)).symm X ⟶ (Localization.Construction.objEquiv (CenterMorphismProperty Z)).symm Y

  The base morphism whose localization image is the given morphism.

• eq : f = (CenterMorphismProperty Z).Q.map self.g

inductive CategoryTheory.Dilatations.GeneratorMorphismData {C : Type u} [Category.{v, u} C] (Z : Center C) {X Y : (CenterMorphismProperty Z).Localization} (f : X ⟶ Y) : Type (max u v)

A generator is either a permitted fraction or the image of a base morphism.

• fraction {C : Type u} [Category.{v, u} C] {Z : Center C} {X Y : (CenterMorphismProperty Z).Localization} {f : X ⟶ Y} : PairMorWitness Z f → GeneratorMorphismData Z f
• original {C : Type u} [Category.{v, u} C] {Z : Center C} {X Y : (CenterMorphismProperty Z).Localization} {f : X ⟶ Y} : OriginalWitness Z f → GeneratorMorphismData Z f

@[instance_reducible]

def CategoryTheory.Dilatations.GeneratorQuiver {C : Type u} [Category.{v, u} C] (Z : Center C) : Quiver (CenterMorphismProperty Z).Localization

The quiver of witnessed original and fraction morphisms.

Equations

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

def CategoryTheory.Dilatations.GeneratorObjects {C : Type u} [Category.{v, u} C] (Z : Center C) : Type u

Objects of the ambient localization, used to build the generator category.

Equations

• CategoryTheory.Dilatations.GeneratorObjects Z = (CategoryTheory.Dilatations.CenterMorphismProperty Z).Localization

@[instance_reducible]

instance CategoryTheory.Dilatations.instQuiverGeneratorObjects {C : Type u} [Category.{v, u} C] (Z : Center C) : Quiver (GeneratorObjects Z)

Equations

• CategoryTheory.Dilatations.instQuiverGeneratorObjects Z = CategoryTheory.Dilatations.GeneratorQuiver Z

def CategoryTheory.Dilatations.GeneratedCategory {C : Type u} [Category.{v, u} C] (Z : Center C) : Type u

The free category on the original and fraction generators.

Equations

• CategoryTheory.Dilatations.GeneratedCategory Z = CategoryTheory.Paths (CategoryTheory.Dilatations.GeneratorObjects Z)

@[instance_reducible]

instance CategoryTheory.Dilatations.instCategoryGeneratedCategory {C : Type u} [Category.{v, u} C] (Z : Center C) : Category.{max u v, u} (GeneratedCategory Z)

Equations

• CategoryTheory.Dilatations.instCategoryGeneratedCategory Z = CategoryTheory.Paths.categoryPaths (CategoryTheory.Dilatations.GeneratorObjects Z)

def CategoryTheory.Dilatations.forgetGenerator {C : Type u} [Category.{v, u} C] (Z : Center C) : GeneratorObjects Z ⥤q (CenterMorphismProperty Z).Localization

Forget the witness distinguishing original and fraction generators.

Equations

• CategoryTheory.Dilatations.forgetGenerator Z = { obj := id, map := fun {x x_1 : CategoryTheory.Dilatations.GeneratorObjects Z} (f : x ⟶ x_1) => f.fst }

noncomputable def CategoryTheory.Dilatations.GeneratedToLocalization {C : Type u} [Category.{v, u} C] (Z : Center C) : Functor (GeneratedCategory Z) (CenterMorphismProperty Z).Localization

Evaluate a path of generators by composition in the localization.

Equations

• CategoryTheory.Dilatations.GeneratedToLocalization Z = CategoryTheory.Paths.lift (CategoryTheory.Dilatations.forgetGenerator Z)

def CategoryTheory.Dilatations.originalFactor {C : Type u} [Category.{v, u} C] (Z : Center C) {X Y : (CenterMorphismProperty Z).Localization} (f : X ⟶ Y) (h : OriginalWitness Z f) : (Localization.Construction.objEquiv (CenterMorphismProperty Z)).symm X ⟶ (Localization.Construction.objEquiv (CenterMorphismProperty Z)).symm Y

Recover the base morphism from its original-morphism witness.

Equations

• CategoryTheory.Dilatations.originalFactor Z f h = h.g

def CategoryTheory.Dilatations.DilaRel {C : Type u} [Category.{v, u} C] (Z : Center C) : HomRel (GeneratedCategory Z)

Two paths are identified exactly when they evaluate equally in the localization.

Equations

• CategoryTheory.Dilatations.DilaRel Z f g = ((CategoryTheory.Dilatations.GeneratedToLocalization Z).map f = (CategoryTheory.Dilatations.GeneratedToLocalization Z).map g)

def CategoryTheory.Dilatations.Dila {C : Type u} [Category.{v, u} C] (Z : Center C) : Type u

Definition 2.13 / Fact 2.11. The dilatation C[{(dᵢ)⁻¹∘Nᵢ}ᵢ∈I]: objects are C's objects, morphisms are {[Nᵢ,dᵢ]}-fractions, composed via Quotient (Fact 2.11's associativity of fraction composition is Quotient.category's own well-definedness).

Equations

• CategoryTheory.Dilatations.Dila Z = CategoryTheory.Quotient (CategoryTheory.Dilatations.DilaRel Z)

@[instance_reducible]

instance CategoryTheory.Dilatations.instCategoryDila {C : Type u} [Category.{v, u} C] (Z : Center C) : Category.{max u v, u} (Dila Z)

Equations

• CategoryTheory.Dilatations.instCategoryDila Z = CategoryTheory.Quotient.category (CategoryTheory.Dilatations.DilaRel Z)

noncomputable def CategoryTheory.Dilatations.DilaToLoc {C : Type u} [Category.{v, u} C] (Z : Center C) : Functor (Dila Z) (CenterMorphismProperty Z).Localization

The canonical faithful functor from the dilatation to the ambient localization.

Equations

• CategoryTheory.Dilatations.DilaToLoc Z = CategoryTheory.Quotient.lift (CategoryTheory.Dilatations.DilaRel Z) (CategoryTheory.Dilatations.GeneratedToLocalization Z) ⋯

instance CategoryTheory.Dilatations.instCongruenceGeneratedCategoryDilaRel {C : Type u} [Category.{v, u} C] (Z : Center C) : Congruence (DilaRel Z)

theorem CategoryTheory.Dilatations.DilaToLoc_faithful {C : Type u} [Category.{v, u} C] (Z : Center C) : (DilaToLoc Z).Faithful

def CategoryTheory.Dilatations.GeneratedToDila {C : Type u} [Category.{v, u} C] (Z : Center C) : Functor (GeneratedCategory Z) (Dila Z)

The quotient functor from generator paths to the dilatation.

Equations

• CategoryTheory.Dilatations.GeneratedToDila Z = CategoryTheory.Quotient.functor (CategoryTheory.Dilatations.DilaRel Z)

instance CategoryTheory.Dilatations.GeneratedToDila_full {C : Type u} [Category.{v, u} C] (Z : Center C) : (GeneratedToDila Z).Full

def CategoryTheory.Dilatations.CToGeneratorQuiver {C : Type u} [Category.{v, u} C] (Z : Center C) : C ⥤q GeneratorObjects Z

The base-category prefunctor sending morphisms to original generators.

Equations

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

def CategoryTheory.Dilatations.CatToDila {C : Type u} [Category.{v, u} C] (Z : Center C) : Functor C (Dila Z)

Proposition 3.1 (1). The canonical functor Θ : C ⥤ C'.

Equations

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

theorem CategoryTheory.Dilatations.CatToDila_comp_DilaToLoc {C : Type u} [Category.{v, u} C] (Z : Center C) : (CatToDila Z).comp (DilaToLoc Z) = LocalizationFunctor Z

theorem CategoryTheory.Dilatations.Fact_3_2 {A : Type u_1} [Category.{u_3, u_1} A] {B : Type u_2} [Category.{u_4, u_2} B] (F : Functor A B) [F.Faithful] {X Y : A} (f : X ⟶ Y) [Mono (F.map f)] [Epi (F.map f)] : Mono f ∧ Epi f

Fact 3.2. A morphism whose image under a faithful functor is a bimorphism (mono and epi) is itself a bimorphism.

theorem CategoryTheory.Dilatations.Prop_3_3 {C : Type u} [Category.{v, u} C] (Z : Center C) (i : Z.I) : Mono ((CatToDila Z).map (Z.mor i)) ∧ Epi ((CatToDila Z).map (Z.mor i))

Proposition 3.3. For i : Z.I, Θ(dᵢ) = (CatToDila Z).map (Z.mor i) is a bimorphism in Dila Z.

def CategoryTheory.Dilatations.CatToDilaSieve {C : Type u} [Category.{v, u} C] (Z : Center C) {X : C} (N : Sieve X) : Sieve ((CatToDila Z).obj X)

Push a sieve forward along the canonical dilatation functor.

Equations

• CategoryTheory.Dilatations.CatToDilaSieve Z N = CategoryTheory.Sieve.functorPushforward (CategoryTheory.Dilatations.CatToDila Z) N

theorem CategoryTheory.Dilatations.fraction_comp_mor {C : Type u} [Category.{v, u} C] (Z : Center C) (i : Z.I) (X : C) (m : X ⟶ Z.cod i) (hm : (Z.N i).arrows m) : CategoryStruct.comp (fractionInLocalization Z ⟨i, ⟨X, ⟨m, hm⟩⟩⟩) ((CenterMorphismProperty Z).Q.map (Z.mor i)) = (CenterMorphismProperty Z).Q.map m

def CategoryTheory.Dilatations.fractionGenerator {C : Type u} [Category.{v, u} C] (Z : Center C) (p : CenterSievePair Z) : (CToGeneratorQuiver Z).obj p.snd.fst ⟶ (CToGeneratorQuiver Z).obj (Z.dom p.fst)

The generator corresponding to a single permitted fraction.

Equations

• CategoryTheory.Dilatations.fractionGenerator Z p = ⟨CategoryTheory.Dilatations.fractionInLocalization Z p, CategoryTheory.Dilatations.GeneratorMorphismData.fraction { p := p, eq := ⋯ }⟩

def CategoryTheory.Dilatations.fractionInDilatation {C : Type u} [Category.{v, u} C] (Z : Center C) (p : CenterSievePair Z) : (CatToDila Z).obj p.snd.fst ⟶ (CatToDila Z).obj (Z.dom p.fst)

Proposition 3.1 (2), existence. The fraction b = dᵢ\n = [n∘l_{dᵢ}] witnessing the unique factorization [n] = Θ(dᵢ) ∘ b.

Equations

• CategoryTheory.Dilatations.fractionInDilatation Z p = (CategoryTheory.Dilatations.GeneratedToDila Z).map (CategoryTheory.Dilatations.fractionGenerator Z p).toPath

theorem CategoryTheory.Dilatations.fraction_in_dila_comp_mor {C : Type u} [Category.{v, u} C] (Z : Center C) (i : Z.I) (X : C) (m : X ⟶ Z.cod i) (hm : (Z.N i).arrows m) : CategoryStruct.comp (fractionInDilatation Z ⟨i, ⟨X, ⟨m, hm⟩⟩⟩) ((CatToDila Z).map (Z.mor i)) = (CatToDila Z).map m

Proposition 3.1 (2), defining property. b ≫ Θ(dᵢ) = Θ(n), i.e. the triangle [n] = Θ(dᵢ) ∘ b commutes.

theorem CategoryTheory.Dilatations.CatToDila_image_sieve_le_singleton {C : Type u} [Category.{v, u} C] (Z : Center C) (i : Z.I) : CatToDilaSieve Z (Z.N i) ≤ Sieve.generate (Presieve.singleton ((CatToDila Z).map (Z.mor i)))

Proposition 3.5. S ^ C'_Θ(Nᵢ) ⊂ S ^ C'_Θ(dᵢ).

theorem CategoryTheory.Dilatations.GeneratedCategory_morphism_induction {C : Type u} [Category.{v, u} C] (Z : Center C) (P : {X Y : GeneratedCategory Z} → (X ⟶ Y) → Prop) (h_id : ∀ (X : GeneratedCategory Z), P (CategoryStruct.id X)) (h_comp : ∀ {X Y W : GeneratedCategory Z} (f : X ⟶ Y) (g : Y ⟶ W), P f → P g → P (CategoryStruct.comp f g)) (h_gen : ∀ {A B : GeneratorObjects Z} (g : A ⟶ B), P g.toPath) {X Y : GeneratedCategory Z} (f : X ⟶ Y) : P f

The universal property

def CategoryTheory.Dilatations.IsImageCenterMor {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (f : (X : D) × (Y : D) × (X ⟶ Y)) : Prop

Morphisms in D obtained as images of the chosen central morphisms of C.

Equations

• CategoryTheory.Dilatations.IsImageCenterMor Z F f = ∃ (i : Z.I), f = ⟨F.obj (Z.dom i), ⟨F.obj (Z.cod i), F.map (Z.mor i)⟩⟩

def CategoryTheory.Dilatations.ImageCenterMorphismProperty {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) : MorphismProperty D

The morphism property consisting of the images of the chosen denominators.

Equations

• CategoryTheory.Dilatations.ImageCenterMorphismProperty Z F f = CategoryTheory.Dilatations.IsImageCenterMor Z F ⟨X, ⟨Y, f⟩⟩

def CategoryTheory.Dilatations.ImageCenterLocalization {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) : Type u

The localization of D obtained by formally inverting the images of the central morphisms.

Equations

• CategoryTheory.Dilatations.ImageCenterLocalization Z F = (CategoryTheory.Dilatations.ImageCenterMorphismProperty Z F).Localization

@[instance_reducible]

noncomputable instance CategoryTheory.Dilatations.instCategoryImageCenterLocalization {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) : Category.{max u v', u} (ImageCenterLocalization Z F)

Equations

• CategoryTheory.Dilatations.instCategoryImageCenterLocalization Z F = id inferInstance

def CategoryTheory.Dilatations.ImageCenterLocalizationFunctor {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) : Functor D (ImageCenterLocalization Z F)

The canonical functor from D to the localization.

Equations

• CategoryTheory.Dilatations.ImageCenterLocalizationFunctor Z F = (CategoryTheory.Dilatations.ImageCenterMorphismProperty Z F).Q

theorem CategoryTheory.Dilatations.exists_factor_D {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) (i : Z.I) (Y : D) (n : Y ⟶ F.obj (Z.cod i)) : (Sieve.functorPushforward F (Z.N i)).arrows n → ∃ (q : Y ⟶ F.obj (Z.dom i)), CategoryStruct.comp q (F.map (Z.mor i)) = n

theorem CategoryTheory.Dilatations.unique_factor_D {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (i : Z.I) (Y : D) (q₁ q₂ : Y ⟶ F.obj (Z.dom i)) : CategoryStruct.comp q₁ (F.map (Z.mor i)) = CategoryStruct.comp q₂ (F.map (Z.mor i)) → q₁ = q₂

theorem CategoryTheory.Dilatations.exists_unique_factor_D {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) (i : Z.I) (Y : D) (n : Y ⟶ F.obj (Z.cod i)) : (Sieve.functorPushforward F (Z.N i)).arrows n → ∃! q : Y ⟶ F.obj (Z.dom i), CategoryStruct.comp q (F.map (Z.mor i)) = n

noncomputable def CategoryTheory.Dilatations.uniqueFactor {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) (i : Z.I) (Y : C) (n : Y ⟶ Z.cod i) (hn : (Z.N i).arrows n) : F.obj Y ⟶ F.obj (Z.dom i)

The unique factor of a mapped numerator through its mapped denominator.

Equations

• CategoryTheory.Dilatations.uniqueFactor Z F hfaith hsieve i Y n hn = Classical.choose ⋯

noncomputable def CategoryTheory.Dilatations.mapGenerator {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) {X Y : GeneratorObjects Z} (g : X ⟶ Y) : F.obj ((Localization.Construction.objEquiv (CenterMorphismProperty Z)).symm X) ⟶ F.obj ((Localization.Construction.objEquiv (CenterMorphismProperty Z)).symm Y)

Interpret each original or fraction generator in a sieve-compatible target category.

Equations

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

noncomputable def CategoryTheory.Dilatations.localizationMap {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) : Functor (CenterMorphismProperty Z).Localization (ImageCenterLocalization Z F)

The functor between localizations induced by the original functor.

Equations

• CategoryTheory.Dilatations.localizationMap Z F = CategoryTheory.Localization.Construction.lift (F.comp (CategoryTheory.Dilatations.ImageCenterLocalizationFunctor Z F)) ⋯

theorem CategoryTheory.Dilatations.localizationMap_comp_Q {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) : (CenterMorphismProperty Z).Q.comp (localizationMap Z F) = F.comp (ImageCenterLocalizationFunctor Z F)

noncomputable def CategoryTheory.Dilatations.generatorImage {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) : GeneratorObjects Z ⥤q D

The prefunctor interpreting dilatation generators in the target category.

Equations

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

noncomputable def CategoryTheory.Dilatations.H {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) : Functor (GeneratedCategory Z) D

Extend the generator interpretation to paths by the free-category universal property.

Equations

• CategoryTheory.Dilatations.H Z F hfaith hsieve = CategoryTheory.Paths.lift (CategoryTheory.Dilatations.generatorImage Z F hfaith hsieve)

theorem CategoryTheory.Dilatations.mapGenerator_original {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) {X Y : C} (f : X ⟶ Y) : mapGenerator Z F hfaith hsieve ⟨(CenterMorphismProperty Z).Q.map f, GeneratorMorphismData.original { g := f, eq := ⋯ }⟩ = F.map f

theorem CategoryTheory.Dilatations.H_map_original {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) {X Y : C} (f : X ⟶ Y) : (H Z F hfaith hsieve).map ((CToGeneratorQuiver Z).map f).toPath = F.map f

theorem CategoryTheory.Dilatations.uniqueFactor_spec {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) (i : Z.I) (Y : C) (n : Y ⟶ Z.cod i) (hn : (Z.N i).arrows n) : CategoryStruct.comp (uniqueFactor Z F hfaith hsieve i Y n hn) (F.map (Z.mor i)) = F.map n

theorem CategoryTheory.Dilatations.generatedLocalization_commutes_obj {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) (A : GeneratedCategory Z) : ((H Z F hfaith hsieve).comp (ImageCenterLocalizationFunctor Z F)).obj A = ((GeneratedToLocalization Z).comp (localizationMap Z F)).obj A

theorem CategoryTheory.Dilatations.H_map_fraction {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) (p : CenterSievePair Z) {gf : (Localization.Construction.objEquiv (CenterMorphismProperty Z)) p.snd.fst ⟶ (Localization.Construction.objEquiv (CenterMorphismProperty Z)) (Z.dom p.fst)} (heq : ⟨(Localization.Construction.objEquiv (CenterMorphismProperty Z)) p.snd.fst, ⟨(Localization.Construction.objEquiv (CenterMorphismProperty Z)) (Z.dom p.fst), gf⟩⟩ = ⟨(Localization.Construction.objEquiv (CenterMorphismProperty Z)) p.snd.fst, ⟨(Localization.Construction.objEquiv (CenterMorphismProperty Z)) (Z.dom p.fst), (Quotient.functor (Localization.Construction.relations (CenterMorphismProperty Z))).map (fractionInPath Z p)⟩⟩) (hgf : gf = fractionInLocalization Z p) : (H Z F hfaith hsieve).map (Quiver.Hom.toPath ⟨gf, GeneratorMorphismData.fraction { p := p, eq := heq }⟩) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (uniqueFactor Z F hfaith hsieve p.fst p.snd.fst ↑p.snd.snd ⋯) (eqToHom ⋯))

theorem CategoryTheory.Dilatations.GeneratedToLocalization_map_fraction {C : Type u} [Category.{v, u} C] (Z : Center C) (p : CenterSievePair Z) {gf : (Localization.Construction.objEquiv (CenterMorphismProperty Z)) p.snd.fst ⟶ (Localization.Construction.objEquiv (CenterMorphismProperty Z)) (Z.dom p.fst)} (heq : ⟨(Localization.Construction.objEquiv (CenterMorphismProperty Z)) p.snd.fst, ⟨(Localization.Construction.objEquiv (CenterMorphismProperty Z)) (Z.dom p.fst), gf⟩⟩ = ⟨(Localization.Construction.objEquiv (CenterMorphismProperty Z)) p.snd.fst, ⟨(Localization.Construction.objEquiv (CenterMorphismProperty Z)) (Z.dom p.fst), (Quotient.functor (Localization.Construction.relations (CenterMorphismProperty Z))).map (fractionInPath Z p)⟩⟩) (hgf : gf = fractionInLocalization Z p) : (GeneratedToLocalization Z).map (Quiver.Hom.toPath ⟨gf, GeneratorMorphismData.fraction { p := p, eq := heq }⟩) = fractionInLocalization Z p

GeneratedToLocalization sends a fraction generator to fractionInLocalization.

theorem CategoryTheory.Dilatations.mapGenerator_original' {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) {A B : (CenterMorphismProperty Z).Localization} {gf : A ⟶ B} (h : OriginalWitness Z gf) : mapGenerator Z F hfaith hsieve ⟨gf, GeneratorMorphismData.original h⟩ = F.map h.g

theorem CategoryTheory.Dilatations.H_map_original_generator {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) {A B : (CenterMorphismProperty Z).Localization} {gf : A ⟶ B} (h : OriginalWitness Z gf) : (H Z F hfaith hsieve).map (Quiver.Hom.toPath ⟨gf, GeneratorMorphismData.original h⟩) = F.map h.g

theorem CategoryTheory.Dilatations.GeneratedToLocalization_map_original {C : Type u} [Category.{v, u} C] (Z : Center C) {A B : (CenterMorphismProperty Z).Localization} {gf : A ⟶ B} (h : OriginalWitness Z gf) : (GeneratedToLocalization Z).map (Quiver.Hom.toPath ⟨gf, GeneratorMorphismData.original h⟩) = gf

GeneratedToLocalization sends an original generator to itself.

theorem CategoryTheory.Dilatations.generatedLocalization_commutes_fraction_core {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) (hobj : ∀ (A : GeneratedCategory Z), ((H Z F hfaith hsieve).comp (ImageCenterLocalizationFunctor Z F)).obj A = ((GeneratedToLocalization Z).comp (localizationMap Z F)).obj A) (i : Z.I) (X : C) (n : X ⟶ Z.cod i) (hn : (Z.N i).arrows n) : (ImageCenterLocalizationFunctor Z F).map (uniqueFactor Z F hfaith hsieve i X n hn) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((localizationMap Z F).map (fractionInLocalization Z ⟨i, ⟨X, ⟨n, hn⟩⟩⟩)) (eqToHom ⋯))

Core cancellation step for the fraction case : matching the two sides of generatedLocalization_commutes after both have been rewritten via H_map_fraction / GeneratedToLocalization_map_fraction, using that L(F(d_i)) is (tautologically) invertible in the image-center localization.

theorem CategoryTheory.Dilatations.generatedLocalization_commutes {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) : (H Z F hfaith hsieve).comp (ImageCenterLocalizationFunctor Z F) = (GeneratedToLocalization Z).comp (localizationMap Z F)

theorem CategoryTheory.Dilatations.H_descends {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) {X Y : GeneratedCategory Z} (f g : X ⟶ Y) : DilaRel Z f g → (H Z F hfaith hsieve).map f = (H Z F hfaith hsieve).map g

H sends DilaRel-related paths to equal morphisms of D: the second, global use of Σ-regularity, by injectivity after post-composing with ImageCenterLocalizationFunctor Z F.

noncomputable def CategoryTheory.Dilatations.DilaLift {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) : Functor (Dila Z) D

Theorem 3.10, the functor F'. The functor Dila Z ⥤ D factoring F through Θ = CatToDila Z, built structurally : the generator-by-generator choice generatorImage, lifted to the free category as H, descends along the quotient by DilaRel via H_descends. Its defining equation F' ∘ Θ = F is DilaLift_fac; its uniqueness is DilaLift_unique.

Equations

• CategoryTheory.Dilatations.DilaLift Z F hfaith hsieve = CategoryTheory.Quotient.lift (CategoryTheory.Dilatations.DilaRel Z) (CategoryTheory.Dilatations.H Z F hfaith hsieve) ⋯

theorem CategoryTheory.Dilatations.DilaLift_fac {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) : (CatToDila Z).comp (DilaLift Z F hfaith hsieve) = F

Theorem 3.10, existence half. F' ∘ Θ = F.

theorem CategoryTheory.Dilatations.exists_Dila_factor {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) : ∃ (G : Functor (Dila Z) D), (CatToDila Z).comp G = F

theorem CategoryTheory.Dilatations.Dila_factor_unique_on_C {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (G₁ G₂ : Functor (Dila Z) D) (h₁ : (CatToDila Z).comp G₁ = F) (h₂ : (CatToDila Z).comp G₂ = F) : (CatToDila Z).comp G₁ = (CatToDila Z).comp G₂

theorem CategoryTheory.Dilatations.map_eq_of_agree_on_C {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) {X Y : C} (G₁ G₂ : Functor (Dila Z) D) (h₁ : (CatToDila Z).comp G₁ = F) (h₂ : (CatToDila Z).comp G₂ = F) (f : X ⟶ Y) : G₁.map ((CatToDila Z).map f) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (G₂.map ((CatToDila Z).map f)) (eqToHom ⋯))

theorem CategoryTheory.Dilatations.imageCenter_mono {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (i : Z.I) : Mono (F.map (Z.mor i))

Sigma-regularity makes every mapped denominator a monomorphism.

theorem CategoryTheory.Dilatations.Dila_factor_unique_fraction {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (G₁ G₂ : Functor (Dila Z) D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (h₁ : (CatToDila Z).comp G₁ = F) (h₂ : (CatToDila Z).comp G₂ = F) (i : Z.I) (X : C) (n : X ⟶ Z.cod i) (hn : (Z.N i).arrows n) : G₁.map (fractionInDilatation Z ⟨i, ⟨X, ⟨n, hn⟩⟩⟩) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (G₂.map (fractionInDilatation Z ⟨i, ⟨X, ⟨n, hn⟩⟩⟩)) (eqToHom ⋯))

theorem CategoryTheory.Dilatations.Subtype.ext_val {α : Type u_1} {p : α → Prop} {a b : Subtype p} (h : ↑a = ↑b) : a = b

theorem CategoryTheory.Dilatations.Subtype.val_eq_of_eq {α : Type u_1} {p : α → Prop} {a b : Subtype p} (h : a = b) : ↑a = ↑b

theorem CategoryTheory.Dilatations.GeneratorQuiver_Hom_ext {C : Type u} [Category.{v, u} C] (Z : Center C) {X Y : GeneratorObjects Z} (g₁ g₂ : X ⟶ Y) (h : g₁.fst = g₂.fst) : (GeneratedToDila Z).map g₁.toPath = (GeneratedToDila Z).map g₂.toPath

theorem CategoryTheory.Dilatations.Generated_factor_unique_generator {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (G₁ G₂ : Functor (Dila Z) D) (h_obj : ∀ (X : Dila Z), G₁.obj X = G₂.obj X) (h_mor : ∀ {X Y : C} (f : X ⟶ Y), G₁.map ((CatToDila Z).map f) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (G₂.map ((CatToDila Z).map f)) (eqToHom ⋯))) (h_fraction : ∀ (i : Z.I) (X : C) (n : X ⟶ Z.cod i) (hn : (Z.N i).arrows n), G₁.map (fractionInDilatation Z ⟨i, ⟨X, ⟨n, hn⟩⟩⟩) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (G₂.map (fractionInDilatation Z ⟨i, ⟨X, ⟨n, hn⟩⟩⟩)) (eqToHom ⋯))) {A B : GeneratorObjects Z} (g : A ⟶ B) : G₁.map ((GeneratedToDila Z).map g.toPath) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (G₂.map ((GeneratedToDila Z).map g.toPath)) (eqToHom ⋯))

theorem CategoryTheory.Dilatations.Generated_factor_unique_map {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (G₁ G₂ : Functor (Dila Z) D) (h_obj : ∀ (X : Dila Z), G₁.obj X = G₂.obj X) (h_mor : ∀ {X Y : C} (f : X ⟶ Y), G₁.map ((CatToDila Z).map f) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (G₂.map ((CatToDila Z).map f)) (eqToHom ⋯))) (h_fraction : ∀ (i : Z.I) (X : C) (n : X ⟶ Z.cod i) (hn : (Z.N i).arrows n), G₁.map (fractionInDilatation Z ⟨i, ⟨X, ⟨n, hn⟩⟩⟩) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (G₂.map (fractionInDilatation Z ⟨i, ⟨X, ⟨n, hn⟩⟩⟩)) (eqToHom ⋯))) {X Y : Dila Z} (f : X ⟶ Y) : G₁.map f = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (G₂.map f) (eqToHom ⋯))

theorem CategoryTheory.Dilatations.localization_obj_eq_Q_obj {C : Type u} [Category.{v, u} C] (Z : Center C) (X : (CenterMorphismProperty Z).Localization) : ∃ (Y : C), (CenterMorphismProperty Z).Q.obj Y = X

theorem CategoryTheory.Dilatations.Dila_obj_eq_C_obj {C : Type u} [Category.{v, u} C] (Z : Center C) (X : Dila Z) : ∃ (Y : C), (CatToDila Z).obj Y = X

theorem CategoryTheory.Dilatations.Dila_factor_unique {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (G₁ G₂ : Functor (Dila Z) D) (h₁ : (CatToDila Z).comp G₁ = F) (h₂ : (CatToDila Z).comp G₂ = F) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) : G₁ = G₂

theorem CategoryTheory.Dilatations.DilaLift_unique {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) (G : Functor (Dila Z) D) (hG : (CatToDila Z).comp G = F) : G = DilaLift Z F hfaith hsieve

Theorem 3.10, uniqueness half. Any G with G ∘ Θ = F equals DilaLift.

theorem CategoryTheory.Dilatations.Dila_universal_property {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : (ImageCenterLocalizationFunctor Z F).Faithful) (hsieve : ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))) : ∃! G : Functor (Dila Z) D, (CatToDila Z).comp G = F

def CategoryTheory.Dilatations.IsSigmaRegular {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) : Prop

Definition 3.6. F : C ⥤ D is Σ-regular (F ∈ Cat ^ Σ-reg_C) if D → D[F(Σ)⁻¹] is faithful.

Equations

• CategoryTheory.Dilatations.IsSigmaRegular Z F = (CategoryTheory.Dilatations.ImageCenterMorphismProperty Z F).Q.Faithful

theorem CategoryTheory.Dilatations.faithful_of_comp_faithful {C₁ : Type u} [Category.{v, u} C₁] {C₂ : Type u} [Category.{v, u} C₂] {C₃ : Type u} [Category.{v, u} C₃] (p : Functor C₁ C₂) (e : Functor C₂ C₃) (hfaith : (p.comp e).Faithful) : p.Faithful

If p ⋙ e is faithful, then p is faithful. This is the elementary categorical fact behind both Fact 3.7 and Fact 3.8 : a functor that factors (on the target side) through a faithful functor is itself faithful.

theorem CategoryTheory.Dilatations.CatToDila_isSigmaRegular {C : Type u} [Category.{v, u} C] (Z : Center C) : IsSigmaRegular Z (CatToDila Z)

Fact 3.7. Θ : C ⥤ C' is Σ-regular.

theorem CategoryTheory.Dilatations.CatToDila_comp_image_sieve_le_singleton {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (G : Functor (Dila Z) D) (i : Z.I) : Sieve.functorPushforward ((CatToDila Z).comp G) (Z.N i) ≤ Sieve.generate (Presieve.singleton (((CatToDila Z).comp G).map (Z.mor i)))

Fact 3.11. If G : Dila Z ⥤ D and i : Z.I, then the pushforward of Z.N i along CatToDila Z ⋙ G is contained in the singleton sieve generated by (CatToDila Z ⋙ G).map (Z.mor i). This is CatToDila_image_sieve_le_singleton pushed forward one further step through G.

theorem CategoryTheory.Dilatations.CatToDila_represents {C : Type u} [Category.{v, u} C] (Z : Center C) {D : Type u} [Category.{v', u} D] (F : Functor C D) (hfaith : IsSigmaRegular Z F) : (∃! G : Functor (Dila Z) D, (CatToDila Z).comp G = F) ↔ ∀ (i : Z.I), Sieve.functorPushforward F (Z.N i) ≤ Sieve.generate (Presieve.singleton (F.map (Z.mor i)))