Documentation

Atlas.ArithmeticGeometry.code.CotangentLocal

source
theorem CotangentDual.algebraMap_comp_section {R : Type u_1} [CommRing R] {k : Type u_2} [Field k] [Algebra k R] [Algebra R k] [IsScalarTower k R k] (c : k) :
(algebraMap R k) ((algebraMap k R) c) = c
source
theorem CotangentDual.mem_maximalIdeal_map_zero {R : Type u_1} [CommRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra R k] (hφ : Function.Surjective ⇑(algebraMap R k)) (x : ↥(IsLocalRing.maximalIdeal R)) :
(algebraMap R k) ↑x = 0
source
noncomputable def CotangentDual.projMaxIdeal {R : Type u_1} [CommRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] [Algebra R k] [IsScalarTower k R k] (hφ : Function.Surjective ⇑(algebraMap R k)) (r : R) :
↥(IsLocalRing.maximalIdeal R)
Instances For
    source
    theorem CotangentDual.projMaxIdeal_add {R : Type u_1} [CommRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] [Algebra R k] [IsScalarTower k R k] (hφ : Function.Surjective ⇑(algebraMap R k)) (x y : R) :
    projMaxIdeal hφ (x + y) = projMaxIdeal hφ x + projMaxIdeal hφ y
    source
    theorem CotangentDual.projMaxIdeal_smul {R : Type u_1} [CommRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] [Algebra R k] [IsScalarTower k R k] (hφ : Function.Surjective ⇑(algebraMap R k)) (c : k) (x : R) :
    projMaxIdeal hφ (c • x) = c • projMaxIdeal hφ x
    source
    theorem CotangentDual.projMaxIdeal_one {R : Type u_1} [CommRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] [Algebra R k] [IsScalarTower k R k] (hφ : Function.Surjective ⇑(algebraMap R k)) :
    projMaxIdeal hφ 1 = 0
    source
    theorem CotangentDual.projMaxIdeal_of_mem {R : Type u_1} [CommRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] [Algebra R k] [IsScalarTower k R k] (hφ : Function.Surjective ⇑(algebraMap R k)) (m : ↥(IsLocalRing.maximalIdeal R)) :
    (IsLocalRing.maximalIdeal R).toCotangent (projMaxIdeal hφ ↑m) = (IsLocalRing.maximalIdeal R).toCotangent m
    source
    theorem CotangentDual.projCotangent_leibniz {R : Type u_1} [CommRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] [Algebra R k] [IsScalarTower k R k] (hφ : Function.Surjective ⇑(algebraMap R k)) (x y : R) :
    (IsLocalRing.maximalIdeal R).toCotangent (projMaxIdeal hφ (x * y)) = (algebraMap k R) ((algebraMap R k) x) • (IsLocalRing.maximalIdeal R).toCotangent (projMaxIdeal hφ y) + (algebraMap k R) ((algebraMap R k) y) • (IsLocalRing.maximalIdeal R).toCotangent (projMaxIdeal hφ x)
    source
    noncomputable def CotangentDual.derivRestrict {R : Type u_1} [CommRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] [Algebra R k] (D : Derivation k R k) :
    ↥(IsLocalRing.maximalIdeal R) →ₗ[k] k
    Instances For
      source
      theorem CotangentDual.derivRestrict_vanishes {R : Type u_1} [CommRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] [Algebra R k] (hφ : Function.Surjective ⇑(algebraMap R k)) (D : Derivation k R k) (x y : ↥(IsLocalRing.maximalIdeal R)) :
      (derivRestrict D) (x * y) = 0
      source
      noncomputable def CotangentDual.derivToDual {R : Type u_1} [CommRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] [Algebra R k] (hφ : Function.Surjective ⇑(algebraMap R k)) (D : Derivation k R k) :
      Module.Dual k (IsLocalRing.CotangentSpace R)
      Instances For
        source
        noncomputable def CotangentDual.dualToDeriv {R : Type u_1} [CommRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] [Algebra R k] [IsScalarTower k R k] (hφ : Function.Surjective ⇑(algebraMap R k)) (ψ : Module.Dual k (IsLocalRing.CotangentSpace R)) :
        Derivation k R k
        Instances For
          source
          noncomputable def CotangentDual.derivToDualLinear {R : Type u_1} [CommRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] [Algebra R k] [IsScalarTower k R k] (hφ : Function.Surjective ⇑(algebraMap R k)) :
          Derivation k R k →ₗ[k] Module.Dual k (IsLocalRing.CotangentSpace R)
          Instances For
            source
            noncomputable def CotangentDual.dualToDerivLinear {R : Type u_1} [CommRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] [Algebra R k] [IsScalarTower k R k] (hφ : Function.Surjective ⇑(algebraMap R k)) :
            Module.Dual k (IsLocalRing.CotangentSpace R) →ₗ[k] Derivation k R k
            Instances For
              source
              noncomputable def CotangentDual.cotangentDualEquivDerivation {R : Type u_1} [CommRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] [Algebra R k] [IsScalarTower k R k] (hφ : Function.Surjective ⇑(algebraMap R k)) :
              Module.Dual k (IsLocalRing.CotangentSpace R) ≃ₗ[k] Derivation k R k
              Instances For
                source
                theorem CotangentDual.cotangent_dual_tangent {R : Type u_1} [CommRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] [Algebra R k] [IsScalarTower k R k] (hφ : Function.Surjective ⇑(algebraMap R k)) :
                Nonempty (Module.Dual k (IsLocalRing.CotangentSpace R) ≃ₗ[k] Derivation k R k)