Module

Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.lean

Nyll.AlgebraicCurves.Geometry.Deformation.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace

31 declarations indexed from sourceView source ↗

Module documentation

Tangent points and the cotangent space

Square-zero lifts identify tangent points with linear maps from the cotangent space.

Imports4

Imported by2

abbrev

pt0

L41 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.pt0

Documentation

The underlying scheme point of a field-valued point.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}

Lean source · statement

abbrev pt0 (pt : Spec (CommRingCat.of K) ⟶ X) : X

abbrev

π

L49 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.π

Documentation

The homomorphism from the local stalk to the residue field supplied by the point.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))

Lean source · statement

abbrev π (pt : Spec (CommRingCat.of K) ⟶ X) : X.presheaf.stalk (pt0 pt) →+* K

theorem

π_algebraMap

L55 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.π_algebraMap

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section
include halg

Lean source · statement

theorem π_algebraMap (hpt : pt ≫ x = 𝟙 _) (a : K) : π pt (algebraMap K _ a) = a

def

πₐ

L73 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.πₐ

Documentation

The stalk-to-field homomorphism viewed as an algebra homomorphism.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))

Lean source · statement

def πₐ (hπ : ∀ a : K, π pt (algebraMap K _ a) = a) : X.presheaf.stalk (pt0 pt) →ₐ[K] K

theorem

πₐ_apply

L76 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.πₐ_apply

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))

Lean source · statement

theorem πₐ_apply (hπ : ∀ a : K, π pt (algebraMap K _ a) = a) (r : X.presheaf.stalk
  (pt0 pt)) :
    πₐ hπ r = π pt r

theorem

ker_πₐ

L80 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.ker_πₐ

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))

Lean source · statement

theorem ker_πₐ (hπ : ∀ a : K, π pt (algebraMap K _ a) = a) :
    RingHom.ker (πₐ hπ) = maximalIdeal (X.presheaf.stalk (pt0 pt))

abbrev

Λ₀

L92 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.Λ₀

Documentation

The scheme morphism induced by a homomorphism from the local stalk.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Local
variable {A : Type u} [CommRing A] [IsLocalRing A]

Lean source · statement

abbrev Λ₀ (pt : Spec (CommRingCat.of K) ⟶ X) (f : X.presheaf.stalk (pt0 pt) ⟶ CommRingCat.of A) :
    Spec (CommRingCat.of A) ⟶ X

theorem

Λ₀_injective

L97 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.Λ₀_injective

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Local
variable {A : Type u} [CommRing A] [IsLocalRing A]
omit inst in

Lean source · statement

