Restriction, composition, and union of centers

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

def CategoryTheory.Dilatations.Center.restrict {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) : Center C

Proposition 3.14, setup. The restriction of Z to a subcollection K ⊂ Z.I.

Equations

• Z.restrict K hK = { I := ↑K, nonempty := ⋯, dom := fun (k : ↑K) => Z.dom ↑k, cod := fun (k : ↑K) => Z.cod ↑k, mor := fun (k : ↑K) => Z.mor ↑k, N := fun (k : ↑K) => Z.N ↑k }

theorem CategoryTheory.Dilatations.CenterMorphismProperty_restrict_le {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) : CenterMorphismProperty (Z.restrict K hK) ≤ CenterMorphismProperty Z

Γ := {d_i}_{i ∈ K} is a subcollection of Σ := {d_i}_{i ∈ I} as MorphismPropertys.

noncomputable def CategoryTheory.Dilatations.baseRestrictFunctor {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) : Functor (CenterMorphismProperty (Z.restrict K hK)).Localization (CenterMorphismProperty Z).Localization

The localization functor induced by inclusion of a restricted set of denominators.

Equations

• CategoryTheory.Dilatations.baseRestrictFunctor Z K hK = CategoryTheory.Localization.Construction.lift (CategoryTheory.Dilatations.CenterMorphismProperty Z).Q ⋯

theorem CategoryTheory.Dilatations.ImageCenterMorphismProperty_restrict_le {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) : ImageCenterMorphismProperty (Z.restrict K hK) (CatToDila Z) ≤ ImageCenterMorphismProperty Z (CatToDila Z)

theorem CategoryTheory.Dilatations.CatToDila_isSigmaRegular_restrict {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) : IsSigmaRegular (Z.restrict K hK) (CatToDila Z)

theorem CategoryTheory.Dilatations.CatToDila_restrict_hsieve {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) (k : (Z.restrict K hK).I) : Sieve.functorPushforward (CatToDila Z) ((Z.restrict K hK).N k) ≤ Sieve.generate (Presieve.singleton ((CatToDila Z).map ((Z.restrict K hK).mor k)))

noncomputable def CategoryTheory.Dilatations.restrictPhi {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) : Functor (Dila (Z.restrict K hK)) (Dila Z)

Proposition 3.14. The canonical functor Φ : C[{dᵢ}_{i∈K}] ⥤ C[{dᵢ}_{i∈I}].

Equations

• CategoryTheory.Dilatations.restrictPhi Z K hK = CategoryTheory.Dilatations.DilaLift (Z.restrict K hK) (CategoryTheory.Dilatations.CatToDila Z) ⋯ ⋯

theorem CategoryTheory.Dilatations.restrictPhi_spec {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) : (CatToDila (Z.restrict K hK)).comp (restrictPhi Z K hK) = CatToDila Z

