instance proof1.instHasFiniteProductsArtinResAlg {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] : CategoryTheory.Limits.HasFiniteProducts (Deformation.ArtinResAlg Λ)

def proof1.J2_iso {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (r : ℕ) [IsNoetherianRing Λ] : quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)) ≅ fintsze r

Equations

• proof1.J2_iso r = Deformation.ArtinResAlg.ofEquiv (id R2_algEquiv)

def proof1.exists_aux_iso {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (r : ℕ) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] [H2 F] : F.obj (fintsze r) ≅ Fin r → F.obj dualNumber_C

Equations

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

def proof1.linearequiv_map {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (r : ℕ) : ((Fin r → IsLocalRing.ResidueField Λ) →ₗ[IsLocalRing.ResidueField Λ] IsLocalRing.ResidueField Λ) →ₗ[IsLocalRing.ResidueField Λ] (CategoryTheory.coyoneda.obj (Opposite.op (fintsze r))).obj dualNumber_C

Equations

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

def proof1.tszehomlinmap {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {M N : FGModuleCat (IsLocalRing.ResidueField Λ)} (f : Deformation.tsze_C Λ M ⟶ Deformation.tsze_C Λ N) : ↑M →ₗ[IsLocalRing.ResidueField Λ] ↑N

Equations

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

@[simp]

theorem proof1.tszehomlinmap_apply {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {M N : FGModuleCat (IsLocalRing.ResidueField Λ)} (f : Deformation.tsze_C Λ M ⟶ Deformation.tsze_C Λ N) (x : ↑M) : (tszehomlinmap f) x = (TrivSqZeroExt.sndHom (IsLocalRing.ResidueField Λ) ↑N) (f.hom ((TrivSqZeroExt.inrHom (IsLocalRing.ResidueField Λ) ↑M) x))

def proof1.linearequiv {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (r : ℕ) : ((Fin r → IsLocalRing.ResidueField Λ) →ₗ[IsLocalRing.ResidueField Λ] IsLocalRing.ResidueField Λ) ≃ₗ[IsLocalRing.ResidueField Λ] (CategoryTheory.coyoneda.obj (Opposite.op (fintsze r))).obj dualNumber_C

Equations

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

def proof1.finmodulebasis {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (r : ℕ) : Basis (Fin r) (IsLocalRing.ResidueField Λ) ((Fin r → IsLocalRing.ResidueField Λ) →ₗ[IsLocalRing.ResidueField Λ] IsLocalRing.ResidueField Λ)

Equations

• proof1.finmodulebasis r = (Pi.basisFun (IsLocalRing.ResidueField Λ) (Fin r)).dualBasis

def proof1.basis_aux {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (r : ℕ) : Basis (Fin r) (IsLocalRing.ResidueField Λ) ((CategoryTheory.coyoneda.obj (Opposite.op (fintsze r))).obj dualNumber_C)

Equations

• proof1.basis_aux r = (proof1.finmodulebasis r).map (proof1.linearequiv r)

theorem proof1.basis_aux_apply {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (r : ℕ) (x : Fin r) : (basis_aux r) x = Deformation.tsze_functor.map (FGModuleCat.ofHom (LinearMap.proj x))

theorem proof1.inv_piComparison_map_fst {β : Type u_1} {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] (G : CategoryTheory.Functor C D) (f : β → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun (b : β) => G.obj (f b)] (b : β) [CategoryTheory.IsIso (CategoryTheory.Limits.piComparison G f)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.piComparison G f)) (G.map (CategoryTheory.Limits.Pi.π f b)) = CategoryTheory.Limits.Pi.π (fun (b : β) => G.obj (f b)) b

theorem proof1.basis_aux_prop {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (r : ℕ) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] [H2 F] (f : Fin r → F.obj dualNumber_C) (x : Fin r) : F.map ((basis_aux r) x) ((exists_aux_iso F r).inv f) = f x

def proof1.equiv_aux {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (r : ℕ) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] [H2 F] (b : Basis (Fin r) (IsLocalRing.ResidueField Λ) (F.obj dualNumber_C)) : (CategoryTheory.coyoneda.obj (Opposite.op (fintsze r))).obj dualNumber_C ≃ₗ[IsLocalRing.ResidueField Λ] F.obj dualNumber_C

Equations

• proof1.equiv_aux F r b = (proof1.basis_aux r).equiv b (Equiv.refl (Fin r))

theorem proof1.equiv_aux_eq {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (r : ℕ) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] [H2 F] (b : Basis (Fin r) (IsLocalRing.ResidueField Λ) (F.obj dualNumber_C)) : ⇑↑(equiv_aux F r b) = (CategoryTheory.coyonedaEquiv.symm ((exists_aux_iso F r).inv ⇑b)).app dualNumber_C

theorem proof1.exists_xi2' {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (r : ℕ) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] [H2 F] (b : Basis (Fin r) (IsLocalRing.ResidueField Λ) (F.obj dualNumber_C)) : ∃ (x : F.obj (fintsze r)), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)

theorem proof1.exists_xi2 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (r : ℕ) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] [H2 F] [IsNoetherianRing Λ] (b : Basis (Fin r) (IsLocalRing.ResidueField Λ) (F.obj dualNumber_C)) : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)

@[reducible, inline]

abbrev proof1.indStepSet1 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {r : ℕ} (Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)) : Set (Ideal (MvPowerSeries (Fin r) Λ))

Equations

• proof1.indStepSet1 Jq = Set.Icc (IsLocalRing.maximalIdeal (MvPowerSeries (Fin r) Λ) * Jq.ideal) Jq.ideal

instance proof1.instQuotInCMvPowerSeriesFinValIdealMemSetIndStepSet1 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {r : ℕ} (Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)) (J : ↑(indStepSet1 Jq)) : QuotInC ↑J

def proof1.indStepSet2 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)) (x : F.obj (quot_C Λ Jq.ideal)) : Set ↑(indStepSet1 Jq)

