@[reducible, inline]
abbrev
denom_ideal
(Λ : Type u_1)
[CommRing Λ]
[IsLocalRing Λ]
(X : Type u_2)
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
:
Ideal X
Equations
- denom_ideal Λ X = IsLocalRing.maximalIdeal X ^ 2 ⊔ Ideal.map (algebraMap Λ X) (IsLocalRing.maximalIdeal Λ)
Instances For
@[reducible, inline]
abbrev
denom
(Λ : Type u_1)
[CommRing Λ]
[IsLocalRing Λ]
(X : Type u_2)
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
:
Equations
- denom Λ X = Submodule.comap (Submodule.subtype (IsLocalRing.maximalIdeal X)) (denom_ideal Λ X)
Instances For
@[reducible, inline]
abbrev
relativeCotangentSpace
(Λ : Type u_1)
[CommRing Λ]
[IsLocalRing Λ]
(X : Type u_2)
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
:
Type u_2
Equations
- relativeCotangentSpace Λ X = (↥(IsLocalRing.maximalIdeal X) ⧸ denom Λ X)
Instances For
theorem
denom_map1'
{Λ : Type u_1}
[CommRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
{Y : Type u_3}
[CommRing Y]
[Algebra Λ Y]
[IsLocalRing Y]
(f : X →ₐ[Λ] Y)
[IsLocalHom f]
:
theorem
denom_map2
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
{Y : Type u_3}
[CommRing Y]
[Algebra Λ Y]
(f : X →ₐ[Λ] Y)
:
Ideal.map (algebraMap Λ X) (IsLocalRing.maximalIdeal Λ) ≤ Ideal.comap f (Ideal.map (algebraMap Λ Y) (IsLocalRing.maximalIdeal Λ))
theorem
denom_map
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
{Y : Type u_3}
[CommRing Y]
[Algebra Λ Y]
[IsLocalRing Y]
(f : X →ₐ[Λ] Y)
[IsLocalHom f]
:
def
relativeCotangentSpace.map_aux'
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
{Y : Type u_3}
[CommRing Y]
[Algebra Λ Y]
[IsLocalRing Y]
(f : X →ₐ[Λ] Y)
[IsLocalHom f]
:
Equations
- relativeCotangentSpace.map_aux' f = (Submodule.restrictScalars Λ (denom Λ X)).mapQ (Submodule.restrictScalars Λ (denom Λ Y)) (Deformation.maximalIdeal_map f) ⋯
Instances For
@[simp]
theorem
relativeCotangentSpace.map_aux'_apply
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
{Y : Type u_3}
[CommRing Y]
[Algebra Λ Y]
[IsLocalRing Y]
(f : X →ₐ[Λ] Y)
[IsLocalHom f]
(x : ↥(IsLocalRing.maximalIdeal X))
{h : f ↑x ∈ IsLocalRing.maximalIdeal Y}
:
@[simp]
theorem
relativeCotangentSpace.map_aux'_comp
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
{Y : Type u_3}
[CommRing Y]
[Algebra Λ Y]
[IsLocalRing Y]
(f : X →ₐ[Λ] Y)
[IsLocalHom f]
{Z : Type u_4}
[CommRing Z]
[Algebra Λ Z]
[IsLocalRing Z]
(g : Y →ₐ[Λ] Z)
[IsLocalHom g]
:
theorem
istorsion
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
:
instance
instModuleResidueFieldRelativeCotangentSpace
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
:
Equations
instance
instIsScalarTowerResidueFieldRelativeCotangentSpace
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
:
theorem
istorsion'
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
:
instance
instModuleResidueFieldRelativeCotangentSpace_1
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
:
instance
instIsScalarTowerResidueFieldRelativeCotangentSpace_1
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
:
instance
instIsScalarTowerResidueFieldRelativeCotangentSpace_2
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
[IsLocalHom (algebraMap Λ X)]
:
def
map_relCotan
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
{Y : Type u_3}
[CommRing Y]
[Algebra Λ Y]
[IsLocalRing Y]
(f : X →ₐ[Λ] Y)
[IsLocalHom f]
:
Equations
- map_relCotan f = { toFun := ⇑(relativeCotangentSpace.map_aux' f), map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
map_relCotan_apply
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
{Y : Type u_3}
[CommRing Y]
[Algebra Λ Y]
[IsLocalRing Y]
(f : X →ₐ[Λ] Y)
[IsLocalHom f]
(x : ↥(IsLocalRing.maximalIdeal X))
:
@[simp]
theorem
map_relCotan_comp
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
{Y : Type u_3}
[CommRing Y]
[Algebra Λ Y]
[IsLocalRing Y]
(f : X →ₐ[Λ] Y)
[IsLocalHom f]
{Z : Type u_4}
[CommRing Z]
[Algebra Λ Z]
[IsLocalRing Z]
(g : Y →ₐ[Λ] Z)
[IsLocalHom g]
:
def
cotan_to_relcotan
(Λ : Type u_1)
[CommRing Λ]
[IsLocalRing Λ]
(X : Type u_2)
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
:
Equations
Instances For
@[simp]
theorem
cotan_to_relcotan_apply
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
(x : ↥(IsLocalRing.maximalIdeal X))
:
theorem
cotan_to_relcotan_surjective
(Λ : Type u_1)
[CommRing Λ]
[IsLocalRing Λ]
(X : Type u_2)
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
:
theorem
commutativediag
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
{Y : Type u_3}
[CommRing Y]
[Algebra Λ Y]
[IsLocalRing Y]
(f : X →ₐ[Λ] Y)
[IsLocalHom f]
:
⇑(cotan_to_relcotan Λ Y) ∘ ⇑((IsLocalRing.maximalIdeal X).mapCotangent (IsLocalRing.maximalIdeal Y) f ⋯) = ⇑(map_relCotan f) ∘ ⇑(cotan_to_relcotan Λ X)