theorem CategoryTheory.Dilatations.faithful_of_comp_faithful_gen {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

Universe-polymorphic version of faithful_of_comp_faithful, with independent universes for each of the three categories.

theorem CategoryTheory.Dilatations.isoMorphismProperty_Q_faithful {E : Type u} [Category.{v', u} E] (W : MorphismProperty E) (hW : ∀ ⦃X Y : E⦄ (f : X ⟶ Y), W f → IsIso f) : W.Q.Faithful

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

Z's own raw localization functor is always Z-regular — every Z-generator is already inverted by .Q (Q_inverts), so isoMorphismProperty_Q_faithful applies directly.

theorem CategoryTheory.Dilatations.LocalizationFunctor_isSigmaRegular_restrict {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) : IsSigmaRegular (Z.restrict K hK) (LocalizationFunctor Z)

theorem CategoryTheory.Dilatations.restrictPhi_comp_DilaToLoc {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) : (restrictPhi Z K hK).comp (DilaToLoc Z) = (DilaToLoc (Z.restrict K hK)).comp (baseRestrictFunctor Z K hK)

theorem CategoryTheory.Dilatations.restrictPhi_faithful {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) (hbase : (baseRestrictFunctor Z K hK).Faithful) : (restrictPhi Z K hK).Faithful

Proposition 3.14 (ii). If C[Γ⁻¹] → C[Σ⁻¹] is faithful, then Φ is faithful.

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

A fraction whose numerator already factors through its denominator is an original morphism.

theorem CategoryTheory.Dilatations.restrictPhi_obj_eq {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) (Y : C) : (restrictPhi Z K hK).obj ((CatToDila (Z.restrict K hK)).obj Y) = (CatToDila Z).obj Y

The basic object-identification : Φ sends the Z.restrict K hK-image of Y to the Z-image of Y, on the nose, via restrictPhi_spec.

theorem CategoryTheory.Dilatations.restrictPhi_full_hobj {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) (X' : GeneratedCategory Z) : (restrictPhi Z K hK).obj ((CatToDila (Z.restrict K hK)).obj ((Localization.Construction.objEquiv (CenterMorphismProperty Z)).symm X')) = (CatToDila Z).obj ((Localization.Construction.objEquiv (CenterMorphismProperty Z)).symm X')

hobj, restated in terms of restrictPhi_obj_eq via the object-equivalence objEquiv.

def CategoryTheory.Dilatations.PhiPreimage {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) {A' B' : GeneratedCategory Z} (p : A' ⟶ B') : Prop

The Φ-preimage predicate used in the induction : p : A' ⟶ B' (in GeneratedCategory Z) has a Φ-preimage among morphisms of Dila (Z.restrict K hK), up to the object-identification restrictPhi_full_hobj.

Equations

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

theorem CategoryTheory.Dilatations.PhiPreimage_id {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) (X' : GeneratedCategory Z) : PhiPreimage Z K hK (CategoryStruct.id X')

Base case : the identity generator has a Φ-preimage (namely the identity).

theorem CategoryTheory.Dilatations.PhiPreimage_comp {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) {X' Y' W' : GeneratedCategory Z} (p : X' ⟶ Y') (q : Y' ⟶ W') (hp : PhiPreimage Z K hK p) (hq : PhiPreimage Z K hK q) : PhiPreimage Z K hK (CategoryStruct.comp p q)

Inductive step : Φ-preimages compose.

theorem CategoryTheory.Dilatations.DilaToLoc_map_fraction {C : Type u} [Category.{v, u} C] (Z : Center C) (p : CenterSievePair Z) : (DilaToLoc Z).map (fractionInDilatation Z p) = fractionInLocalization Z p

DilaToLoc sends a fraction generator back down to the corresponding fraction morphism of the localization.

theorem CategoryTheory.Dilatations.fractionInLocalization_eq {C : Type u} [Category.{v, u} C] (Z : Center C) (p : CenterSievePair Z) : fractionInLocalization Z p = CategoryStruct.comp ((CenterMorphismProperty Z).Q.map ↑p.snd.snd) (Localization.Construction.wInv (Z.mor p.fst) ⋯)

theorem CategoryTheory.Dilatations.baseRestrictFunctor_map_Q {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) {X Y : C} (f : X ⟶ Y) : (baseRestrictFunctor Z K hK).map ((CenterMorphismProperty (Z.restrict K hK)).Q.map f) = (CenterMorphismProperty Z).Q.map f

theorem CategoryTheory.Dilatations.baseRestrictFunctor_map_wInv {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) {X Y : C} (w : X ⟶ Y) (hw : CenterMorphismProperty (Z.restrict K hK) w) : (baseRestrictFunctor Z K hK).map (Localization.Construction.wInv w hw) = Localization.Construction.wInv w ⋯

theorem CategoryTheory.Dilatations.baseRestrictFunctor_map_fraction {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) (i : Z.I) (hiK : i ∈ K) (X0 : C) (n : X0 ⟶ Z.cod i) (hn : (Z.N i).arrows n) : (baseRestrictFunctor Z K hK).map (fractionInLocalization (Z.restrict K hK) ⟨⟨i, hiK⟩, ⟨X0, ⟨n, hn⟩⟩⟩) = fractionInLocalization Z ⟨i, ⟨X0, ⟨n, hn⟩⟩⟩

theorem CategoryTheory.Dilatations.restrictPhi_map_fraction {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) (i : Z.I) (hiK : i ∈ K) (X0 : C) (n : X0 ⟶ Z.cod i) (hn : (Z.N i).arrows n) : (restrictPhi Z K hK).map (fractionInDilatation (Z.restrict K hK) ⟨⟨i, hiK⟩, ⟨X0, ⟨n, hn⟩⟩⟩) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (fractionInDilatation Z ⟨i, ⟨X0, ⟨n, hn⟩⟩⟩) (eqToHom ⋯))

restrictPhi sends the fraction generator of Z.restrict K hK at an index i ∈ K to the corresponding fraction generator of Z at i, up to the object-identification restrictPhi_obj_eq.

theorem CategoryTheory.Dilatations.PhiPreimage_fraction_mem {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) (i : Z.I) (hiK : i ∈ K) (X0 : C) (n : X0 ⟶ Z.cod i) (hn : (Z.N i).arrows n) : PhiPreimage Z K hK (Quiver.Hom.toPath ⟨fractionInLocalization Z ⟨i, ⟨X0, ⟨n, hn⟩⟩⟩, GeneratorMorphismData.fraction { p := ⟨i, ⟨X0, ⟨n, hn⟩⟩⟩, eq := ⋯ }⟩)

Generator case, i ∈ K: a fraction generator indexed by i ∈ K has a Φ-preimage — the corresponding fraction generator of Z.restrict K hK, via restrictPhi_map_fraction.

theorem CategoryTheory.Dilatations.PhiPreimage_original {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) {X0 Y0 : C} (c : X0 ⟶ Y0) : PhiPreimage Z K hK (Quiver.Hom.toPath ⟨(CenterMorphismProperty Z).Q.map c, GeneratorMorphismData.original { g := c, eq := ⋯ }⟩)

Generator case, original morphisms : always has a Φ-preimage.

theorem CategoryTheory.Dilatations.PhiPreimage_fraction_notmem {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) (hI : ∀ i ∉ K, Z.N i = Sieve.generate (Presieve.singleton (Z.mor i))) (i : Z.I) (hiK : i ∉ K) (X0 : C) (n : X0 ⟶ Z.cod i) (hn : (Z.N i).arrows n) : PhiPreimage Z K hK (Quiver.Hom.toPath ⟨fractionInLocalization Z ⟨i, ⟨X0, ⟨n, hn⟩⟩⟩, GeneratorMorphismData.fraction { p := ⟨i, ⟨X0, ⟨n, hn⟩⟩⟩, eq := ⋯ }⟩)

Generator case, i ∉ K: under hI, a fraction generator indexed by i ∉ K reduces to an ordinary morphism, which already has a Φ-preimage.

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

Every object of Dila Z is the CatToDila-image of some object of C.

theorem CategoryTheory.Dilatations.PhiPreimage_edge {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) (hI : ∀ i ∉ K, Z.N i = Sieve.generate (Presieve.singleton (Z.mor i))) {X Y : (CenterMorphismProperty Z).Localization} (e : X ⟶ Y) : PhiPreimage Z K hK e.toPath

A single generator edge always has a Φ-preimage.

theorem CategoryTheory.Dilatations.PhiPreimage_all {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) (hI : ∀ i ∉ K, Z.N i = Sieve.generate (Presieve.singleton (Z.mor i))) {A' B' : GeneratedCategory Z} (p : A' ⟶ B') : PhiPreimage Z K hK p

Every morphism of GeneratedCategory Z has a Φ-preimage : induction on the underlying path, using PhiPreimage_id, PhiPreimage_comp, and PhiPreimage_edge.

theorem CategoryTheory.Dilatations.restrictPhi_full {C : Type u} [Category.{v, u} C] (Z : Center C) (K : Set Z.I) (hK : K.Nonempty) (hI : ∀ i ∉ K, Z.N i = Sieve.generate (Presieve.singleton (Z.mor i))) : (restrictPhi Z K hK).Full

Proposition 3.15

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

Pushing a center W on C forward along a functor F : C ⥤ D gives a center on D, namely {[F(N_j), F(d_j)]}_j.

Equations

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

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

Combining two centers Z and W on the same category C into one center indexed by Z.I ⊕ W.I.

Equations

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

theorem CategoryTheory.Dilatations.CenterMorphismProperty_sum_inl_le {C : Type u} [Category.{v, u} C] (Z W : Center C) : CenterMorphismProperty Z ≤ CenterMorphismProperty (Z.sum W)

theorem CategoryTheory.Dilatations.CenterMorphismProperty_sum_inr_le {C : Type u} [Category.{v, u} C] (Z W : Center C) : CenterMorphismProperty W ≤ CenterMorphismProperty (Z.sum W)

theorem CategoryTheory.Dilatations.ImageCenterMorphismProperty_sum_inl_le {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v', u} D] (Z W : Center C) (F : Functor C D) : ImageCenterMorphismProperty Z F ≤ ImageCenterMorphismProperty (Z.sum W) F

theorem CategoryTheory.Dilatations.ImageCenterMorphismProperty_sum_inr_le {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v', u} D] (Z W : Center C) (F : Functor C D) : ImageCenterMorphismProperty W F ≤ ImageCenterMorphismProperty (Z.sum W) F

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

The dilatation of the Z-part of Z.sum W is regular for CatToDila (Z.sum W): analogous to CatToDila_isSigmaRegular_restrict, but for the Sum.inl-inclusion into Z.sum W instead of a Center.restrict.

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

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

The sieve condition needed to extend CatToDila (Z.sum W) along CatToDila Z.

theorem CategoryTheory.Dilatations.CatToDila_sum_hsieve_inr {C : Type u} [Category.{v, u} C] (Z W : Center C) (j : W.I) : Sieve.functorPushforward (CatToDila (Z.sum W)) (W.N j) ≤ Sieve.generate (Presieve.singleton ((CatToDila (Z.sum W)).map (W.mor j)))

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

Proposition 3.15, setup. The canonical functor Φ : Dila Z ⥤ Dila (Z.sum W), obtained directly from the universal property of Dila Z (Theorem 3.10 / Dila_universal_property) applied to CatToDila (Z.sum W), rather than through Center.restrict/restrictPhi — this avoids having to reindex Z.sum W restricted to its Z-part back to Z, since the two constructions agree by the uniqueness clause of the universal property.

Equations

• CategoryTheory.Dilatations.Phi315 Z W = CategoryTheory.Dilatations.DilaLift Z (CategoryTheory.Dilatations.CatToDila (Z.sum W)) ⋯ ⋯

theorem CategoryTheory.Dilatations.Phi315_spec {C : Type u} [Category.{v, u} C] (Z W : Center C) : (CatToDila Z).comp (Phi315 Z W) = CatToDila (Z.sum W)

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

The pushed-forward center {[Θ(Nj), Θ(dj)]}_{j∈J} living in Dila Z.

Equations

• CategoryTheory.Dilatations.CenterZW Z W = W.pushforward (CategoryTheory.Dilatations.CatToDila Z)

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

β. The dilatation functor for CenterZW.

Equations

• CategoryTheory.Dilatations.Beta315 Z W = CategoryTheory.Dilatations.CatToDila (CategoryTheory.Dilatations.CenterZW Z W)

theorem CategoryTheory.Dilatations.sigma_hom_eq {D : Type u} [Category.{v', u} D] {A A' B B' : D} (hA : A = A') (hB : B = B') (m : A ⟶ B) (m' : A' ⟶ B') (hm : m' = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp m (eqToHom hB))) : ⟨A, ⟨B, m⟩⟩ = ⟨A', ⟨B', m'⟩⟩

A helper for comparing two elements of Σ X Y : D, X ⟶ Y whose objects agree via a (possibly non-trivial) eqToHom-transport of the morphism.

theorem CategoryTheory.Dilatations.ImageCenterMorphismProperty_ZW_Phi_eq {C : Type u} [Category.{v, u} C] (Z W : Center C) : ImageCenterMorphismProperty (CenterZW Z W) (Phi315 Z W) = ImageCenterMorphismProperty W (CatToDila (Z.sum W))

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

Fact 2.14. C[(dᵢ)⁻¹∘Nᵢ] → C[{dᵢ}⁻¹] is faithful.

theorem CategoryTheory.Dilatations.Phi315_isSigmaRegular {C : Type u} [Category.{v, u} C] (Z W : Center C) : IsSigmaRegular (CenterZW Z W) (Phi315 Z W)

Proposition 3.15 (i). Φ belongs to Cat ^ {Θ(dj)}_j-reg_{Dila Z}.

theorem CategoryTheory.Dilatations.functorPushforward_singleton_congr {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v', u} D] {F G : Functor C D} (h : F = G) {X Y : C} (S : Sieve X) (f : Y ⟶ X) (hle : Sieve.functorPushforward G S ≤ Sieve.generate (Presieve.singleton (G.map f))) : Sieve.functorPushforward F S ≤ Sieve.generate (Presieve.singleton (F.map f))

theorem CategoryTheory.Dilatations.Phi315_hsieve {C : Type u} [Category.{v, u} C] (Z W : Center C) (j : (CenterZW Z W).I) : Sieve.functorPushforward (Phi315 Z W) ((CenterZW Z W).N j) ≤ Sieve.generate (Presieve.singleton ((Phi315 Z W).map ((CenterZW Z W).mor j)))

noncomputable def CategoryTheory.Dilatations.Alpha'315 {C : Type u} [Category.{v, u} C] (Z W : Center C) : Functor (Dila (CenterZW Z W)) (Dila (Z.sum W))

Proposition 3.15 (iv), setup. The unique functor α' with Φ = α' ∘ β. Built ahead of Part (ii)/(iii) since Part (ii) depends on Alpha'315_spec.

Equations

• CategoryTheory.Dilatations.Alpha'315 Z W = CategoryTheory.Dilatations.DilaLift (CategoryTheory.Dilatations.CenterZW Z W) (CategoryTheory.Dilatations.Phi315 Z W) ⋯ ⋯

theorem CategoryTheory.Dilatations.Alpha'315_spec {C : Type u} [Category.{v, u} C] (Z W : Center C) : (Beta315 Z W).comp (Alpha'315 Z W) = Phi315 Z W

theorem CategoryTheory.Dilatations.Alpha'315_unique {C : Type u} [Category.{v, u} C] (Z W : Center C) (G : Functor (Dila (CenterZW Z W)) (Dila (Z.sum W))) (hG : (Beta315 Z W).comp G = Phi315 Z W) : G = Alpha'315 Z W

theorem CategoryTheory.Dilatations.Phi315_obj_eq {C : Type u} [Category.{v, u} C] (Z W : Center C) (X : C) : (Phi315 Z W).obj ((CatToDila Z).obj X) = (CatToDila (Z.sum W)).obj X

Φ sends the Θ-image of a C-object to the Θ'-image, on the nose (both Θ ⋙ Φ and Θ' are functors C ⥤ Dila (Z.sum W), so the object part of Phi315_spec needs no eqToHom).

theorem CategoryTheory.Dilatations.Phi315_map_eq {C : Type u} [Category.{v, u} C] (Z W : Center C) {X Y : C} (f : X ⟶ Y) : (Phi315 Z W).map ((CatToDila Z).map f) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((CatToDila (Z.sum W)).map f) (eqToHom ⋯))

The map-level companion of Phi315_obj_eq: since Φ is opaque (built via .choose), this needs the eqToHom-sandwiched form, exactly as in restrictPhi's own object/map lemmas.

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

The "flattened" comparison functor Dila Z → C[{dᵢ}_{I'}⁻¹], obtained by composing Φ with DilaToLoc (Z.sum W).

Equations

• CategoryTheory.Dilatations.comparisonToLocalization Z W = (CategoryTheory.Dilatations.Phi315 Z W).comp (CategoryTheory.Dilatations.DilaToLoc (Z.sum W))

theorem CategoryTheory.Dilatations.comparisonToLocalization_obj {C : Type u} [Category.{v, u} C] (Z W : Center C) (X : C) : (comparisonToLocalization Z W).obj ((CatToDila Z).obj X) = (CenterMorphismProperty (Z.sum W)).Q.obj X

theorem CategoryTheory.Dilatations.comparisonToLocalization_map {C : Type u} [Category.{v, u} C] (Z W : Center C) {X Y : C} (f : X ⟶ Y) : (comparisonToLocalization Z W).map ((CatToDila Z).map f) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((CenterMorphismProperty (Z.sum W)).Q.map f) (eqToHom ⋯))

comparisonToLocalization sends the Θ-image of a C-morphism to its direct image under (CenterMorphismProperty (Z.sum W)).Q, up to the object-identification comparisonToLocalization_obj.

theorem CategoryTheory.Dilatations.comparisonToLocalization_isSigmaRegular {C : Type u} [Category.{v, u} C] (Z W : Center C) : IsSigmaRegular (CenterZW Z W) (comparisonToLocalization Z W)

Part of "Fact 2.14 applied a third time". comparisonToLocalization is regular for CenterZW Z W: its image-center morphism property is exactly the Sum.inr-image of (CenterMorphismProperty (Z.sum W)).Q's own generators (via comparisonToLocalization_map), which are already invertible by MorphismProperty.Q_inverts, so isoMorphismProperty_Q_faithful applies directly — no appeal to Φ's own faithfulness (which is not known) is needed.

theorem CategoryTheory.Dilatations.comparisonToLocalization_comp {C : Type u} [Category.{v, u} C] (Z W : Center C) : (CatToDila Z).comp (comparisonToLocalization Z W) = (CenterMorphismProperty (Z.sum W)).Q

comparisonToLocalization precomposed with Θ is literally (CenterMorphismProperty (Z.sum W)).Q, as a functor equality (both sides C ⥤ (CenterMorphismProperty (Z.sum W)).Localization) — combining Phi315_spec (Θ ⋙ Φ = Θ') with CatToDila_comp_DilaToLoc (Z.sum W).

theorem CategoryTheory.Dilatations.comparisonToLocalization_hsieve {C : Type u} [Category.{v, u} C] (Z W : Center C) (j : (CenterZW Z W).I) : Sieve.functorPushforward (comparisonToLocalization Z W) ((CenterZW Z W).N j) ≤ Sieve.generate (Presieve.singleton ((comparisonToLocalization Z W).map ((CenterZW Z W).mor j)))

The sieve condition needed to extend comparisonToLocalization along CatToDila (CenterZW Z W): (CatToDila Z ⋙ comparisonToLocalization Z W).map (W.mor j) is already an isomorphism, so its generated sieve is the top sieve.

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

The unique extension of comparisonToLocalization along β. By Dila_universal_property (CenterZW Z W) (comparisonToLocalization Z W) comparisonToLocalization_isSigmaRegular comparisonToLocalization_hsieve.

Equations

• CategoryTheory.Dilatations.H315 Z W = Exists.choose ⋯

theorem CategoryTheory.Dilatations.H315_spec {C : Type u} [Category.{v, u} C] (Z W : Center C) : (Beta315 Z W).comp (H315 Z W) = comparisonToLocalization Z W

theorem CategoryTheory.Dilatations.H315_eq {C : Type u} [Category.{v, u} C] (Z W : Center C) : H315 Z W = (Alpha'315 Z W).comp (DilaToLoc (Z.sum W))

H315 agrees with α' ⋙ DilaToLoc (Z.sum W): both extend comparisonToLocalization along β (β ⋙ (α' ⋙ DilaToLoc (Z.sum W)) = (β ⋙ α') ⋙ DilaToLoc (Z.sum W) = Φ ⋙ DilaToLoc (Z.sum W) = comparisonToLocalization, using Alpha'315_spec), so by the uniqueness half of the same universal property used to build H315, they coincide. Alpha'315 only needs Part (i), so this holds unconditionally.

theorem CategoryTheory.Dilatations.BetaComp315_hsieve {C : Type u} [Category.{v, u} C] (Z W : Center C) (k : (Z.sum W).I) : Sieve.functorPushforward ((CatToDila Z).comp (Beta315 Z W)) ((Z.sum W).N k) ≤ Sieve.generate (Presieve.singleton (((CatToDila Z).comp (Beta315 Z W)).map ((Z.sum W).mor k)))

noncomputable def CategoryTheory.Dilatations.Alpha315 {C : Type u} [Category.{v, u} C] (Z W : Center C) (hreg : IsSigmaRegular (Z.sum W) ((CatToDila Z).comp (Beta315 Z W))) : Functor (Dila (Z.sum W)) (Dila (CenterZW Z W))

Proposition 3.15 (iii), setup.

Equations

• CategoryTheory.Dilatations.Alpha315 Z W hreg = Exists.choose ⋯

theorem CategoryTheory.Dilatations.Alpha315_spec {C : Type u} [Category.{v, u} C] (Z W : Center C) (hreg : IsSigmaRegular (Z.sum W) ((CatToDila Z).comp (Beta315 Z W))) : (CatToDila (Z.sum W)).comp (Alpha315 Z W hreg) = (CatToDila Z).comp (Beta315 Z W)

theorem CategoryTheory.Dilatations.Alpha315_unique {C : Type u} [Category.{v, u} C] (Z W : Center C) (hreg : IsSigmaRegular (Z.sum W) ((CatToDila Z).comp (Beta315 Z W))) (G : Functor (Dila (Z.sum W)) (Dila (CenterZW Z W))) (hG : (CatToDila (Z.sum W)).comp G = (CatToDila Z).comp (Beta315 Z W)) : G = Alpha315 Z W hreg

theorem CategoryTheory.Dilatations.IsSigmaRegular_sum_inl_of {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v', u} D] (Z W : Center C) (F : Functor C D) (hF : IsSigmaRegular (Z.sum W) F) : IsSigmaRegular Z F

General form of CatToDila_isSigmaRegular_sum_inl: regularity for the Z-part transfers from regularity of Z.sum W for any target functor F, not just CatToDila (Z.sum W).

theorem CategoryTheory.Dilatations.Phi315_comp_Alpha315 {C : Type u} [Category.{v, u} C] (Z W : Center C) (hreg : IsSigmaRegular (Z.sum W) ((CatToDila Z).comp (Beta315 Z W))) : (Phi315 Z W).comp (Alpha315 Z W hreg) = Beta315 Z W

Proposition 3.15 (v), part 1. Φ ∘ α = β (equivalently Φ ⋙ α = β in Lean's left-to-right composition). Conditional on item 2 (hreg).

theorem CategoryTheory.Dilatations.Alpha315_comp_Alpha'315 {C : Type u} [Category.{v, u} C] (Z W : Center C) (hreg : IsSigmaRegular (Z.sum W) ((CatToDila Z).comp (Beta315 Z W))) : (Alpha315 Z W hreg).comp (Alpha'315 Z W) = Functor.id (Dila (Z.sum W))

Proposition 3.15 (v), part 2 / α ∘ α' = id. Alpha315 Z W ⋙ Alpha'315 Z W = 𝟭 _ (i.e. α' ∘ α = 𝟭 in the paper's right-to-left composition). Conditional on item 2 (hreg).

theorem CategoryTheory.Dilatations.Alpha'315_comp_Alpha315 {C : Type u} [Category.{v, u} C] (Z W : Center C) (hreg : IsSigmaRegular (Z.sum W) ((CatToDila Z).comp (Beta315 Z W))) : (Alpha'315 Z W).comp (Alpha315 Z W hreg) = Functor.id (Dila (CenterZW Z W))

Proposition 3.15 (v), part 3 / α' ∘ α = id. Alpha'315 Z W ⋙ Alpha315 Z W = 𝟭 _ (i.e. α ∘ α' = 𝟭 in the paper's right-to-left composition). Conditional on item 2 (hreg).

noncomputable def CategoryTheory.Dilatations.Iso315 {C : Type u} [Category.{v, u} C] (Z W : Center C) (hreg : IsSigmaRegular (Z.sum W) ((CatToDila Z).comp (Beta315 Z W))) : ↧(Dila (CenterZW Z W)) ≅ ↧(Dila (Z.sum W))

Proposition 3.15 (vi). The mutually-inverse Alpha315 Z W and Alpha'315 Z W assemble into an isomorphism of categories Dila (CenterZW Z W) ≅ Dila (Z.sum W) (as objects of Cat, i.e. a pair of mutually-inverse functors — this needs only hom_inv_id/inv_hom_id, not the fuller coherence of a CategoryTheory.Equivalence). Conditional on item 2 (hreg).

Equations

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

Proposition 3.18

For a fixed center {[Nᵢ,dᵢ]}_{i∈I} on C and an alternative choice of sieves {N'ᵢ}_{i∈I} (same generators dᵢ), the dilatation for the combined two-copy center {[Nᵢ,dᵢ]}_{i∈I}, {[N'ᵢ,dᵢ]}_{i∈I} identifies with the dilatation for the single center with sieves Nᵢ ∪ N'ᵢ.

def CategoryTheory.Dilatations.Center.altSieve {C : Type u} [Category.{v, u} C] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) : Center C

Same generators {dᵢ} as Z, with an alternative choice of sieves N'. Represents {[N'ᵢ,dᵢ]}_{i∈I}.

Equations

• Z.altSieve N' = { I := Z.I, nonempty := ⋯, dom := Z.dom, cod := Z.cod, mor := Z.mor, N := N' }

def CategoryTheory.Dilatations.Center.sieveUnion {C : Type u} [Category.{v, u} C] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) : Center C

Same generators as Z, with sieves Nᵢ ∪ N'ᵢ. Represents {[N''ᵢ,dᵢ]}_{i∈I} from Proposition 3.18.

Equations

• Z.sieveUnion N' = { I := Z.I, nonempty := ⋯, dom := Z.dom, cod := Z.cod, mor := Z.mor, N := fun (i : Z.I) => Z.N i ⊔ N' i }