Equations

• proof1.indStepSet2 F Jq x = {J : ↑(proof1.indStepSet1 Jq) | ∃ (y : F.obj (quot_C Λ ↑J)), F.map (transitionmap_C Λ ⋯) y = x}

def proof1.embed {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {r : ℕ} (Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)) : ↑(indStepSet1 Jq) ↪o { p : Ideal (MvPowerSeries (Fin r) Λ) // IsLocalRing.maximalIdeal (MvPowerSeries (Fin r) Λ) * Jq.ideal ≤ p }

Equations

• proof1.embed Jq = { toFun := fun (J : ↑(proof1.indStepSet1 Jq)) => ⟨↑J, ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯ }

instance proof1.instQuotInCMvPowerSeriesFinHMulIdealMaximalIdealIdeal {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {r : ℕ} (Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)) : QuotInC (IsLocalRing.maximalIdeal (MvPowerSeries (Fin r) Λ) * Jq.ideal)

instance proof1.instWellFoundedLTElemIdealMvPowerSeriesFinIndStepSet1 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {r : ℕ} [IsNoetherianRing Λ] (Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)) : WellFoundedLT ↑(indStepSet1 Jq)

theorem proof1.nonempty {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)) (x : F.obj (quot_C Λ Jq.ideal)) : (indStepSet2 F Jq x).Nonempty

def proof1.quot_inf_equiv (Λ : Type u) [CommRing Λ] {R : Type u} [CommRing R] [Algebra Λ R] (J K : Ideal R) : (R ⧸ J ⊓ K) ≃ₐ[Λ] ↥(pullbackSubalgebra (Ideal.Quotient.factorₐ Λ ⋯) (Ideal.Quotient.factorₐ Λ ⋯))

Equations

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

theorem proof1.quot_inf_equiv_hom_snd (Λ : Type u) [CommRing Λ] {R : Type u} [CommRing R] [Algebra Λ R] {J K : Ideal R} (x : R ⧸ J ⊓ K) : (↑((quot_inf_equiv Λ J K) x)).2 = (Ideal.Quotient.factor ⋯) x

def proof1.quot_iso {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Algebra Λ R] [IsResidueAlgebra Λ R] (J K : Ideal R) [QuotInC J] [QuotInC K] : quot_C Λ (J ⊓ K) ≅ pullbackinC (transitionmap_C Λ ⋯) (transitionmap_C Λ ⋯)

Equations

• proof1.quot_iso J K = Deformation.ArtinResAlg.ofEquiv (proof1.quot_inf_equiv Λ J K)

theorem proof1.quot_iso_snd {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Algebra Λ R] [IsResidueAlgebra Λ R] {J K : Ideal R} [QuotInC J] [QuotInC K] : CategoryTheory.CategoryStruct.comp (quot_iso J K).hom (sndinC (transitionmap_C Λ ⋯) (transitionmap_C Λ ⋯)) = transitionmap_C Λ ⋯

