Module

RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList

26 declarations indexed from sourceView source ↗

Module documentation

Ring Theory Sequence Is Weakly Regular is Zero tor one quotient of List

Imports35

Mathlib.CategoryTheory.Monoidal.Tor
Mathlib.CategoryTheory.Abelian.LeftDerived
Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Mathlib.CategoryTheory.Abelian.Projective.Resolution
Mathlib.Algebra.Category.ModuleCat.Projective
Mathlib.Algebra.Category.ModuleCat.Abelian
Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Mathlib.CategoryTheory.Monoidal.Closed.Basic
Mathlib.CategoryTheory.Monoidal.Braided.Basic
Mathlib.CategoryTheory.Monoidal.Preadditive
Mathlib.Algebra.Homology.HomologySequence
Mathlib.Algebra.Homology.HomologicalComplexAbelian
Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Mathlib.Algebra.Homology.Additive
Mathlib.Algebra.Homology.ShortComplex.ShortExact
Mathlib.Algebra.Homology.ShortComplex.Exact
Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Mathlib.Algebra.Category.ModuleCat.EpiMono
Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Mathlib.CategoryTheory.Limits.Preserves.Finite
Mathlib.RingTheory.Flat.CategoryTheory
Mathlib.RingTheory.Flat.Basic
Mathlib.RingTheory.Regular.RegularSequence
Mathlib.RingTheory.Regular.IsSMulRegular
Mathlib.LinearAlgebra.TensorProduct.Quotient
Mathlib.LinearAlgebra.TensorProduct.RightExactness
Mathlib.LinearAlgebra.TensorProduct.Map
Mathlib.Algebra.Exact.Basic
Mathlib.LinearAlgebra.Isomorphisms
Mathlib.LinearAlgebra.Quotient.Basic
Mathlib.RingTheory.Ideal.Span
Mathlib.Tactic.CategoryTheory.Slice
Mathlib.Tactic.Simps.Basic

Imported by2

theorem

torLES_tensorRight_shortExact

L69 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torLES_tensorRight_shortExact

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorLES
variable {R : Type u} [CommRing R]

Lean source · statement

theorem torLES_tensorRight_shortExact {S : ShortComplex (ModuleCat.{u} R)}
    (hS : S.ShortExact) (M : ModuleCat.{u} R) [Module.Flat R M] :
    (S.map (tensorRight M)).ShortExact

def

torLES_resolutionTensorSES

L76 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torLES_resolutionTensorSES

Documentation

Tensor a short complex with each term of the chosen projective resolution.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorLES
variable {R : Type u} [CommRing R]

Lean source · statement

def torLES_resolutionTensorSES (S : ShortComplex (ModuleCat.{u} R))
    {Y : ModuleCat.{u} R} (P : ProjectiveResolution Y) :
    ShortComplex (HomologicalComplex (ModuleCat.{u} R) (ComplexShape.down ℕ))

theorem

torLES_resolutionTensorSES_shortExact

L89 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torLES_resolutionTensorSES_shortExact

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorLES
variable {R : Type u} [CommRing R]

Lean source · statement

theorem torLES_resolutionTensorSES_shortExact (S : ShortComplex (ModuleCat.{u} R))
    (hS : S.ShortExact) {Y : ModuleCat.{u} R} (P : ProjectiveResolution Y) :
    (torLES_resolutionTensorSES S P).ShortExact

def

torLES_torIso

L99 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torLES_torIso

Documentation

Identify Tor with the homology of the tensor product with the chosen resolution.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorLES
variable {R : Type u} [CommRing R]
variable {Y : ModuleCat.{u} R} (P : ProjectiveResolution Y)

Lean source · statement

def torLES_torIso (X : ModuleCat.{u} R) (n : ℕ) :
    ((Tor (ModuleCat.{u} R) n).obj X).obj Y ≅
      ((((curriedTensor (ModuleCat.{u} R)).obj X).mapHomologicalComplex
        (ComplexShape.down ℕ)).obj P.complex).homology n

theorem

torLES_torMap_app_eq

L105 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torLES_torMap_app_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorLES
variable {R : Type u} [CommRing R]
variable {Y : ModuleCat.{u} R} (P : ProjectiveResolution Y)

Lean source · statement

