noncomputable def inversediagramJ {Λ : Type u} [CommRing Λ] {A : Deformation.ProArtinResAlg Λ} (J : ℕ → Ideal ↑A) [∀ (n : ℕ), QuotInC (J n)] (h : Antitone J) : CategoryTheory.Functor ℕᵒᵖ (Deformation.ArtinResAlg Λ)

For a decreasing sequence of ideals J such that the quotients are in ArtinResAlg Λ, the diagram with objects A / (J n)

Equations

• inversediagramJ J h = { obj := fun (n : ℕᵒᵖ) => quot_C Λ (J (Opposite.unop n)), map := fun {X Y : ℕᵒᵖ} (f : X ⟶ Y) => transitionmap_C Λ ⋯, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem inversediagramJ_map {Λ : Type u} [CommRing Λ] {A : Deformation.ProArtinResAlg Λ} (J : ℕ → Ideal ↑A) [∀ (n : ℕ), QuotInC (J n)] (h : Antitone J) {X✝ Y✝ : ℕᵒᵖ} (f : X✝ ⟶ Y✝) : (inversediagramJ J h).map f = transitionmap_C Λ ⋯

@[simp]

theorem inversediagramJ_obj_carrier {Λ : Type u} [CommRing Λ] {A : Deformation.ProArtinResAlg Λ} (J : ℕ → Ideal ↑A) [∀ (n : ℕ), QuotInC (J n)] (h : Antitone J) (n : ℕᵒᵖ) : ↑((inversediagramJ J h).obj n) = (↑A ⧸ J (Opposite.unop n))

@[reducible, inline]

noncomputable abbrev inversediagram {Λ : Type u} [CommRing Λ] (A : Deformation.ProArtinResAlg Λ) : CategoryTheory.Functor ℕᵒᵖ (Deformation.ArtinResAlg Λ)

The diagram in ArtinResAlg Λ with objects A / (maximalIdeal A ^ n.succ)

Equations

• inversediagram A = inversediagramJ (fun (n : ℕ) => IsLocalRing.maximalIdeal ↑A ^ n.succ) ⋯

@[simp]

theorem inversediagram_map_hom_apply {Λ : Type u} [CommRing Λ] (A : Deformation.ProArtinResAlg Λ) {X✝ Y✝ : ℕᵒᵖ} (f : X✝ ⟶ Y✝) (a✝ : ↑A ⧸ (fun (n : ℕ) => IsLocalRing.maximalIdeal ↑A ^ n.succ) (Opposite.unop X✝)) : ((inversediagram A).map f).hom a✝ = (Ideal.Quotient.factorₐ ↑A ⋯) a✝

@[simp]

theorem inversediagram_obj_carrier {Λ : Type u} [CommRing Λ] (A : Deformation.ProArtinResAlg Λ) (n : ℕᵒᵖ) : ↑((inversediagram A).obj n) = (↑A ⧸ IsLocalRing.maximalIdeal ↑A ^ (Opposite.unop n + 1))

@[reducible, inline]

abbrev CategoryTheory.Functor.completion_obj' {Λ : Type u} [CommRing Λ] (F : Functor (Deformation.ArtinResAlg Λ) (Type u)) (A : Deformation.ProArtinResAlg Λ) : Type u

object part of the extension of a functor F by taking the projective limit of the F (A/m^n)

Equations

• F.completion_obj' A = CategoryTheory.Limits.limit ((inversediagram A).comp F)

@[reducible, inline]

abbrev CategoryTheory.Functor.completionJ {Λ : Type u} [CommRing Λ] (F : Functor (Deformation.ArtinResAlg Λ) (Type u)) {A : Deformation.ProArtinResAlg Λ} (J : ℕ → Ideal ↑A) [∀ (n : ℕ), QuotInC (J n)] (h : Antitone J) : Type u

similarly to the extension of a functor F, for any decreasing sequence of ideals J inducing quotients in ArtinResAlg Λ, the projective limit of the F (A/ J n)

Equations

• F.completionJ J h = CategoryTheory.Limits.limit ((inversediagramJ J h).comp F)

@[simp]

theorem limit_π_transitionmap_C {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {A : Deformation.ProArtinResAlg Λ} (J : ℕ → Ideal ↑A) [∀ (n : ℕ), QuotInC (J n)] (hJ : Antitone J) (i j : ℕ) (hij : J i ≤ J j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((inversediagramJ J hJ).comp F) (Opposite.op i)) (F.map (transitionmap_C Λ hij)) = CategoryTheory.Limits.limit.π ((inversediagramJ J hJ).comp F) (Opposite.op j)

@[simp]

theorem limit_π_transitionmap_C_apply {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {A : Deformation.ProArtinResAlg Λ} (J : ℕ → Ideal ↑A) [∀ (n : ℕ), QuotInC (J n)] (hJ : Antitone J) (i j : ℕ) (hij : J i ≤ J j) (x : F.completionJ J hJ) : F.map (transitionmap_C Λ hij) (CategoryTheory.Limits.limit.π ((inversediagramJ J hJ).comp F) (Opposite.op i) x) = CategoryTheory.Limits.limit.π ((inversediagramJ J hJ).comp F) (Opposite.op j) x

def inversediagram_map {Λ : Type u} [CommRing Λ] {A B : Deformation.ProArtinResAlg Λ} (f : A ⟶ B) : inversediagram A ⟶ inversediagram B

Equations

• inversediagram_map f = { app := fun (n : ℕᵒᵖ) => quot_maxideal_C_map f.hom (Opposite.unop n), naturality := ⋯ }

@[simp]

theorem inversediagram_map_app {Λ : Type u} [CommRing Λ] {A B : Deformation.ProArtinResAlg Λ} (f : A ⟶ B) (n : ℕᵒᵖ) : (inversediagram_map f).app n = quot_maxideal_C_map f.hom (Opposite.unop n)

@[simp]

theorem inversediagram_map_id {Λ : Type u} [CommRing Λ] {A : Deformation.ProArtinResAlg Λ} : inversediagram_map (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (inversediagram A)

@[simp]

theorem inversediagram_map_comp {Λ : Type u} [CommRing Λ] {A B C : Deformation.ProArtinResAlg Λ} (f : A ⟶ B) (g : B ⟶ C) : inversediagram_map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (inversediagram_map f) (inversediagram_map g)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Functor.completion_map' {Λ : Type u} [CommRing Λ] (F : Functor (Deformation.ArtinResAlg Λ) (Type u)) {A B : Deformation.ProArtinResAlg Λ} (f : A ⟶ B) : F.completion_obj' A ⟶ F.completion_obj' B

map part of the extension of a functor F by taking the projective limit of (F A/m^n)

Equations

• F.completion_map' f = CategoryTheory.Limits.limMap (CategoryTheory.Functor.whiskerRight (inversediagram_map f) F)

noncomputable def CategoryTheory.Functor.completion {Λ : Type u} [CommRing Λ] (F : Functor (Deformation.ArtinResAlg Λ) (Type u)) : Functor (Deformation.ProArtinResAlg Λ) (Type u)

extend a functor F by taking the projective limit of the family F (A/m^n)

Equations

• F.completion = { obj := F.completion_obj', map := fun {X Y : Deformation.ProArtinResAlg Λ} => F.completion_map', map_id := ⋯, map_comp := ⋯ }

noncomputable def CategoryTheory.NatTrans.completion {Λ : Type u} [CommRing Λ] {F G : Functor (Deformation.ArtinResAlg Λ) (Type u)} (η : F ⟶ G) : F.completion ⟶ G.completion

Equations

• CategoryTheory.NatTrans.completion η = { app := fun (X : Deformation.ProArtinResAlg Λ) => CategoryTheory.Limits.limMap ((inversediagram X).whiskerLeft η), naturality := ⋯ }

noncomputable def completionFunctor {Λ : Type u} [CommRing Λ] : CategoryTheory.Functor (CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (CategoryTheory.Functor (Deformation.ProArtinResAlg Λ) (Type u))

Equations

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

noncomputable def limitcone_of_eventually_iso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (G : CategoryTheory.Functor ℕᵒᵖ C) (n : ℕᵒᵖ) (h : ∀ (m : ℕᵒᵖ) (f : m ⟶ n), CategoryTheory.IsIso (G.map f)) : CategoryTheory.Limits.LimitCone G

Equations

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

@[simp]

theorem limitcone_of_eventually_iso_cone_pt (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (G : CategoryTheory.Functor ℕᵒᵖ C) (n : ℕᵒᵖ) (h : ∀ (m : ℕᵒᵖ) (f : m ⟶ n), CategoryTheory.IsIso (G.map f)) : (limitcone_of_eventually_iso C G n h).cone.pt = G.obj n

@[simp]

theorem limitcone_of_eventually_iso_isLimit_lift (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (G : CategoryTheory.Functor ℕᵒᵖ C) (n : ℕᵒᵖ) (h : ∀ (m : ℕᵒᵖ) (f : m ⟶ n), CategoryTheory.IsIso (G.map f)) (s : CategoryTheory.Limits.Cone G) : (limitcone_of_eventually_iso C G n h).isLimit.lift s = s.π.app n

@[simp]

theorem limitcone_of_eventually_iso_cone_π_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (G : CategoryTheory.Functor ℕᵒᵖ C) (n : ℕᵒᵖ) (h : ∀ (m : ℕᵒᵖ) (f : m ⟶ n), CategoryTheory.IsIso (G.map f)) (m : ℕᵒᵖ) : (limitcone_of_eventually_iso C G n h).cone.π.app m = if f : Opposite.unop m ≤ Opposite.unop n then G.map (CategoryTheory.opHomOfLE f) else CategoryTheory.inv (G.map (CategoryTheory.opHomOfLE ⋯))

def artin_inversediagram_cone {Λ : Type u} [CommRing Λ] (A : Deformation.ArtinResAlg Λ) : CategoryTheory.Limits.Cone (inversediagram (Deformation.inclusionFunctor.obj A))

Equations

• artin_inversediagram_cone A = { pt := A, π := { app := fun (n : ℕᵒᵖ) => Deformation.ArtinResAlg.ofHom (Ideal.Quotient.mkₐ Λ (maxideal (↑A) (Opposite.unop n))), naturality := ⋯ } }

@[simp]

theorem artin_inversediagram_cone_π_app_hom_apply {Λ : Type u} [CommRing Λ] (A : Deformation.ArtinResAlg Λ) (n : ℕᵒᵖ) (a : ↑A) : ((artin_inversediagram_cone A).π.app n).hom a = (Ideal.Quotient.mk (maxideal (↑A) (Opposite.unop n))) a

@[simp]

theorem artin_inversediagram_cone_pt {Λ : Type u} [CommRing Λ] (A : Deformation.ArtinResAlg Λ) : (artin_inversediagram_cone A).pt = A

def auxequiv {Λ : Type u} [CommRing Λ] (A : Deformation.ArtinResAlg Λ) (n : ℕ) (hn : IsLocalRing.maximalIdeal ↑A ^ (n + 1) = 0) : ↑((inversediagram (Deformation.inclusionFunctor.obj A)).obj (Opposite.op n)) ≃ₐ[Λ] ↑A

Equations

• auxequiv A n hn = (Ideal.quotientEquivAlgOfEq Λ ⋯).trans (AlgEquiv.quotientBot Λ ↑(Deformation.inclusionFunctor.obj A))

theorem isiso_transitionmap {Λ : Type u} [CommRing Λ] (A : Deformation.ArtinResAlg Λ) (n : ℕ) (hn : IsLocalRing.maximalIdeal ↑A ^ (n + 1) = 0) (m : ℕ) (hmn : m ≥ n) : CategoryTheory.IsIso (transitionmap_C Λ ⋯)

noncomputable def completion_iso_n {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (A : Deformation.ArtinResAlg Λ) (n : ℕ) (hn : IsLocalRing.maximalIdeal ↑A ^ (n + 1) = 0) : F.completion.obj (Deformation.inclusionFunctor.obj A) ≅ F.obj A

Equations

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

noncomputable def completion_iso {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (A : Deformation.ArtinResAlg Λ) : F.completion.obj (Deformation.inclusionFunctor.obj A) ≅ F.obj A

Equations

• completion_iso F A = completion_iso_n F A (Exists.choose ⋯) ⋯

@[simp]

theorem completion_iso_inv_π {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (A : Deformation.ArtinResAlg Λ) (n : ℕᵒᵖ) : CategoryTheory.CategoryStruct.comp (completion_iso F A).inv (CategoryTheory.Limits.limit.π ((inversediagram (Deformation.inclusionFunctor.obj A)).comp F) n) = F.map ((artin_inversediagram_cone A).π.app n)

noncomputable def natiso_completion {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) : F ≅ Deformation.inclusionFunctor.comp F.completion

Equations

• natiso_completion F = CategoryTheory.NatIso.ofComponents (fun (x : Deformation.ArtinResAlg Λ) => (completion_iso F x).symm) ⋯

@[simp]

theorem completion_iso_map_hom {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {X Y : Deformation.ArtinResAlg Λ} (f : X ⟶ Y) (x : F.completion.obj (Deformation.inclusionFunctor.obj X)) : (completion_iso F Y).hom (F.completion.map (Deformation.inclusionFunctor.map f) x) = F.map f ((completion_iso F X).hom x)

theorem antitone_sup_maxideal {Λ : Type u} [CommRing Λ] (A : Deformation.ProArtinResAlg Λ) (J : Ideal ↑A) : Antitone fun (n : ℕ) => J ⊔ IsLocalRing.maximalIdeal ↑A ^ n.succ

noncomputable def quot_quot_iso {Λ : Type u} [CommRing Λ] (A : Deformation.ProArtinResAlg Λ) (J : Ideal ↑A) [Nontrivial (↑A ⧸ J)] (n : ℕ) : quot_C Λ (IsLocalRing.maximalIdeal (↑A ⧸ J) ^ (n + 1)) ≅ quot_C Λ (J ⊔ IsLocalRing.maximalIdeal ↑A ^ (n + 1))

Equations

• quot_quot_iso A J n = Deformation.ArtinResAlg.ofEquiv ((Ideal.quotientEquivAlgOfEq Λ ⋯).trans (DoubleQuot.quotQuotEquivQuotSupₐ Λ J (IsLocalRing.maximalIdeal ↑A ^ (n + 1))))

noncomputable def inversediagram_quot_iso {Λ : Type u} [CommRing Λ] (A : Deformation.ProArtinResAlg Λ) (J : Ideal ↑A) [Nontrivial (↑A ⧸ J)] [Deformation.IsComplete (↑A ⧸ J)] : inversediagram (Deformation.ProArtinResAlg.of Λ (↑A ⧸ J)) ≅ inversediagramJ (fun (n : ℕ) => J ⊔ IsLocalRing.maximalIdeal ↑A ^ n.succ) ⋯

Equations

• inversediagram_quot_iso A J = CategoryTheory.NatIso.ofComponents (fun (n : ℕᵒᵖ) => quot_quot_iso A J (Opposite.unop n)) ⋯

noncomputable def completion_quot_iso {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (A : Deformation.ProArtinResAlg Λ) (J : Ideal ↑A) [Nontrivial (↑A ⧸ J)] [Deformation.IsComplete (↑A ⧸ J)] : F.completion.obj (Deformation.ProArtinResAlg.of Λ (↑A ⧸ J)) ≅ F.completionJ (fun (n : ℕ) => J ⊔ IsLocalRing.maximalIdeal ↑A ^ n.succ) ⋯

Equations

• completion_quot_iso F A J = CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.Functor.isoWhiskerRight (inversediagram_quot_iso A J) F)

@[simp]

theorem completion_quot_iso_hom_π {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (A : Deformation.ProArtinResAlg Λ) (J : Ideal ↑A) [Nontrivial (↑A ⧸ J)] [Deformation.IsComplete (↑A ⧸ J)] (j : ℕᵒᵖ) : CategoryTheory.CategoryStruct.comp (completion_quot_iso F A J).hom (CategoryTheory.Limits.limit.π ((inversediagramJ (fun (n : ℕ) => J ⊔ IsLocalRing.maximalIdeal ↑A ^ n.succ) ⋯).comp F) j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((inversediagram (Deformation.ProArtinResAlg.of Λ (↑A ⧸ J))).comp F) j) (F.map (quot_quot_iso A J (Opposite.unop j)).hom)

@[simp]

theorem completion_quot_iso_hom_π_apply {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (A : Deformation.ProArtinResAlg Λ) (J : Ideal ↑A) [Nontrivial (↑A ⧸ J)] [Deformation.IsComplete (↑A ⧸ J)] (j : ℕᵒᵖ) (x : F.completion.obj (Deformation.ProArtinResAlg.of Λ (↑A ⧸ J))) : CategoryTheory.Limits.limit.π ((inversediagramJ (fun (n : ℕ) => J ⊔ IsLocalRing.maximalIdeal ↑A ^ n.succ) ⋯).comp F) j ((completion_quot_iso F A J).hom x) = F.map (quot_quot_iso A J (Opposite.unop j)).hom (CategoryTheory.Limits.limit.π ((inversediagram (Deformation.ProArtinResAlg.of Λ (↑A ⧸ J))).comp F) j x)

@[simp]

theorem completion_quot_iso_inv_π {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (A : Deformation.ProArtinResAlg Λ) (J : Ideal ↑A) [Nontrivial (↑A ⧸ J)] [Deformation.IsComplete (↑A ⧸ J)] (j : ℕᵒᵖ) : CategoryTheory.CategoryStruct.comp (completion_quot_iso F A J).inv (CategoryTheory.Limits.limit.π ((inversediagram (Deformation.ProArtinResAlg.of Λ (↑A ⧸ J))).comp F) j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((inversediagramJ (fun (n : ℕ) => J ⊔ IsLocalRing.maximalIdeal ↑A ^ n.succ) ⋯).comp F) j) (F.map (quot_quot_iso A J (Opposite.unop j)).inv)

@[simp]

theorem completion_quot_iso_inv_π_apply {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (A : Deformation.ProArtinResAlg Λ) (J : Ideal ↑A) [Nontrivial (↑A ⧸ J)] [Deformation.IsComplete (↑A ⧸ J)] (j : ℕᵒᵖ) (x : F.completionJ (fun (n : ℕ) => J ⊔ IsLocalRing.maximalIdeal ↑A ^ n.succ) ⋯) : CategoryTheory.Limits.limit.π ((inversediagram (Deformation.ProArtinResAlg.of Λ (↑A ⧸ J))).comp F) j ((completion_quot_iso F A J).inv x) = F.map (quot_quot_iso A J (Opposite.unop j)).inv (CategoryTheory.Limits.limit.π ((inversediagramJ (fun (n : ℕ) => J ⊔ IsLocalRing.maximalIdeal ↑A ^ n.succ) ⋯).comp F) j x)

noncomputable def completion_cone_of_le {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {A : Deformation.ProArtinResAlg Λ} {I J : ℕ → Ideal ↑A} [∀ (n : ℕ), QuotInC (I n)] (hI : Antitone I) [∀ (n : ℕ), QuotInC (J n)] (hJ : Antitone J) (hIJ : ∀ (n : ℕ), ∃ (m : ℕ), I m ≤ J n) : CategoryTheory.Limits.Cone ((inversediagramJ J hJ).comp F)

Equations

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

@[simp]

theorem completion_cone_of_le_pt {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {A : Deformation.ProArtinResAlg Λ} {I J : ℕ → Ideal ↑A} [∀ (n : ℕ), QuotInC (I n)] (hI : Antitone I) [∀ (n : ℕ), QuotInC (J n)] (hJ : Antitone J) (hIJ : ∀ (n : ℕ), ∃ (m : ℕ), I m ≤ J n) : (completion_cone_of_le F hI hJ hIJ).pt = F.completionJ I hI

@[simp]

theorem completion_cone_of_le_π_app {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {A : Deformation.ProArtinResAlg Λ} {I J : ℕ → Ideal ↑A} [∀ (n : ℕ), QuotInC (I n)] (hI : Antitone I) [∀ (n : ℕ), QuotInC (J n)] (hJ : Antitone J) (hIJ : ∀ (n : ℕ), ∃ (m : ℕ), I m ≤ J n) (j : ℕᵒᵖ) (a✝ : ((CategoryTheory.Functor.const ℕᵒᵖ).obj (F.completionJ I hI)).obj j) : (completion_cone_of_le F hI hJ hIJ).π.app j a✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((inversediagramJ I hI).comp F) (Opposite.op ⋯.choose)) (F.map (transitionmap_C Λ ⋯)) a✝

noncomputable def completion_map_of_le {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {A : Deformation.ProArtinResAlg Λ} {I J : ℕ → Ideal ↑A} [∀ (n : ℕ), QuotInC (I n)] (hI : Antitone I) [∀ (n : ℕ), QuotInC (J n)] (hJ : Antitone J) (hIJ : ∀ (n : ℕ), ∃ (m : ℕ), I m ≤ J n) : F.completionJ I hI ⟶ F.completionJ J hJ

Equations

• completion_map_of_le F hI hJ hIJ = CategoryTheory.Limits.limit.lift ((inversediagramJ J hJ).comp F) (completion_cone_of_le F hI hJ hIJ)

@[simp]

theorem completion_map_of_le_π {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {A : Deformation.ProArtinResAlg Λ} {I J : ℕ → Ideal ↑A} [∀ (n : ℕ), QuotInC (I n)] (hI : Antitone I) [∀ (n : ℕ), QuotInC (J n)] (hJ : Antitone J) (hIJ : ∀ (n : ℕ), ∃ (m : ℕ), I m ≤ J n) (j : ℕ) : CategoryTheory.CategoryStruct.comp (completion_map_of_le F hI hJ hIJ) (CategoryTheory.Limits.limit.π ((inversediagramJ J hJ).comp F) (Opposite.op j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((inversediagramJ I hI).comp F) (Opposite.op ⋯.choose)) (F.map (transitionmap_C Λ ⋯))

@[simp]

theorem completion_map_of_le_π_apply {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {A : Deformation.ProArtinResAlg Λ} {I J : ℕ → Ideal ↑A} [∀ (n : ℕ), QuotInC (I n)] (hI : Antitone I) [∀ (n : ℕ), QuotInC (J n)] (hJ : Antitone J) (hIJ : ∀ (n : ℕ), ∃ (m : ℕ), I m ≤ J n) (j : ℕ) (x : F.completionJ I hI) : CategoryTheory.Limits.limit.π ((inversediagramJ J hJ).comp F) (Opposite.op j) (completion_map_of_le F hI hJ hIJ x) = F.map (transitionmap_C Λ ⋯) (CategoryTheory.Limits.limit.π ((inversediagramJ I hI).comp F) (Opposite.op ⋯.choose) x)

@[simp]

theorem completion_map_of_le_le_id {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {A : Deformation.ProArtinResAlg Λ} {I J : ℕ → Ideal ↑A} [∀ (n : ℕ), QuotInC (I n)] (hI : Antitone I) [∀ (n : ℕ), QuotInC (J n)] (hJ : Antitone J) (hIJ : ∀ (n : ℕ), ∃ (m : ℕ), I m ≤ J n) (hJI : ∀ (n : ℕ), ∃ (m : ℕ), J m ≤ I n) : CategoryTheory.CategoryStruct.comp (completion_map_of_le F hI hJ hIJ) (completion_map_of_le F hJ hI hJI) = CategoryTheory.CategoryStruct.id (F.completionJ I hI)

@[simp]

theorem completion_map_of_le_le_id_apply {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {A : Deformation.ProArtinResAlg Λ} {I J : ℕ → Ideal ↑A} [∀ (n : ℕ), QuotInC (I n)] (hI : Antitone I) [∀ (n : ℕ), QuotInC (J n)] (hJ : Antitone J) (hIJ : ∀ (n : ℕ), ∃ (m : ℕ), I m ≤ J n) (hJI : ∀ (n : ℕ), ∃ (m : ℕ), J m ≤ I n) (x : F.completionJ I hI) : completion_map_of_le F hJ hI hJI (completion_map_of_le F hI hJ hIJ x) = x

noncomputable def completion_iso_of_le_ge {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {A : Deformation.ProArtinResAlg Λ} {I J : ℕ → Ideal ↑A} [∀ (n : ℕ), QuotInC (I n)] (hI : Antitone I) [∀ (n : ℕ), QuotInC (J n)] (hJ : Antitone J) (hIJ : ∀ (n : ℕ), ∃ (m : ℕ), I m ≤ J n) (hJI : ∀ (n : ℕ), ∃ (m : ℕ), J m ≤ I n) : F.completionJ I hI ≅ F.completionJ J hJ

Equations

• completion_iso_of_le_ge F hI hJ hIJ hJI = { hom := completion_map_of_le F hI hJ hIJ, inv := completion_map_of_le F hJ hI hJI, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem completion_iso_of_le_ge_inv {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {A : Deformation.ProArtinResAlg Λ} {I J : ℕ → Ideal ↑A} [∀ (n : ℕ), QuotInC (I n)] (hI : Antitone I) [∀ (n : ℕ), QuotInC (J n)] (hJ : Antitone J) (hIJ : ∀ (n : ℕ), ∃ (m : ℕ), I m ≤ J n) (hJI : ∀ (n : ℕ), ∃ (m : ℕ), J m ≤ I n) (a✝ : F.completionJ J hJ) : (completion_iso_of_le_ge F hI hJ hIJ hJI).inv a✝ = completion_map_of_le F hJ hI hJI a✝

@[simp]

theorem completion_iso_of_le_ge_hom {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {A : Deformation.ProArtinResAlg Λ} {I J : ℕ → Ideal ↑A} [∀ (n : ℕ), QuotInC (I n)] (hI : Antitone I) [∀ (n : ℕ), QuotInC (J n)] (hJ : Antitone J) (hIJ : ∀ (n : ℕ), ∃ (m : ℕ), I m ≤ J n) (hJI : ∀ (n : ℕ), ∃ (m : ℕ), J m ≤ I n) (a✝ : F.completionJ I hI) : (completion_iso_of_le_ge F hI hJ hIJ hJI).hom a✝ = completion_map_of_le F hI hJ hIJ a✝