def proof1.auxmap {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Algebra Λ R] [IsResidueAlgebra Λ R] (J K : Ideal R) [QuotInC J] [QuotInC K] : F.obj (quot_C Λ (J ⊓ K)) ⟶ CategoryTheory.Limits.Types.PullbackObj (F.map (transitionmap_C Λ ⋯)) (F.map (transitionmap_C Λ ⋯))

Equations

• proof1.auxmap F J K = CategoryTheory.CategoryStruct.comp (F.mapIso (proof1.quot_iso J K)).hom (pullbackComparison_spec F (transitionmap_C Λ ⋯) (transitionmap_C Λ ⋯))

theorem proof1.auxmap_hom_snd {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Algebra Λ R] [IsResidueAlgebra Λ R] (J K : Ideal R) [QuotInC J] [QuotInC K] [QuotInC (J ⊔ K)] : F.map (transitionmap_C Λ ⋯) = CategoryTheory.CategoryStruct.comp (auxmap F J K) (CategoryTheory.Limits.Types.pullbackCone (F.map (transitionmap_C Λ ⋯)) (F.map (transitionmap_C Λ ⋯))).snd

theorem proof1.auxmap_surjective {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [H1 F] {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Algebra Λ R] [IsResidueAlgebra Λ R] {J K : Ideal R} [QuotInC J] [QuotInC K] : Function.Surjective (auxmap F J K)

@[reducible, inline]

abbrev proof1.nJq {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {r : ℕ} (Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)) : Submodule (MvPowerSeries (Fin r) Λ) ↥Jq.ideal

Equations

• proof1.nJq Jq = IsLocalRing.maximalIdeal (MvPowerSeries (Fin r) Λ) • ⊤

theorem proof1.Jqtorsion {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {r : ℕ} {Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)} : Module.IsTorsionBySet (MvPowerSeries (Fin r) Λ) (↥Jq.ideal ⧸ nJq Jq) ↑(IsLocalRing.maximalIdeal (MvPowerSeries (Fin r) Λ))

instance proof1.instModuleResidueFieldMvPowerSeriesFinQuotientSubtypeMemIdealIdealSubmoduleNJq {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {r : ℕ} {Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)} : Module (IsLocalRing.ResidueField (MvPowerSeries (Fin r) Λ)) (↥Jq.ideal ⧸ nJq Jq)

Equations

• proof1.instModuleResidueFieldMvPowerSeriesFinQuotientSubtypeMemIdealIdealSubmoduleNJq = ⋯.module

instance proof1.instIsScalarTowerMvPowerSeriesFinResidueFieldQuotientSubtypeMemIdealIdealSubmoduleNJq {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {r : ℕ} {Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)} : IsScalarTower (MvPowerSeries (Fin r) Λ) (IsLocalRing.ResidueField (MvPowerSeries (Fin r) Λ)) (↥Jq.ideal ⧸ nJq Jq)

def proof1.Submodule.extendScalarsOfSurjectiveEquiv {R : Type u_1} {S' : Type u_2} [CommSemiring R] [Semiring S'] [Algebra R S'] {M : Type u_3} [AddCommMonoid M] [Module R M] [Module S' M] [IsScalarTower R S' M] (h : Function.Surjective ⇑(algebraMap R S')) : Submodule R M ≃o Submodule S' M

If R →+* S' is surjective, then S'-linear maps between modules are exactly R-linear maps.

Equations

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

@[reducible, inline]

abbrev proof1.Submodule.extendScalarsOfSurjective {R : Type u_1} {S' : Type u_2} [CommSemiring R] [Semiring S'] [Algebra R S'] {M : Type u_3} [AddCommMonoid M] [Module R M] [Module S' M] [IsScalarTower R S' M] (h : Function.Surjective ⇑(algebraMap R S')) (l : Submodule R M) : Submodule S' M

If R →+* S' is surjective, then R-linear maps are also S'-linear.

Equations

• proof1.Submodule.extendScalarsOfSurjective h l = (proof1.Submodule.extendScalarsOfSurjectiveEquiv h) l

def proof1.exists_sum_Jq_aux_iso {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {r : ℕ} {Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)} : ↑(indStepSet1 Jq) ≃o Submodule (IsLocalRing.ResidueField (MvPowerSeries (Fin r) Λ)) (↥Jq.ideal ⧸ nJq Jq)

Equations

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

def proof1.le_stable {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] {Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)} {x : F.obj (quot_C Λ Jq.ideal)} (J : ↑(indStepSet2 F Jq x)) (K : ↑(indStepSet1 Jq)) (h : ↑J ≤ K) : ↑(indStepSet2 F Jq x)

Equations

• proof1.le_stable J K h = ⟨K, ⋯⟩