theorem CategoryTheory.Dilatations.ImageCenterMorphismProperty_altSieve {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v', u} D] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) (F : Functor C D) : ImageCenterMorphismProperty (Z.altSieve N') F = ImageCenterMorphismProperty Z F

theorem CategoryTheory.Dilatations.ImageCenterMorphismProperty_sieveUnion {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v', u} D] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) (F : Functor C D) : ImageCenterMorphismProperty (Z.sieveUnion N') F = ImageCenterMorphismProperty Z F

theorem CategoryTheory.Dilatations.ImageCenterMorphismProperty_sum_altSieve_self {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v', u} D] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) (F : Functor C D) : ImageCenterMorphismProperty (Z.sum (Z.altSieve N')) F = ImageCenterMorphismProperty Z F

The combined two-copy center Z.sum (Z.altSieve N') shares its ImageCenterMorphismProperty with Z alone : both Sum.inl and Sum.inr witnesses reduce to the same underlying generator data, since Z.altSieve N' shares dom/cod/mor with Z.

theorem CategoryTheory.Dilatations.IsSigmaRegular_altSieve {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v', u} D] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) (F : Functor C D) : IsSigmaRegular (Z.altSieve N') F ↔ IsSigmaRegular Z F

theorem CategoryTheory.Dilatations.CenterMorphismProperty_altSieve {C : Type u} [Category.{v, u} C] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) : CenterMorphismProperty (Z.altSieve N') = CenterMorphismProperty Z

noncomputable def CategoryTheory.Dilatations.Fact313Phi {C : Type u} [Category.{v, u} C] (Z : Center C) (M : (i : Z.I) → Sieve (Z.cod i)) (hM : ∀ (i : Z.I), M i ≤ Z.N i) : Functor (Dila (Z.altSieve M)) (Dila Z)

Fact 3.13. For a family of subsieves Mᵢ ⊆ Nᵢ, the canonical comparison functor φ : C[{(dᵢ)⁻¹∘Mᵢ}] ⥤ C[{(dᵢ)⁻¹∘Nᵢ}].

Equations

• CategoryTheory.Dilatations.Fact313Phi Z M hM = Exists.choose ⋯

theorem CategoryTheory.Dilatations.Fact313Phi_spec {C : Type u} [Category.{v, u} C] (Z : Center C) (M : (i : Z.I) → Sieve (Z.cod i)) (hM : ∀ (i : Z.I), M i ≤ Z.N i) : (CatToDila (Z.altSieve M)).comp (Fact313Phi Z M hM) = CatToDila Z

theorem CategoryTheory.Dilatations.Fact313Phi_faithful {C : Type u} [Category.{v, u} C] (Z : Center C) (M : (i : Z.I) → Sieve (Z.cod i)) (hM : ∀ (i : Z.I), M i ≤ Z.N i) : (Fact313Phi Z M hM).Faithful

Fact 3.13. φ is faithful : Dila_factor_unique identifies φ ⋙ DilaToLoc Z with DilaToLoc (Z.altSieve M) (both are the unique factorization of the same raw localization functor, since CenterMorphismProperty doesn't see the sieve component at all), and the latter is always faithful (Fact 2.14).

theorem CategoryTheory.Dilatations.IsSigmaRegular_sieveUnion {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v', u} D] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) (F : Functor C D) : IsSigmaRegular (Z.sieveUnion N') F ↔ IsSigmaRegular Z F

theorem CategoryTheory.Dilatations.IsSigmaRegular_sum_altSieve_self {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v', u} D] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) (F : Functor C D) : IsSigmaRegular (Z.sum (Z.altSieve N')) F ↔ IsSigmaRegular Z F

theorem CategoryTheory.Dilatations.CatToDila_sieveUnion_hsieve {C : Type u} [Category.{v, u} C] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) (i : Z.I) : Sieve.functorPushforward (CatToDila (Z.sum (Z.altSieve N'))) ((Z.sieveUnion N').N i) ≤ Sieve.generate (Presieve.singleton ((CatToDila (Z.sum (Z.altSieve N'))).map ((Z.sieveUnion N').mor i)))

The sieve condition needed to extend CatToDila (Z.sieveUnion N') along CatToDila (Z.sum (Z.altSieve N')) (Fact 3.17, via Sieve.functorPushforward_union, combined with Proposition 3.5 applied to both Z and Z.altSieve N' inside the sum).

noncomputable def CategoryTheory.Dilatations.Alpha318 {C : Type u} [Category.{v, u} C] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) : Functor (Dila (Z.sieveUnion N')) (Dila (Z.sum (Z.altSieve N')))

