@[reducible, inline]

noncomputable abbrev smooth_def_maps {Λ : Type u} [CommRing Λ] {F G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} (η : F ⟶ G) {A B : Deformation.ArtinResAlg Λ} (f : B ⟶ A) : F.obj B ⟶ CategoryTheory.Limits.pullback (η.app A) (G.map f)

The maps involved in the definition of smooth natural transformation.

Equations

• smooth_def_maps η f = CategoryTheory.Limits.pullback.lift (F.map f) (η.app B) ⋯

theorem smooth_def_maps_fst {Λ : Type u} [CommRing Λ] (F G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (η : F ⟶ G) {A B : Deformation.ArtinResAlg Λ} (f : B ⟶ A) : CategoryTheory.CategoryStruct.comp (smooth_def_maps η f) (CategoryTheory.Limits.pullback.fst (η.app A) (G.map f)) = F.map f

theorem smooth_def_maps_snd {Λ : Type u} [CommRing Λ] (F G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (η : F ⟶ G) {A B : Deformation.ArtinResAlg Λ} (f : B ⟶ A) : CategoryTheory.CategoryStruct.comp (smooth_def_maps η f) (CategoryTheory.Limits.pullback.snd (η.app A) (G.map f)) = η.app B

instance instIsIsoObjArtinResAlgPullbackAppMapSmooth_def_mapsOfFunctorType {Λ : Type u} [CommRing Λ] (F G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (η : F ⟶ G) [CategoryTheory.IsIso η] {A B : Deformation.ArtinResAlg Λ} (f : B ⟶ A) : CategoryTheory.IsIso (smooth_def_maps η f)

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

a natural transformation F ⟹ G is smooth if for any surjective B ⟶ A in ArtinResidueAlg the induced morphism F B ⟶ F A ⨯_G(A) G B is surjective

Equations

• IsSmooth η = ∀ {B A : Deformation.ArtinResAlg Λ} (f : B ⟶ A), Function.Surjective ⇑f.hom → Function.Surjective (smooth_def_maps η f)

def pullbackObj_lift {X Y Z : Type w} {f : X ⟶ Z} {g : Y ⟶ Z} {W : Type w} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) : W ⟶ CategoryTheory.Limits.Types.PullbackObj f g

Equations

• pullbackObj_lift h k w = CategoryTheory.Limits.PullbackCone.IsLimit.lift (CategoryTheory.Limits.Types.pullbackLimitCone f g).isLimit h k w

theorem eq_lift_pullbackObj {Λ : Type u} [CommRing Λ] (F G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (η : F ⟶ G) {A B : Deformation.ArtinResAlg Λ} (f : B ⟶ A) : smooth_def_maps η f = CategoryTheory.CategoryStruct.comp (pullbackObj_lift (F.map f) (η.app B) ⋯) (CategoryTheory.Limits.Types.pullbackIsoPullback (η.app A) (G.map f)).inv

theorem smooth_def_map_surj_iff_aux {Λ : Type u} [CommRing Λ] (F G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (η : F ⟶ G) {A B : Deformation.ArtinResAlg Λ} (f : B ⟶ A) : Function.Surjective (smooth_def_maps η f) ↔ Function.Surjective (pullbackObj_lift (F.map f) (η.app B) ⋯)

theorem smooth_def_map_surj_iff {Λ : Type u} [CommRing Λ] (F G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (η : F ⟶ G) {A B : Deformation.ArtinResAlg Λ} (f : B ⟶ A) : Function.Surjective (smooth_def_maps η f) ↔ ∀ (x : F.obj A) (y : G.obj B), η.app A x = G.map f y → ∃ (z : F.obj B), F.map f z = x ∧ η.app B z = y

theorem isSmooth_iff {Λ : Type u} [CommRing Λ] {F G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} (η : F ⟶ G) [IsLocalRing Λ] : IsSmooth η ↔ ∀ {B A : Deformation.ArtinResAlg Λ} (f : B ⟶ A), Function.Surjective ⇑f.hom → IsSmallExtension f → Function.Surjective (smooth_def_maps η f)

it is enough to check the condition on small extensions

theorem terminal_from_eq_residue {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A : Deformation.ArtinResAlg Λ} : CategoryTheory.Limits.terminal.from A = CategoryTheory.CategoryStruct.comp (residuehom_artin Λ A) (CategoryTheory.Limits.terminalIsoIsTerminal (isTerminal_residueField_artin' Λ A)).inv

theorem surjective_terminal_from {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A : Deformation.ArtinResAlg Λ} : Function.Surjective ⇑(CategoryTheory.Limits.terminal.from A).hom

theorem surj_of_smooth {Λ : Type u} [CommRing Λ] {F G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {η : F ⟶ G} [IsLocalRing Λ] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) G] (h : IsSmooth η) (A : Deformation.ArtinResAlg Λ) : Function.Surjective (η.app A)