instance proof1.instFactLeIdealMvPowerSeriesFinHMulMaximalIdealIdeal {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {r : ℕ} (Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)) : Fact (IsLocalRing.maximalIdeal (MvPowerSeries (Fin r) Λ) * Jq.ideal ≤ Jq.ideal)

theorem proof1.exists_sum_Jq {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] {Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)} {x : F.obj (quot_C Λ Jq.ideal)} (J K : ↑(indStepSet2 F Jq x)) : ∃ (J' : ↑(indStepSet2 F Jq x)), ↑↑J' ⊓ ↑↑K = ↑↑J ⊓ ↑↑K ∧ ↑↑J' ⊔ ↑↑K = Jq.ideal

def proof1.intersection_stable {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] [H1 F] {Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)} {x : F.obj (quot_C Λ Jq.ideal)} (J K : ↑(indStepSet2 F Jq x)) : ↑(indStepSet2 F Jq x)

Equations

• proof1.intersection_stable J K = ⟨⟨↑↑J ⊓ ↑↑K, ⋯⟩, ⋯⟩

theorem proof1.indStepExists {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] [H1 F] (Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)) (x : F.obj (quot_C Λ Jq.ideal)) : ∃ J ∈ indStepSet2 F Jq x, ∀ (I : ↑(indStepSet2 F Jq x)), ↑J ≤ ↑↑I

def proof1.inddef {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] [H1 F] (Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)) (x : F.obj (quot_C Λ Jq.ideal)) : (J : QuotCIdeal (MvPowerSeries (Fin r) Λ)) × F.obj (quot_C Λ J.ideal)

Equations

• proof1.inddef F Jq x = ⟨{ ideal := ↑⋯.choose, quotinc := ⋯ }, Exists.choose ⋯⟩

theorem proof1.inddef_2 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] [H1 F] (Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)) (x : F.obj (quot_C Λ Jq.ideal)) : (inddef F Jq x).fst.ideal ≤ Jq.ideal

theorem proof1.inddef_1 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] [H1 F] (Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)) (x : F.obj (quot_C Λ Jq.ideal)) : IsLocalRing.maximalIdeal (MvPowerSeries (Fin r) Λ) * Jq.ideal ≤ (inddef F Jq x).fst.ideal

theorem proof1.inddef_3 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] [H1 F] (Jq : QuotCIdeal (MvPowerSeries (Fin r) Λ)) (x : F.obj (quot_C Λ Jq.ideal)) : F.map (transitionmap_C Λ ⋯) (inddef F Jq x).snd = x

def proof1.pairs {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] : ℕ → (J : QuotCIdeal (MvPowerSeries (Fin r) Λ)) × F.obj (quot_C Λ J.ideal)

Equations

• proof1.pairs F hr 0 = ⟨{ ideal := denom_ideal Λ (MvPowerSeries (Fin r) Λ), quotinc := ⋯ }, hr.choose⟩
• proof1.pairs F hr n.succ = proof1.inddef F (proof1.pairs F hr n).fst (proof1.pairs F hr n).snd

@[simp]

theorem proof1.pairs_0_ideal {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] : (pairs F hr 0).fst.ideal = denom_ideal Λ (MvPowerSeries (Fin r) Λ)

@[reducible, inline]

abbrev proof1.ideals {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] (n : ℕ) : Ideal (MvPowerSeries (Fin r) Λ)

Equations

• proof1.ideals F hr n = (proof1.pairs F hr n).fst.ideal

@[reducible, inline]

abbrev proof1.quotients {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] (n : ℕ) : Deformation.ArtinResAlg Λ

Equations

• proof1.quotients F hr n = quot_C Λ (proof1.pairs F hr n).fst.ideal

theorem proof1.pairs_antitone {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] : Antitone (ideals F hr)

@[reducible, inline]

abbrev proof1.transmap {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] {n m : ℕ} (h : n ≤ m) : quotients F hr m ⟶ quotients F hr n

Equations

• proof1.transmap F hr h = transitionmap_C Λ ⋯

@[simp]

theorem proof1.pairs_compatible {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] (m n : ℕ) (hnm : n ≤ m) : F.map (transmap F hr hnm) (pairs F hr m).snd = (pairs F hr n).snd

@[simp]

theorem proof1.pairs_compatible' {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] (m n : ℕ) (hnm : ideals F hr m ≤ ideals F hr n) : F.map (transitionmap_C Λ hnm) (pairs F hr m).snd = (pairs F hr n).snd