theorem torLES_torMap_app_eq {X X' : ModuleCat.{u} R} (f : X ⟶ X') (n : ℕ) :
    ((Tor (ModuleCat.{u} R) n).map f).app Y =
      (torLES_torIso P X n).hom ≫
        HomologicalComplex.homologyMap
          ((NatTrans.mapHomologicalComplex ((curriedTensor (ModuleCat.{u} R)).map f)
            (ComplexShape.down ℕ)).app P.complex) n ≫
        (torLES_torIso P X' n).inv

def

torLES_torDelta

L115 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torLES_torDelta

Documentation

The connecting map in the Tor long exact sequence, computed using the chosen resolution.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorLES
variable {R : Type u} [CommRing R]
variable {Y : ModuleCat.{u} R} (P : ProjectiveResolution Y)

Lean source · statement

def torLES_torDelta (S : ShortComplex (ModuleCat.{u} R))
    (hS : S.ShortExact) (n : ℕ) :
    ((Tor (ModuleCat.{u} R) (n + 1)).obj S.X₃).obj Y ⟶
      ((Tor (ModuleCat.{u} R) n).obj S.X₁).obj Y

theorem

torLES_torMap_comp_eq_zero

L123 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torLES_torMap_comp_eq_zero

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorLES
variable {R : Type u} [CommRing R]
variable {Y : ModuleCat.{u} R} (P : ProjectiveResolution Y)
include P in

Lean source · statement

theorem torLES_torMap_comp_eq_zero (S : ShortComplex (ModuleCat.{u} R)) (n : ℕ) :
    ((Tor (ModuleCat.{u} R) n).map S.f).app Y ≫
      ((Tor (ModuleCat.{u} R) n).map S.g).app Y = 0

theorem

torLES_torMap_comp_torDelta_eq_zero

L137 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torLES_torMap_comp_torDelta_eq_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorLES
variable {R : Type u} [CommRing R]
variable {Y : ModuleCat.{u} R} (P : ProjectiveResolution Y)

Lean source · statement

theorem torLES_torMap_comp_torDelta_eq_zero (S : ShortComplex (ModuleCat.{u} R))
    (hS : S.ShortExact) (n : ℕ) :
    ((Tor (ModuleCat.{u} R) (n + 1)).map S.g).app Y ≫ torLES_torDelta P S hS n = 0

theorem

torLES_torDelta_comp_eq_zero

L149 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torLES_torDelta_comp_eq_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorLES
variable {R : Type u} [CommRing R]
variable {Y : ModuleCat.{u} R} (P : ProjectiveResolution Y)

Lean source · statement

theorem torLES_torDelta_comp_eq_zero (S : ShortComplex (ModuleCat.{u} R))
    (hS : S.ShortExact) (n : ℕ) :
    torLES_torDelta P S hS n ≫ ((Tor (ModuleCat.{u} R) n).map S.f).app Y = 0

theorem

torLES_tor_exact₂

L161 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torLES_tor_exact₂

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorLES
variable {R : Type u} [CommRing R]
variable {Y : ModuleCat.{u} R} (P : ProjectiveResolution Y)

Lean source · statement

theorem torLES_tor_exact₂ (S : ShortComplex (ModuleCat.{u} R)) (hS : S.ShortExact)
    (n : ℕ) :
    (ShortComplex.mk (((Tor (ModuleCat.{u} R) n).map S.f).app Y)
      (((Tor (ModuleCat.{u} R) n).map S.g).app Y)
      (torLES_torMap_comp_eq_zero P S n)).Exact

theorem

torLES_tor_exact₃

L177 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torLES_tor_exact₃

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorLES
variable {R : Type u} [CommRing R]
variable {Y : ModuleCat.{u} R} (P : ProjectiveResolution Y)

Lean source · statement

theorem torLES_tor_exact₃ (S : ShortComplex (ModuleCat.{u} R)) (hS : S.ShortExact)
    (n : ℕ) :
    (ShortComplex.mk (((Tor (ModuleCat.{u} R) (n + 1)).map S.g).app Y)
      (torLES_torDelta P S hS n)
      (torLES_torMap_comp_torDelta_eq_zero P S hS n)).Exact

theorem

torLES_tor_exact₁

L192 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torLES_tor_exact₁

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorLES
variable {R : Type u} [CommRing R]
variable {Y : ModuleCat.{u} R} (P : ProjectiveResolution Y)

Lean source · statement

theorem torLES_tor_exact₁ (S : ShortComplex (ModuleCat.{u} R)) (hS : S.ShortExact)
    (n : ℕ) :
    (ShortComplex.mk (torLES_torDelta P S hS n)
      (((Tor (ModuleCat.{u} R) n).map S.f).app Y)
      (torLES_torDelta_comp_eq_zero P S hS n)).Exact

theorem

torLES_tor_isZero_X₂

L207 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torLES_tor_isZero_X₂

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorLES
variable {R : Type u} [CommRing R]
variable {Y : ModuleCat.{u} R} (P : ProjectiveResolution Y)
include P in

Lean source · statement

theorem torLES_tor_isZero_X₂ (S : ShortComplex (ModuleCat.{u} R)) (hS : S.ShortExact)
    (n : ℕ) (h₁ : IsZero (((Tor (ModuleCat.{u} R) (n + 1)).obj S.X₁).obj Y))
    (h₃ : IsZero (((Tor (ModuleCat.{u} R) (n + 1)).obj S.X₃).obj Y)) :
    IsZero (((Tor (ModuleCat.{u} R) (n + 1)).obj S.X₂).obj Y)

theorem

torFV_resolutionTensor_exactAt

L219 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torFV_resolutionTensor_exactAt

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorFV
variable {R : Type u} [CommRing R]

Lean source · statement

theorem torFV_resolutionTensor_exactAt (M : ModuleCat.{u} R) [Module.Flat R M]
    {Y : ModuleCat.{u} R} (P : ProjectiveResolution Y) (n : ℕ) :
    ((((curriedTensor (ModuleCat.{u} R)).obj M).mapHomologicalComplex
      (ComplexShape.down ℕ)).obj P.complex).ExactAt (n + 1)

theorem

torFV_tor_succ_isZero_of_flat_res

L226 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torFV_tor_succ_isZero_of_flat_res

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorFV
variable {R : Type u} [CommRing R]

Lean source · statement

theorem torFV_tor_succ_isZero_of_flat_res (M : ModuleCat.{u} R) [Module.Flat R M]
    {Y : ModuleCat.{u} R} (P : ProjectiveResolution Y) (n : ℕ) :
    IsZero (((Tor (ModuleCat.{u} R) (n + 1)).obj M).obj Y)

theorem

torFV_tor_succ_isZero_of_flat

L233 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torFV_tor_succ_isZero_of_flat

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorFV
variable {R : Type u} [CommRing R]

Lean source · statement

theorem torFV_tor_succ_isZero_of_flat (M : ModuleCat.{u} R) [Module.Flat R M]
    (Y : ModuleCat.{u} R) (n : ℕ) :
    IsZero (((Tor (ModuleCat.{u} R) (n + 1)).obj M).obj Y)

theorem

torFV_tor_one_isZero_of_flat

L239 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torFV_tor_one_isZero_of_flat

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorFV
variable {R : Type u} [CommRing R]

Lean source · statement

theorem torFV_tor_one_isZero_of_flat (M : ModuleCat.{u} R) [Module.Flat R M]
    (Y : ModuleCat.{u} R) :
    IsZero (((Tor (ModuleCat.{u} R) 1).obj M).obj Y)

theorem

torFV_tor_succ_isZero_of_isZero

L244 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torFV_tor_succ_isZero_of_isZero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorFV
variable {R : Type u} [CommRing R]

Lean source · statement

theorem torFV_tor_succ_isZero_of_isZero (X : ModuleCat.{u} R) (hX : IsZero X)
    (Y : ModuleCat.{u} R) (n : ℕ) :
    IsZero (((Tor (ModuleCat.{u} R) (n + 1)).obj X).obj Y)

theorem

torFV_tor_one_isZero_of_isZero

L253 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.torFV_tor_one_isZero_of_isZero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorFV
variable {R : Type u} [CommRing R]

Lean source · statement

theorem torFV_tor_one_isZero_of_isZero (X : ModuleCat.{u} R) (hX : IsZero X)
    (Y : ModuleCat.{u} R) :
    IsZero (((Tor (ModuleCat.{u} R) 1).obj X).obj Y)

theorem

ar_opcyclesMap_fromLeftDerivedZero'_naturality

L263 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.ar_opcyclesMap_fromLeftDerivedZero'_naturality

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorZeroBridge
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ar_opcyclesMap_fromLeftDerivedZero'_naturality
    {Y : ModuleCat.{u} R} (P : ProjectiveResolution Y) {X X' : ModuleCat.{u} R}
    (f : X ⟶ X') :
    HomologicalComplex.opcyclesMap
        ((NatTrans.mapHomologicalComplex ((curriedTensor (ModuleCat.{u} R)).map f)
          (ComplexShape.down ℕ)).app P.complex) 0 ≫
        P.fromLeftDerivedZero' ((curriedTensor (ModuleCat.{u} R)).obj X') =
      P.fromLeftDerivedZero' ((curriedTensor (ModuleCat.{u} R)).obj X) ≫
        ((curriedTensor (ModuleCat.{u} R)).map f).app Y

theorem

ar_tor0_map_fromLeftDerivedZero_naturality

L280 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.ar_tor0_map_fromLeftDerivedZero_naturality

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section TorZeroBridge
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ar_tor0_map_fromLeftDerivedZero_naturality
    {Y : ModuleCat.{u} R} (P : ProjectiveResolution Y) {X X' : ModuleCat.{u} R}
    (f : X ⟶ X') :
    ((Tor (ModuleCat.{u} R) 0).map f).app Y ≫
        ((curriedTensor (ModuleCat.{u} R)).obj X').fromLeftDerivedZero.app Y =
      ((curriedTensor (ModuleCat.{u} R)).obj X).fromLeftDerivedZero.app Y ≫
        ((curriedTensor (ModuleCat.{u} R)).map f).app Y

theorem

dv_tor_isZero_of_iso

L353 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.dv_tor_isZero_of_iso

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section Main
variable {R : Type u} [CommRing R]

Lean source · statement

theorem dv_tor_isZero_of_iso {X X' Y : ModuleCat.{u} R} (e : X ≅ X') (n : ℕ)
    (h : IsZero (((Tor (ModuleCat.{u} R) n).obj X').obj Y)) :
    IsZero (((Tor (ModuleCat.{u} R) n).obj X).obj Y)

theorem

tor1_isZero_of_rTensor_injective

L358 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.tor1_isZero_of_rTensor_injective

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section Main
variable {R : Type u} [CommRing R]

Lean source · statement

theorem tor1_isZero_of_rTensor_injective
    {A N M : Type u} [AddCommGroup A] [Module R A] [AddCommGroup N] [Module R N]
    [AddCommGroup M] [Module R M] (e : N →ₗ[R] A) (he : Function.Injective e)
    (hA : IsZero (((Tor (ModuleCat.{u} R) 1).obj (ModuleCat.of R A)).obj (ModuleCat.of R M)))
    (hinj : Function.Injective (LinearMap.rTensor M e)) :
    IsZero (((Tor (ModuleCat.{u} R) 1).obj (ModuleCat.of R (A ⧸ LinearMap.range e))).obj
      (ModuleCat.of R M))

theorem

step

L410 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.step

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section Main
variable {R : Type u} [CommRing R]

Lean source · statement

theorem step {M : Type u} [AddCommGroup M] [Module R M] (I : Ideal R) (x : R)
    (hI : IsZero (((Tor (ModuleCat.{u} R) 1).obj (ModuleCat.of R (R ⧸ I))).obj (ModuleCat.of R M)))
    (hx : IsSMulRegular (M ⧸ (I • ⊤ : Submodule R M)) x) :
    IsZero (((Tor (ModuleCat.{u} R) 1).obj (ModuleCat.of R (R ⧸ (I ⊔ Ideal.span {x})))).obj
      (ModuleCat.of R M))

theorem

main

L468 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList.TorRegSeq.main

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace TorRegSeq
section Main
variable {R : Type u} [CommRing R]

Lean source · statement

theorem main {M : Type u} [AddCommGroup M] [Module R M] {rs : List R}
    (hM : RingTheory.Sequence.IsWeaklyRegular M rs) :
    ∀ n, n ≤ rs.length →
      IsZero (((Tor (ModuleCat.{u} R) 1).obj (ModuleCat.of R (R ⧸ Ideal.ofList (rs.take n)))).obj
        (ModuleCat.of R M))

theorem

isZero_tor_one_quotient_ofList

L498 ↗

RingTheory.Sequence.IsWeaklyRegular.isZero_tor_one_quotient_ofList

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct

Lean source · statement

theorem _root_.RingTheory.Sequence.IsWeaklyRegular.isZero_tor_one_quotient_ofList
    {R : Type u} [CommRing R] {M : Type u} [AddCommGroup M] [Module R M]
    {rs : List R} (hM : RingTheory.Sequence.IsWeaklyRegular M rs) :
    IsZero (((Tor (ModuleCat.{u} R) 1).obj (ModuleCat.of R (R ⧸ Ideal.ofList rs))).obj
      (ModuleCat.of R M))

Module documentation

Ring Theory Sequence Is Weakly Regular is Zero tor one quotient of List

Declarations