Schlessinger.Categories.HasPullbacks

`ArtinResAlg` has pullbacks #

The subalgebra of X × Y defining the pullback of f and g.

def pullbackSubalgebra {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] {Y : Type u} [CommRing Y] [Algebra Λ Y] {Z : Type u} [CommRing Z] [Algebra Λ Z] (f : X →ₐ[Λ] Z) (g : Y →ₐ[Λ] Z) :

Subalgebra Λ (X × Y)

Equations

pullbackSubalgebra f g = { carrier := {(x, y) : X × Y | f x = g y}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

Instances For

source

@[simp]

theorem coe_pullbackSubalgebra {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] {Y : Type u} [CommRing Y] [Algebra Λ Y] {Z : Type u} [CommRing Z] [Algebra Λ Z] (f : X →ₐ[Λ] Z) (g : Y →ₐ[Λ] Z) :

↑(pullbackSubalgebra f g) = {(x, y) : X × Y | f x = g y}

source

@[simp]

theorem mem_pullbackSubalgebra {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] {Y : Type u} [CommRing Y] [Algebra Λ Y] {Z : Type u} [CommRing Z] [Algebra Λ Z] (f : X →ₐ[Λ] Z) (g : Y →ₐ[Λ] Z) (x : X × Y) :

x ∈ pullbackSubalgebra f g ↔ f x.1 = g x.2

source

theorem pullbackprop {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] {Y : Type u} [CommRing Y] [Algebra Λ Y] {Z : Type u} [CommRing Z] [Algebra Λ Z] {f : X →ₐ[Λ] Z} {g : Y →ₐ[Λ] Z} (x : ↥(pullbackSubalgebra f g)) :

f (↑x).1 = g (↑x).2

The first projection from the pullback as an AlgHom.

source

def pullbackSubalgebra_fst {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] {Y : Type u} [CommRing Y] [Algebra Λ Y] {Z : Type u} [CommRing Z] [Algebra Λ Z] (f : X →ₐ[Λ] Z) (g : Y →ₐ[Λ] Z) :

↥(pullbackSubalgebra f g) →ₐ[Λ] X

Equations

pullbackSubalgebra_fst f g = (AlgHom.fst Λ X Y).comp (pullbackSubalgebra f g).val

Instances For

source

@[simp]

theorem pullbackSubalgebra_fst_apply {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] {Y : Type u} [CommRing Y] [Algebra Λ Y] {Z : Type u} [CommRing Z] [Algebra Λ Z] (f : X →ₐ[Λ] Z) (g : Y →ₐ[Λ] Z) (a✝ : ↥(pullbackSubalgebra f g)) :

(pullbackSubalgebra_fst f g) a✝ = (↑a✝).1

The second projection from the pullback as an AlgHom.

source

def pullbackSubalgebra_snd {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] {Y : Type u} [CommRing Y] [Algebra Λ Y] {Z : Type u} [CommRing Z] [Algebra Λ Z] (f : X →ₐ[Λ] Z) (g : Y →ₐ[Λ] Z) :

↥(pullbackSubalgebra f g) →ₐ[Λ] Y

Equations

pullbackSubalgebra_snd f g = (AlgHom.snd Λ X Y).comp (pullbackSubalgebra f g).val

Instances For

source

@[simp]

theorem pullbackSubalgebra_snd_apply {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] {Y : Type u} [CommRing Y] [Algebra Λ Y] {Z : Type u} [CommRing Z] [Algebra Λ Z] (f : X →ₐ[Λ] Z) (g : Y →ₐ[Λ] Z) (a✝ : ↥(pullbackSubalgebra f g)) :

(pullbackSubalgebra_snd f g) a✝ = (↑a✝).2

source

theorem isunit_iff_pullback {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] {Y : Type u} [CommRing Y] [Algebra Λ Y] {Z : Type u} [CommRing Z] [Algebra Λ Z] (f : X →ₐ[Λ] Z) (g : Y →ₐ[Λ] Z) [IsLocalHom f] [IsLocalHom g] (x : ↥(pullbackSubalgebra f g)) :

IsUnit (↑x).1 ↔ IsUnit (↑x).2

source

theorem isunit_iff_fst_pullback {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] {Y : Type u} [CommRing Y] [Algebra Λ Y] {Z : Type u} [CommRing Z] [Algebra Λ Z] (f : X →ₐ[Λ] Z) (g : Y →ₐ[Λ] Z) [IsLocalHom f] [IsLocalHom g] (x : ↥(pullbackSubalgebra f g)) :

IsUnit x ↔ IsUnit (↑x).1

source

instance instIsLocalRingSubtypeProdMemSubalgebraPullbackSubalgebra {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] {Y : Type u} [CommRing Y] [Algebra Λ Y] {Z : Type u} [CommRing Z] [Algebra Λ Z] (f : X →ₐ[Λ] Z) (g : Y →ₐ[Λ] Z) [IsLocalHom f] [IsLocalHom g] [IsLocalRing X] [IsLocalRing Y] [IsLocalRing Z] :

IsLocalRing ↥(pullbackSubalgebra f g)

source

instance instIsLocalHomSubtypeProdMemSubalgebraPullbackSubalgebraRingHomAlgebraMap {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] {Y : Type u} [CommRing Y] [Algebra Λ Y] {Z : Type u} [CommRing Z] [Algebra Λ Z] (f : X →ₐ[Λ] Z) (g : Y →ₐ[Λ] Z) [IsLocalHom f] [IsLocalHom g] [IsLocalHom (algebraMap Λ X)] :

IsLocalHom (algebraMap Λ ↥(pullbackSubalgebra f g))

source

instance isLocalHom_fst {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] {Y : Type u} [CommRing Y] [Algebra Λ Y] {Z : Type u} [CommRing Z] [Algebra Λ Z] (f : X →ₐ[Λ] Z) (g : Y →ₐ[Λ] Z) [IsLocalHom f] [IsLocalHom g] :

IsLocalHom (pullbackSubalgebra_fst f g)

source

instance isLocalHom_snd {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] {Y : Type u} [CommRing Y] [Algebra Λ Y] {Z : Type u} [CommRing Z] [Algebra Λ Z] (f : X →ₐ[Λ] Z) (g : Y →ₐ[Λ] Z) [IsLocalHom f] [IsLocalHom g] :

IsLocalHom (pullbackSubalgebra_snd f g)

source

instance instIsResidueAlgebraSubtypeProdMemSubalgebraPullbackSubalgebra {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] {Y : Type u} [CommRing Y] [Algebra Λ Y] {Z : Type u} [CommRing Z] [Algebra Λ Z] (f : X →ₐ[Λ] Z) (g : Y →ₐ[Λ] Z) [IsLocalHom f] [IsLocalHom g] [IsLocalRing X] [IsResidueAlgebra Λ X] [IsLocalRing Y] [IsLocalRing Z] :

IsResidueAlgebra Λ ↥(pullbackSubalgebra f g)

source

instance instIsArtinianPullback {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] {Y : Type u} [CommRing Y] [Algebra Λ Y] {Z : Type u} [CommRing Z] [Algebra Λ Z] (f : X →ₐ[Λ] Z) (g : Y →ₐ[Λ] Z) [IsLocalRing X] [IsArtinianRing X] [IsResidueAlgebra Λ X] [IsLocalRing Y] [IsArtinianRing Y] [IsResidueAlgebra Λ Y] [IsLocalRing Λ] :

IsArtinianRing ↥(pullbackSubalgebra f g)

The pullback object in ArtinResAlg Λ

source

def pullbackinC {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) :

Deformation.ArtinResAlg Λ

Equations

pullbackinC f g = Deformation.ArtinResAlg.of Λ ↥(pullbackSubalgebra f.hom g.hom)

Instances For

The first projection of the pullback in ArtinResAlg Λ

source

def fstinC {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) :

pullbackinC f g ⟶ X

Equations

fstinC f g = Deformation.ArtinResAlg.ofHom (pullbackSubalgebra_fst f.hom g.hom)

Instances For

source

@[simp]

theorem fstinC_apply {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) (x : ↑(pullbackinC f g)) :

(fstinC f g).hom x = (↑x).1

The second projection of the pullback in ArtinResAlg Λ

source

def sndinC {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) :

pullbackinC f g ⟶ Y

Equations

sndinC f g = Deformation.ArtinResAlg.ofHom (pullbackSubalgebra_snd f.hom g.hom)

Instances For

source

@[simp]

theorem sndinC_apply {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) (x : ↑(pullbackinC f g)) :

(sndinC f g).hom x = (↑x).2

The PullbackCone defining the pullback.

source

def pullbackConeinC {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) :

CategoryTheory.Limits.PullbackCone f g

Equations

pullbackConeinC f g = CategoryTheory.Limits.PullbackCone.mk (fstinC f g) (sndinC f g) ⋯

Instances For

The lift of a PullbackCone over f and g as an AlgHom.

source

def lift_alghom {Λ : Type u} [CommRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} {f : X ⟶ Z} {g : Y ⟶ Z} (s : CategoryTheory.Limits.PullbackCone f g) :

↑s.pt →ₐ[Λ] ↥(pullbackSubalgebra f.hom g.hom)

Equations

lift_alghom s = (s.fst.hom.prod s.snd.hom).codRestrict (pullbackSubalgebra f.hom g.hom) ⋯

Instances For

source

@[simp]

theorem lift_alghom_apply_coe {Λ : Type u} [CommRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} {f : X ⟶ Z} {g : Y ⟶ Z} (s : CategoryTheory.Limits.PullbackCone f g) (n : ↑s.pt) :

↑((lift_alghom s) n) = (s.fst.hom n, s.snd.hom n)

source

@[simp]

theorem fstinC_lift_alghom {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} {f : X ⟶ Z} {g : Y ⟶ Z} (s : CategoryTheory.Limits.PullbackCone f g) (x : ↑s.pt) :

(fstinC f g).hom ((lift_alghom s) x) = s.fst.hom x

source

@[simp]

theorem sndinC_lift_alghom {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} {f : X ⟶ Z} {g : Y ⟶ Z} (s : CategoryTheory.Limits.PullbackCone f g) (x : ↑s.pt) :

(sndinC f g).hom ((lift_alghom s) x) = s.snd.hom x

The lift of a PullbackCone over f and g as an morphism.

source

def pullbackinC_lift {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} {f : X ⟶ Z} {g : Y ⟶ Z} (s : CategoryTheory.Limits.PullbackCone f g) :

s.pt ⟶ pullbackinC f g

Equations

pullbackinC_lift s = Deformation.ArtinResAlg.ofHom (lift_alghom s)

Instances For

pullbackConeinC f g is a limit

source

def isLimit_pullbackConeinC {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) :

CategoryTheory.Limits.IsLimit (pullbackConeinC f g)

Equations

isLimit_pullbackConeinC f g = CategoryTheory.Limits.PullbackCone.IsLimit.mk ⋯ pullbackinC_lift ⋯ ⋯ ⋯

Instances For

source

@[simp]

theorem pullbackConeinC_lift {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} {f : X ⟶ Z} {g : Y ⟶ Z} (s : CategoryTheory.Limits.PullbackCone f g) :

(isLimit_pullbackConeinC f g).lift s = pullbackinC_lift s

source

@[simp]

theorem pullbackConeinC_fst {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} {f : X ⟶ Z} {g : Y ⟶ Z} :

(pullbackConeinC f g).fst = fstinC f g

source

@[simp]

theorem pullbackConeinC_snd {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} {f : X ⟶ Z} {g : Y ⟶ Z} :

(pullbackConeinC f g).snd = sndinC f g

source

@[simp]

theorem pullbackinC_lift_fstinC {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} {f : X ⟶ Z} {g : Y ⟶ Z} (s : CategoryTheory.Limits.PullbackCone f g) :

CategoryTheory.CategoryStruct.comp (pullbackinC_lift s) (fstinC f g) = s.fst

source

@[simp]

theorem pullbackinC_lift_fstinC_apply {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} {f : X ⟶ Z} {g : Y ⟶ Z} (s : CategoryTheory.Limits.PullbackCone f g) (x : ↑s.pt) :

(↑((pullbackinC_lift s).hom x)).1 = s.fst.hom x

source

@[simp]

theorem pullbackinC_lift_sndinC {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} {f : X ⟶ Z} {g : Y ⟶ Z} (s : CategoryTheory.Limits.PullbackCone f g) :

CategoryTheory.CategoryStruct.comp (pullbackinC_lift s) (sndinC f g) = s.snd

source

@[simp]

theorem pullbackinC_lift_sndinC_apply {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} {f : X ⟶ Z} {g : Y ⟶ Z} (s : CategoryTheory.Limits.PullbackCone f g) (x : ↑s.pt) :

(↑((pullbackinC_lift s).hom x)).2 = s.snd.hom x

source

instance instHasPullbackArtinResAlg {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) :

CategoryTheory.Limits.HasPullback f g

source

instance instHasPullbacksArtinResAlg {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] :

CategoryTheory.Limits.HasPullbacks (Deformation.ArtinResAlg Λ)

The arbitrary pullback given by pullback is isomorphic to pullbackinC

source

noncomputable def pullbackiso {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) :

CategoryTheory.Limits.pullback f g ≅ pullbackinC f g

Equations

pullbackiso f g = (CategoryTheory.Limits.pullback.isLimit f g).conePointUniqueUpToIso (isLimit_pullbackConeinC f g)

Instances For

source

@[simp]

theorem pullbackiso_hom_fst {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (pullbackiso f g).hom (fstinC f g) = CategoryTheory.Limits.pullback.fst f g

source

@[simp]

theorem pullbackiso_hom_snd {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (pullbackiso f g).hom (sndinC f g) = CategoryTheory.Limits.pullback.snd f g

source

@[simp]

theorem pullbackiso_inv_fst {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (pullbackiso f g).inv (CategoryTheory.Limits.pullback.fst f g) = fstinC f g

source

@[simp]

theorem pullbackiso_inv_snd {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (pullbackiso f g).inv (CategoryTheory.Limits.pullback.snd f g) = sndinC f g

ArtinResAlg has pullbacks #

`ArtinResAlg` has pullbacks #