theorem proof1.maxideal_le {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] (n : ℕ) : IsLocalRing.maximalIdeal (MvPowerSeries (Fin r) Λ) ^ (n + 2) ≤ (pairs F hr n).fst.ideal

instance proof1.tangentiso {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] : CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm (pairs F hr 0).snd).app dualNumber_C)

def proof1.ideal {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] : Ideal (MvPowerSeries (Fin r) Λ)

Equations

• proof1.ideal F hr = iInf (proof1.ideals F hr)

instance proof1.instNontrivialQuotientMvPowerSeriesFinIdealIdeal {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] : Nontrivial (MvPowerSeries (Fin r) Λ ⧸ ideal F hr)

instance proof1.instIsCompleteQuotientMvPowerSeriesFinIdealIdeal {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] : Deformation.IsComplete (MvPowerSeries (Fin r) Λ ⧸ ideal F hr)

@[reducible, inline]

abbrev proof1.R {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] : Deformation.ProArtinResAlg Λ

Equations

• proof1.R F hr = Deformation.ProArtinResAlg.of Λ (MvPowerSeries (Fin r) Λ ⧸ proof1.ideal F hr)

def proof1.quot_mk_S_R {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] : Deformation.ProArtinResAlg.of Λ (MvPowerSeries (Fin r) Λ) ⟶ R F hr

Equations

• proof1.quot_mk_S_R F hr = Deformation.ProArtinResAlg.ofHom (Ideal.Quotient.mkₐ Λ (proof1.ideal F hr))

def proof1.procouple {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] : Procouple F

Equations

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

theorem proof1.procouple_fst {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] : (procouple F hr).fst = R F hr

instance proof1.instIsLocalHomQuotientIdealRingHomFactorOfIsLocalRingOfNontrivial_schlessinger {R : Type u_1} [CommRing R] [IsLocalRing R] {I J : Ideal R} [Nontrivial (R ⧸ I)] [Nontrivial (R ⧸ J)] (h : I ≤ J) : IsLocalHom (Ideal.Quotient.factor h)

instance proof1.instIsLocalHomQuotientIdealAlgHomFactorₐOfIsLocalRingOfNontrivial_schlessinger {Λ : Type u} [CommRing Λ] {R : Type u_1} [CommRing R] [Algebra Λ R] [IsLocalRing R] {I J : Ideal R} [Nontrivial (R ⧸ I)] [Nontrivial (R ⧸ J)] (h : I ≤ J) : IsLocalHom (Ideal.Quotient.factorₐ Λ h)

def proof1.map_R_ideals {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] (n : ℕ) : R F hr ⟶ Deformation.inclusionFunctor.obj (quotients F hr n)

Equations

• proof1.map_R_ideals hr n = Deformation.ProArtinResAlg.ofHom (Ideal.Quotient.factorₐ Λ ⋯)

def proof1.map_R_ideals' {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] (n : ℕ) : R F hr ⟶ Deformation.inclusionFunctor.obj (quotients F hr n)

Equations

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

theorem proof1.map_R_ideals'_eq {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] (n : ℕ) : map_R_ideals hr n = map_R_ideals' hr n

@[simp]

theorem proof1.map_R_ideals_mk {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] (n : ℕ) (x : MvPowerSeries (Fin r) Λ) : (map_R_ideals hr n).hom ((Ideal.Quotient.mk (ideal F hr)) x) = (Ideal.Quotient.mk (pairs F hr n).fst.ideal) x

@[simp]

theorem proof1.procouple_snd {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] (n : ℕ) : (nattrans_of F (procouple F hr).snd).app (quotients F hr n) (map_R_ideals hr n) = (pairs F hr n).snd

