instance
instSMulCommClassResidueField_schlessinger
(Λ : Type u_1)
[CommRing Λ]
[IsLocalRing Λ]
(X : Type u_2)
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
[IsResidueAlgebra Λ X]
:
noncomputable def
decomp_2
(Λ : Type u_1)
[CommRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
[IsResidueAlgebra Λ X]
(x : X)
:
Instances For
theorem
decomp_sum
(Λ : Type u_1)
[CommRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
[IsResidueAlgebra Λ X]
(x : X)
:
@[simp]
theorem
residue_decomp_1
(Λ : Type u_1)
[CommRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
[IsResidueAlgebra Λ X]
(x : X)
:
theorem
mk_decomps_eq
(Λ : Type u_1)
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
[IsResidueAlgebra Λ X]
(a1 a2 : Λ)
(b1 b2 : ↥(IsLocalRing.maximalIdeal X))
(h : (algebraMap Λ X) a1 + ↑b1 = (algebraMap Λ X) a2 + ↑b2)
:
theorem
fun_of_decomp
(Λ : Type u_1)
[CommRing Λ]
[IsLocalRing Λ]
{X : Type u_2}
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
[IsResidueAlgebra Λ X]
(f : Module.Dual (IsLocalRing.ResidueField X) (relativeCotangentSpace Λ X))
(x : X)
(a : Λ)
(b : ↥(IsLocalRing.maximalIdeal X))
(h : (algebraMap Λ X) a + ↑b = x)
:
noncomputable def
dual_relcotan_equiv_deriv_fun_fun
(Λ : Type u_1)
[CommRing Λ]
[IsLocalRing Λ]
(X : Type u_2)
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
[IsResidueAlgebra Λ X]
(f : Module.Dual (IsLocalRing.ResidueField X) (relativeCotangentSpace Λ X))
:
Derivation Λ X (IsLocalRing.ResidueField X)
Equations
- dual_relcotan_equiv_deriv_fun_fun Λ X f = { toFun := fun (x : X) => f (Submodule.Quotient.mk (decomp_2 Λ x)), map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }
Instances For
@[simp]
theorem
dual_relcotan_equiv_deriv_fun_fun_apply
(Λ : Type u_1)
[CommRing Λ]
[IsLocalRing Λ]
(X : Type u_2)
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
[IsResidueAlgebra Λ X]
(f : Module.Dual (IsLocalRing.ResidueField X) (relativeCotangentSpace Λ X))
(x : X)
:
noncomputable def
dual_relcotan_equiv_deriv_fun
(Λ : Type u_1)
[CommRing Λ]
[IsLocalRing Λ]
(X : Type u_2)
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
[IsResidueAlgebra Λ X]
:
Equations
- dual_relcotan_equiv_deriv_fun Λ X = { toFun := dual_relcotan_equiv_deriv_fun_fun Λ X, map_add' := ⋯, map_smul' := ⋯ }
Instances For
theorem
deriv_max_sq_zero
(Λ : Type u_1)
[CommRing Λ]
(X : Type u_2)
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
(f : Derivation Λ X (IsLocalRing.ResidueField X))
(x : ↥(IsLocalRing.maximalIdeal X ^ 2))
:
theorem
deriv_map_zero
(Λ : Type u_1)
[CommRing Λ]
[IsLocalRing Λ]
(X : Type u_2)
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
[IsResidueAlgebra Λ X]
(f : Derivation Λ X (IsLocalRing.ResidueField X))
(x : ↥(Ideal.map (algebraMap Λ X) (IsLocalRing.maximalIdeal Λ)))
:
theorem
denom_in_ker
(Λ : Type u_1)
[CommRing Λ]
[IsLocalRing Λ]
(X : Type u_2)
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
[IsResidueAlgebra Λ X]
(f : Derivation Λ X (IsLocalRing.ResidueField X))
:
noncomputable def
dual_relcotan_equiv_deriv_inv
(Λ : Type u_1)
[CommRing Λ]
[IsLocalRing Λ]
(X : Type u_2)
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
[IsResidueAlgebra Λ X]
(f : Derivation Λ X (IsLocalRing.ResidueField X))
:
Equations
- dual_relcotan_equiv_deriv_inv Λ X f = { toFun := fun (x : relativeCotangentSpace Λ X) => f ↑(Quotient.out x), map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
dual_relcotan_equiv_deriv_inv_apply
(Λ : Type u_1)
[CommRing Λ]
[IsLocalRing Λ]
(X : Type u_2)
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
[IsResidueAlgebra Λ X]
(f : Derivation Λ X (IsLocalRing.ResidueField X))
(x : relativeCotangentSpace Λ X)
:
noncomputable def
dual_relcotan_equiv_deriv
(Λ : Type u_1)
[CommRing Λ]
[IsLocalRing Λ]
(X : Type u_2)
[CommRing X]
[Algebra Λ X]
[IsLocalRing X]
[IsResidueAlgebra Λ X]
:
Equations
- dual_relcotan_equiv_deriv Λ X = { toFun := dual_relcotan_equiv_deriv_fun_fun Λ X, map_add' := ⋯, map_smul' := ⋯, invFun := dual_relcotan_equiv_deriv_inv Λ X, left_inv := ⋯, right_inv := ⋯ }