theorem Λ₀_injective {f f' : X.presheaf.stalk (pt0 pt) ⟶ CommRingCat.of A} [IsLocalHom f.hom]
    [IsLocalHom f'.hom] (h : Λ₀ pt f = Λ₀ pt f') : f = f'

theorem

appTop_Λ₀_comp

L106 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.appTop_Λ₀_comp

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Local
variable {A : Type u} [CommRing A] [IsLocalRing A]
omit inst [IsLocalRing A] in

Lean source · statement

theorem appTop_Λ₀_comp (f : X.presheaf.stalk (pt0 pt) ⟶ CommRingCat.of A) :
    (Λ₀ pt f ≫ x).appTop ≫ (Scheme.ΓSpecIso (CommRingCat.of A)).hom =
      x.appTop ≫ X.presheaf.germ ⊤ (pt0 pt) trivial ≫ f

theorem

Λ₀_comp_eq_Spec_map

L118 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.Λ₀_comp_eq_Spec_map

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Local
variable {A : Type u} [CommRing A] [IsLocalRing A]
omit [IsLocalRing A] in
include halg in

Lean source · statement

theorem Λ₀_comp_eq_Spec_map (f : X.presheaf.stalk (pt0 pt) ⟶ CommRingCat.of A) (g : K →+* A)
    (hfg : ∀ a : K, f.hom (algebraMap K _ a) = g a) :
    Λ₀ pt f ≫ x = Spec.map (CommRingCat.ofHom g)

theorem

apply_algebraMap_of_Λ₀_comp_eq

L134 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.apply_algebraMap_of_Λ₀_comp_eq

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Local
variable {A : Type u} [CommRing A] [IsLocalRing A]
omit [IsLocalRing A] in
include halg in

Lean source · statement

theorem apply_algebraMap_of_Λ₀_comp_eq (f : X.presheaf.stalk (pt0 pt) ⟶ CommRingCat.of A) (g : K
  →+* A)
    (h : Λ₀ pt f ≫ x = Spec.map (CommRingCat.ofHom g)) (a : K) :
    f.hom (algebraMap K _ a) = g a

def

liftHom

L153 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.liftHom

Documentation

The square-zero algebra homomorphism determined by a cotangent-space linear map.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

def liftHom (f : (RingHom.ker (πₐ hπ)).Cotangent →ₗ[K] V) :
    X.presheaf.stalk (pt0 pt) →ₐ[K] TrivSqZeroExt K V

theorem

fst_liftHom

L157 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.fst_liftHom

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

theorem fst_liftHom (f : (RingHom.ker (πₐ hπ)).Cotangent →ₗ[K] V) (r : X.presheaf.stalk (pt0 pt)) :
    (liftHom hπ f r).fst = π pt r

theorem

snd_liftHom

L161 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.snd_liftHom

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

theorem snd_liftHom (f : (RingHom.ker (πₐ hπ)).Cotangent →ₗ[K] V) (a : RingHom.ker (πₐ hπ)) :
    (liftHom hπ f (a : X.presheaf.stalk (pt0 pt))).snd = f ((RingHom.ker (πₐ hπ)).toCotangent a)

theorem

liftHom_unique

L165 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.liftHom_unique

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

theorem liftHom_unique (f : (RingHom.ker (πₐ hπ)).Cotangent →ₗ[K] V)
    (ψ : X.presheaf.stalk (pt0 pt) →ₐ[K] TrivSqZeroExt K V) (h1 : ∀ r, (ψ r).fst = π pt r)
    (h2 : ∀ a : RingHom.ker (πₐ hπ), (ψ (a : X.presheaf.stalk (pt0 pt))).snd =
      f ((RingHom.ker (πₐ hπ)).toCotangent a)) :
    ψ = liftHom hπ f

theorem

exists_eq_liftHom

L173 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.exists_eq_liftHom

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

theorem exists_eq_liftHom (ψ : X.presheaf.stalk (pt0 pt) →ₐ[K] TrivSqZeroExt K V)
    (h1 : ∀ r, (ψ r).fst = π pt r) : ∃ f, ψ = liftHom hπ f

theorem

liftHom_injective

L178 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.liftHom_injective

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

theorem liftHom_injective : Function.Injective (liftHom hπ (V := V))

theorem

map_comp_liftHom

L185 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.map_comp_liftHom

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

theorem map_comp_liftHom (φ : V →ₗ[K] W) (f : (RingHom.ker (πₐ hπ)).Cotangent →ₗ[K] V) :
    (TrivSqZeroExt.map φ).comp (liftHom hπ f) = liftHom hπ (φ ∘ₗ f)

theorem

isLocalHom_of_fst_eq

L192 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.isLocalHom_of_fst_eq

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
omit inst in

Lean source · statement

theorem isLocalHom_of_fst_eq (ψ : X.presheaf.stalk (pt0 pt) →+* TrivSqZeroExt K V)
    (h1 : ∀ r, (ψ r).fst = π pt r) : IsLocalHom ψ

instance

isLocalHom_liftHom

L199 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.isLocalHom_liftHom

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

instance isLocalHom_liftHom (f : (RingHom.ker (πₐ hπ)).Cotangent →ₗ[K] V) :
    IsLocalHom (CommRingCat.ofHom (liftHom hπ f).toRingHom).hom

theorem

isLocalHom_fstHom

L204 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.isLocalHom_fstHom

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
omit inst in

Lean source · statement

theorem isLocalHom_fstHom : IsLocalHom (TrivSqZeroExt.fstHom K K V).toRingHom

instance

isLocalHom_fstHom'

L207 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.isLocalHom_fstHom'

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

instance isLocalHom_fstHom' : IsLocalHom (CommRingCat.ofHom (TrivSqZeroExt.fstHom K K
  V).toRingHom).hom

def

pointOf

L214 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.pointOf

Documentation

The tangent point induced by a cotangent-space linear map.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
include halg

Lean source · statement

def pointOf (f : (RingHom.ker (πₐ hπ)).Cotangent →ₗ[K] V) : TangentPoints x pt V

theorem

pointOf_coe

L221 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.pointOf_coe

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
include halg

Lean source · statement

theorem pointOf_coe (f : (RingHom.ker (πₐ hπ)).Cotangent →ₗ[K] V) :
    (pointOf halg hπ f).1 = Λ₀ pt (CommRingCat.ofHom (liftHom hπ f).toRingHom)

theorem

pointOf_injective

L224 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.pointOf_injective

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
include halg

Lean source · statement

theorem pointOf_injective : Function.Injective (pointOf halg hπ (V := V))

theorem

pointOf_map

L235 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.pointOf_map

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
include halg

Lean source · statement

theorem pointOf_map (φ : V →ₗ[K] W) (f : (RingHom.ker (πₐ hπ)).Cotangent →ₗ[K] V) :
    pointOf halg hπ (φ ∘ₗ f) = (pointOf halg hπ f).map φ

theorem

pointOf_surjective

L242 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.pointOf_surjective

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
include halg

Lean source · statement

theorem pointOf_surjective : Function.Surjective (pointOf halg hπ (V := V))

def

pointEquiv

L285 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.pointEquiv

Documentation

The equivalence between cotangent-space linear maps and tangent points.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
include halg

Lean source · statement

def pointEquiv : ((RingHom.ker (πₐ hπ)).Cotangent →ₗ[K] V) ≃ TangentPoints x pt V

theorem

pointEquiv_apply

L288 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.pointEquiv_apply

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1
noncomputable section
variable {K : Type u} [Field K] {X : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of K)}
  {pt : Spec (CommRingCat.of K) ⟶ X}