theorem proof1.homkeps_max_sq_zero {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (X : Deformation.ProArtinResAlg Λ) (f : X ⟶ Deformation.inclusionFunctor.obj dualNumber_C) (x : ↥(IsLocalRing.maximalIdeal ↑X ^ 2)) : f.hom ↑x = 0

theorem proof1.homkeps_map_zero {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (X : Deformation.ProArtinResAlg Λ) (f : X ⟶ Deformation.inclusionFunctor.obj dualNumber_C) (x : ↥(Ideal.map (algebraMap Λ ↑X) (IsLocalRing.maximalIdeal Λ))) : f.hom ↑x = 0

theorem proof1.homkeps_denom_le_ker {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (X : Deformation.ProArtinResAlg Λ) (f : X ⟶ Deformation.inclusionFunctor.obj dualNumber_C) : denom_ideal Λ ↑X ≤ RingHom.ker f.hom

noncomputable def proof1.prop2_hom {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] : (hR (R F hr)).obj dualNumber_C → (CategoryTheory.coyoneda.obj (Opposite.op (quotients F hr 0))).obj dualNumber_C

Equations

• proof1.prop2_hom F hr u = Deformation.ArtinResAlg.ofHom (Ideal.Quotient.liftₐ (proof1.pairs F hr 0).fst.ideal (CategoryTheory.CategoryStruct.comp (proof1.quot_mk_S_R F hr) u).hom ⋯)

theorem proof1.prop2_hom_comp {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] (f : (hR (R F hr)).obj dualNumber_C) : f = CategoryTheory.CategoryStruct.comp (map_R_ideals hr 0) (Deformation.inclusionFunctor.map (prop2_hom F hr f))

noncomputable def proof1.prop2_inv {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] : (CategoryTheory.coyoneda.obj (Opposite.op (quotients F hr 0))).obj dualNumber_C → (hR (R F hr)).obj dualNumber_C

Equations

• proof1.prop2_inv F hr u = CategoryTheory.CategoryStruct.comp (proof1.map_R_ideals hr 0) (Deformation.inclusionFunctor.map u)

noncomputable def proof1.prop2_iso {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] : (hR (R F hr)).obj dualNumber_C ≅ (CategoryTheory.coyoneda.obj (Opposite.op (quotients F hr 0))).obj dualNumber_C

Equations

• proof1.prop2_iso F hr = { hom := proof1.prop2_hom F hr, inv := proof1.prop2_inv F hr, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem proof1.prop2_iso_comm {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] : CategoryTheory.CategoryStruct.comp (prop2_iso F hr).hom ((CategoryTheory.coyonedaEquiv.symm (pairs F hr 0).snd).app dualNumber_C) = (nattrans_of F (procouple F hr).snd).app dualNumber_C

instance proof1.prop2 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] : CategoryTheory.IsIso ((nattrans_of F (procouple F hr).snd).app dualNumber_C)

theorem proof1.suff1 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) {η : F.obj A'} (comm : (nattrans_of F (procouple F hr).snd).app A u = F.map p η) [IsSmallExtension p] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] [H2 F] (h : ∃ (u' : R F hr ⟶ Deformation.inclusionFunctor.obj A'), CategoryTheory.CategoryStruct.comp u' (Deformation.inclusionFunctor.map p) = u) : ∃ (z : (hR (procouple F hr).fst).obj A'), (hR (procouple F hr).fst).map p z = u ∧ (nattrans_of F (procouple F hr).snd).app A' z = η

def proof1.u_S {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] {A : Deformation.ArtinResAlg Λ} (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) : MvPowerSeries (Fin r) Λ →ₐ[Λ] ↑A

Equations

• proof1.u_S hr u = u.hom.comp (Ideal.Quotient.mkₐ Λ (proof1.ideal F hr))

instance proof1.instIsLocalHomCarrierRObjArtinResAlgProArtinResAlgInclusionFunctorAlgHomHom {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] {A : Deformation.ArtinResAlg Λ} (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) : IsLocalHom u.hom

theorem proof1.exist_factor {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A : Deformation.ArtinResAlg Λ} (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) : ∃ (q : ℕ), ideals F hr q ≤ RingHom.ker (u_S hr u)

def proof1.u_fac {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A : Deformation.ArtinResAlg Λ} (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) : quotients F hr ⋯.choose ⟶ A

Equations

• proof1.u_fac hr u = Deformation.ArtinResAlg.ofHom (Ideal.Quotient.liftₐ (proof1.pairs F hr ⋯.choose).fst.ideal (proof1.u_S hr u) ⋯)

theorem proof1.u_fac_eq {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A : Deformation.ArtinResAlg Λ} (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) : CategoryTheory.CategoryStruct.comp (map_R_ideals hr ⋯.choose) (Deformation.inclusionFunctor.map (u_fac hr u)) = u

theorem proof1.comm' {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) {η : F.obj A'} (comm : (nattrans_of F (procouple F hr).snd).app A u = F.map p η) : F.map (u_fac hr u) (pairs F hr ⋯.choose).snd = F.map p η

theorem proof1.suff2 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) (h : ∃ (v : quotients F hr ⋯.choose.succ ⟶ A'), CategoryTheory.CategoryStruct.comp v p = CategoryTheory.CategoryStruct.comp (transmap F hr ⋯) (u_fac hr u)) : ∃ (u' : R F hr ⟶ Deformation.inclusionFunctor.obj A'), CategoryTheory.CategoryStruct.comp u' (Deformation.inclusionFunctor.map p) = u

theorem proof1.issmall_aux_lem {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) (x : ↑(pullbackinC (u_fac hr u) p)) : x ∈ RingHom.ker (fstinC (u_fac hr u) p).hom ↔ (↑x).1 = 0 ∧ (↑x).2 ∈ RingHom.ker p.hom

def proof1.issmall_aux_equiv {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) : ↥(RingHom.ker (fstinC (u_fac hr u) p).hom) ≃ₗ[Λ] ↥(RingHom.ker p.hom)

Equations

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

instance proof1.instIsSmallExtensionFstinCU_fac {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) [small : IsSmallExtension p] : IsSmallExtension (fstinC (u_fac hr u) p)

theorem proof1.surj_fst {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) : Function.Surjective ⇑(fstinC (u_fac hr u) p).hom

theorem proof1.exist_w {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) (i : Fin r) : ∃ (y : ↑(pullbackinC (u_fac hr u) p)), (fstinC (u_fac hr u) p).hom y = (Ideal.Quotient.mk (pairs F hr ⋯.choose).fst.ideal) (MvPowerSeries.X i)

def proof1.pre_w {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) (i : Fin r) : ↑(pullbackinC (u_fac hr u) p)

Equations

• proof1.pre_w hr p surj u i = ⋯.choose

@[simp]

theorem proof1.pre_w_def {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) (i : Fin r) : (fstinC (u_fac hr u) p).hom (pre_w hr p surj u i) = (Ideal.Quotient.mk (pairs F hr ⋯.choose).fst.ideal) (MvPowerSeries.X i)

def proof1.instUniformSpaceCarrier {Λ : Type u} [CommRing Λ] (X : Deformation.ArtinResAlg Λ) : UniformSpace ↑X

Equations

• proof1.instUniformSpaceCarrier X = ⊥

theorem proof1.instDiscreteUniformityCarrier {Λ : Type u} [CommRing Λ] (X : Deformation.ArtinResAlg Λ) : DiscreteUniformity ↑X

theorem proof1.instCompleteSpaceCarrier {Λ : Type u} [CommRing Λ] (X : Deformation.ArtinResAlg Λ) : CompleteSpace ↑X

theorem proof1.hasEval_pre_w {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) : MvPowerSeries.HasEval (pre_w hr p surj u)

theorem proof1.instContinuousSMulCarrier {Λ : Type u} [CommRing Λ] (X : Deformation.ArtinResAlg Λ) : ContinuousSMul Λ ↑X

def proof1.w {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) : MvPowerSeries (Fin r) Λ →ₐ[Λ] ↑(pullbackinC (u_fac hr u) p)

Equations

• proof1.w hr p surj u = MvPowerSeries.aeval ⋯

theorem proof1.w_def' {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) : (fstinC (u_fac hr u) p).hom.comp (w hr p surj u) = Ideal.Quotient.mkₐ Λ (pairs F hr ⋯.choose).fst.ideal

theorem proof1.w_def {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) (x : MvPowerSeries (Fin r) Λ) : (↑((w hr p surj u) x)).1 = (Ideal.Quotient.mk (pairs F hr ⋯.choose).fst.ideal) x

instance proof1.instIsLocalHomMvPowerSeriesFinCarrierPullbackinCU_facAlgHomW {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) : IsLocalHom (w hr p surj u)

def proof1.w_C {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) : Deformation.ProArtinResAlg.of Λ (MvPowerSeries (Fin r) Λ) ⟶ Deformation.inclusionFunctor.obj (pullbackinC (u_fac hr u) p)

Equations

• proof1.w_C hr p surj u = Deformation.ProArtinResAlg.ofHom (proof1.w hr p surj u)

theorem proof1.w_prop {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) : CategoryTheory.CategoryStruct.comp (w_C hr p surj u) (Deformation.inclusionFunctor.map (fstinC (u_fac hr u) p)) = proartin_quot_mk (ideals F hr ⋯.choose)

theorem proof1.surj_w_fst {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) : Function.Surjective ⇑(CategoryTheory.CategoryStruct.comp (w_C hr p surj u) (Deformation.inclusionFunctor.map (fstinC (u_fac hr u) p))).hom

theorem proof1.suff3 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) (h : ∃ (v : quotients F hr ⋯.choose.succ ⟶ pullbackinC (u_fac hr u) p), CategoryTheory.CategoryStruct.comp v (fstinC (u_fac hr u) p) = transmap F hr ⋯) : ∃ (v : quotients F hr ⋯.choose.succ ⟶ A'), CategoryTheory.CategoryStruct.comp v p = CategoryTheory.CategoryStruct.comp (transmap F hr ⋯) (u_fac hr u)

theorem proof1.suff4' {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) (h : ideals F hr (⋯.choose + 1) ≤ RingHom.ker (w_C hr p surj u).hom) : ∃ (v : quotients F hr ⋯.choose.succ ⟶ pullbackinC (u_fac hr u) p), CategoryTheory.CategoryStruct.comp v (fstinC (u_fac hr u) p) = transmap F hr ⋯

theorem proof1.mem_indstepset1 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) [IsSmallExtension p] : RingHom.ker (w_C hr p surj u).hom ∈ indStepSet1 { ideal := ideals F hr ⋯.choose, quotinc := ⋯ }

def proof1.ker_indstepset1 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) [IsSmallExtension p] : ↑(indStepSet1 { ideal := ideals F hr ⋯.choose, quotinc := ⋯ })

Equations

• proof1.ker_indstepset1 hr p surj u = ⟨RingHom.ker (proof1.w_C hr p surj u).hom, ⋯⟩

theorem proof1.exists_lift {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) {η : F.obj A'} (comm' : F.map (u_fac hr u) (pairs F hr ⋯.choose).snd = F.map p η) [IsSmallExtension p] : ∃ (x : F.obj (pullbackinC (u_fac hr u) p)), F.map (fstinC (u_fac hr u) p) x = (pairs F hr ⋯.choose).snd

def proof1.iso_ker_of_surj {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) [IsSmallExtension p] (h : Function.Surjective ⇑(w_C hr p surj u).hom) : quot_C Λ ↑(ker_indstepset1 hr p surj u) ≅ pullbackinC (u_fac hr u) p

Equations

• proof1.iso_ker_of_surj hr p surj u h = Deformation.ArtinResAlg.ofEquiv (Ideal.quotientKerAlgEquivOfSurjective h)

theorem proof1.iso_ker_of_surj_def {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) [IsSmallExtension p] (h : Function.Surjective ⇑(w_C hr p surj u).hom) : CategoryTheory.CategoryStruct.comp (proartin_quot_mk ↑(ker_indstepset1 hr p surj u)) (Deformation.inclusionFunctor.map (iso_ker_of_surj hr p surj u h).hom) = w_C hr p surj u

theorem proof1.iso_ker_of_surj_comp {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) [IsSmallExtension p] (h : Function.Surjective ⇑(w_C hr p surj u).hom) : CategoryTheory.CategoryStruct.comp (iso_ker_of_surj hr p surj u h).inv (transitionmap_C Λ ⋯) = fstinC (u_fac hr u) p

theorem proof1.mem_indstepset2 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) {η : F.obj A'} (comm' : F.map (u_fac hr u) (pairs F hr ⋯.choose).snd = F.map p η) [IsSmallExtension p] (h : Function.Surjective ⇑(w_C hr p surj u).hom) : ker_indstepset1 hr p surj u ∈ indStepSet2 F { ideal := ideals F hr ⋯.choose, quotinc := ⋯ } (pairs F hr ⋯.choose).snd