Proposition 3.18, direction one. The unique functor α : Dila (Z.sieveUnion N') ⥤ Dila (Z.sum (Z.altSieve N')) extending CatToDila (Z.sum (Z.altSieve N')) along CatToDila (Z.sieveUnion N').

Equations

• CategoryTheory.Dilatations.Alpha318 Z N' = Exists.choose ⋯

theorem CategoryTheory.Dilatations.Alpha318_spec {C : Type u} [Category.{v, u} C] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) : (CatToDila (Z.sieveUnion N')).comp (Alpha318 Z N') = CatToDila (Z.sum (Z.altSieve N'))

theorem CategoryTheory.Dilatations.CatToDila_sum_altSieve_hsieve {C : Type u} [Category.{v, u} C] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) (k : Z.I ⊕ Z.I) : Sieve.functorPushforward (CatToDila (Z.sieveUnion N')) ((Z.sum (Z.altSieve N')).N k) ≤ Sieve.generate (Presieve.singleton ((CatToDila (Z.sieveUnion N')).map ((Z.sum (Z.altSieve N')).mor k)))

The sieve condition needed to extend CatToDila (Z.sieveUnion N') along CatToDila (Z.sum (Z.altSieve N')).

noncomputable def CategoryTheory.Dilatations.Alpha'318 {C : Type u} [Category.{v, u} C] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) : Functor (Dila (Z.sum (Z.altSieve N'))) (Dila (Z.sieveUnion N'))

Proposition 3.18, direction two. The unique functor α' : Dila (Z.sum (Z.altSieve N')) ⥤ Dila (Z.sieveUnion N') extending CatToDila (Z.sieveUnion N') along CatToDila (Z.sum (Z.altSieve N')).

Equations

• CategoryTheory.Dilatations.Alpha'318 Z N' = Exists.choose ⋯

theorem CategoryTheory.Dilatations.Alpha'318_spec {C : Type u} [Category.{v, u} C] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) : (CatToDila (Z.sum (Z.altSieve N'))).comp (Alpha'318 Z N') = CatToDila (Z.sieveUnion N')

theorem CategoryTheory.Dilatations.Alpha318_comp_Alpha'318 {C : Type u} [Category.{v, u} C] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) : (Alpha318 Z N').comp (Alpha'318 Z N') = Functor.id (Dila (Z.sieveUnion N'))

theorem CategoryTheory.Dilatations.Alpha'318_comp_Alpha318 {C : Type u} [Category.{v, u} C] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) : (Alpha'318 Z N').comp (Alpha318 Z N') = Functor.id (Dila (Z.sum (Z.altSieve N')))

noncomputable def CategoryTheory.Dilatations.Iso318 {C : Type u} [Category.{v, u} C] (Z : Center C) (N' : (i : Z.I) → Sieve (Z.cod i)) : ↧(Dila (Z.sum (Z.altSieve N'))) ≅ ↧(Dila (Z.sieveUnion N'))

Proposition 3.18. Dila (Z.sum (Z.altSieve N')) (i.e. C[{(dᵢ)⁻¹∘Nᵢ}, {(dᵢ)⁻¹∘N'ᵢ}]) is isomorphic to Dila (Z.sieveUnion N') (i.e. C[{(dᵢ)⁻¹∘(Nᵢ∪N'ᵢ)}]).

Equations

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