variable [inst : Algebra K (X.presheaf.stalk (pt0 pt))]
  (halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
    (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
      K)).inv.hom a)))
section Tangent
variable (hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
include halg

Lean source · statement

theorem pointEquiv_apply (f : (RingHom.ker (πₐ hπ)).Cotangent →ₗ[K] V) :
    pointEquiv halg hπ f = pointOf halg hπ f

def

cotangentCast

L296 ↗

AlgebraicCurves.Geometry.Deformation.Proofs.Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace.P2mTJ1.cotangentCast

Documentation

Transports a cotangent space along the equality of the defining ideals.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
namespace P2mTJ1

Lean source · statement

def cotangentCast {K : Type u} [Field K] {S : Type u} [CommRing S] [Algebra K S] {I J
  : Ideal S}
    (h : I = J) : I.Cotangent ≃ₗ[K] J.Cotangent

theorem

exists_tangentPoints_equiv_linearMap_cotangentSpace

L305 ↗

AlgebraicGeometry.Scheme.exists_tangentPoints_equiv_linearMap_cotangentSpace

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace Scheme_exists_tangentPoints_equiv_linearMap_cotangentSpace
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TrivSqZeroExt
open P2mTJ1 IsLocalRing in

Lean source · full declaration

theorem _root_.AlgebraicGeometry.Scheme.exists_tangentPoints_equiv_linearMap_cotangentSpace
    {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K))
    (pt : Spec (CommRingCat.of K) ⟶ X) (hpt : pt ≫ x = 𝟙 (Spec (CommRingCat.of K))) :
    letI : Algebra K (X.presheaf.stalk (pt.base (IsLocalRing.closedPoint K))) :=
      ((X.presheaf.germ ⊤ (pt.base (IsLocalRing.closedPoint K)) trivial).hom.comp
        (x.appTop.hom.comp (Scheme.ΓSpecIso (CommRingCat.of K)).inv.hom)).toAlgebra
    ∃ γ : ∀ (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V],
        TangentPoints x pt V ≃
          (IsLocalRing.CotangentSpace (X.presheaf.stalk (pt.base (IsLocalRing.closedPoint K)))
            →ₗ[K] V),
      ∀ (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
        (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
        (φ : V →ₗ[K] W) (v : TangentPoints x pt V),
        γ W (v.map φ) = φ ∘ₗ γ V v := by
  let alg : Algebra K (X.presheaf.stalk (pt0 pt)) :=
    ((X.presheaf.germ ⊤ (pt0 pt) trivial).hom.comp
      (x.appTop.hom.comp (Scheme.ΓSpecIso (CommRingCat.of K)).inv.hom)).toAlgebra
  have halg : ∀ a : K, algebraMap K (X.presheaf.stalk (pt0 pt)) a =
      (X.presheaf.germ ⊤ (pt0 pt) trivial).hom (x.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
        K)).inv.hom a)) :=
    fun a => rfl
  have hπ : ∀ a : K, π pt (algebraMap K (X.presheaf.stalk (pt0 pt)) a) = a := π_algebraMap halg hpt
  let c : IsLocalRing.CotangentSpace (X.presheaf.stalk (pt0 pt)) ≃ₗ[K] (RingHom.ker (πₐ
    hπ)).Cotangent :=
    cotangentCast (ker_πₐ hπ).symm
  refine ⟨fun V _ _ _ _ =>
    { toFun := fun v => ((pointEquiv halg hπ).symm v) ∘ₗ c.toLinearMap
      invFun := fun g => pointEquiv halg hπ (g ∘ₗ c.symm.toLinearMap)
      left_inv := fun v => by
        change pointEquiv halg hπ ((((pointEquiv halg hπ).symm v) ∘ₗ c.toLinearMap) ∘ₗ
          c.symm.toLinearMap) = v
        have : (((pointEquiv halg hπ).symm v) ∘ₗ c.toLinearMap) ∘ₗ c.symm.toLinearMap =
            (pointEquiv halg hπ).symm v := by
          ext y; simp
        rw [this, Equiv.apply_symm_apply]
      right_inv := fun g => by
        change ((pointEquiv halg hπ).symm (pointEquiv halg hπ (g ∘ₗ c.symm.toLinearMap))) ∘ₗ
          c.toLinearMap = g
        rw [Equiv.symm_apply_apply]
        ext y; simp }, ?_⟩
  intro V _ _ _ _ W _ _ _ _ φ v
  obtain ⟨f, rfl⟩ := (pointEquiv halg hπ (V := V)).surjective v
  have hmap : (pointEquiv halg hπ f).map φ = pointEquiv halg hπ (φ ∘ₗ f) := (pointOf_map halg hπ φ
    f).symm
  rw [hmap]
  change ((pointEquiv halg hπ).symm (pointEquiv halg hπ (φ ∘ₗ f))) ∘ₗ c.toLinearMap =
    φ ∘ₗ (((pointEquiv halg hπ).symm (pointEquiv halg hπ f)) ∘ₗ c.toLinearMap)
  rw [Equiv.symm_apply_apply, Equiv.symm_apply_apply, LinearMap.comp_assoc]

Module documentation

Tangent points and the cotangent space

Declarations