theorem proof1.suff4 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] {A' A : Deformation.ArtinResAlg Λ} (p : A' ⟶ A) (surj : Function.Surjective ⇑p.hom) (u : R F hr ⟶ Deformation.inclusionFunctor.obj A) {η : F.obj A'} (comm' : F.map (u_fac hr u) (pairs F hr ⋯.choose).snd = F.map p η) [IsSmallExtension p] : ∃ (v : quotients F hr ⋯.choose.succ ⟶ pullbackinC (u_fac hr u) p), CategoryTheory.CategoryStruct.comp v (fstinC (u_fac hr u) p) = transmap F hr ⋯

theorem proof1.prop1 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {r : ℕ} [IsNoetherianRing Λ] (hr : ∃ (x : F.obj (quot_C Λ (denom_ideal Λ (MvPowerSeries (Fin r) Λ)))), CategoryTheory.IsIso ((CategoryTheory.coyonedaEquiv.symm x).app dualNumber_C)) [H1 F] [Deformation.IsComplete Λ] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] [H2 F] : IsSmooth (nattrans_of F (procouple F hr).snd)

theorem proof1.ishull {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsNoetherianRing Λ] [H1 F] [Deformation.IsComplete Λ] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] [H2 F] [H3 F] : IsHull F (procouple F ⋯)