NYLL
Module

IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
39 declarations indexed from sourceView source ↗

Module documentation

Is Local Ring flat of is Scalar Tower of flat of flat quotient maximal Ideal map univ

Imports2
Imported by2

Declarations

abbrev

Igw157LcTor1ResidueVanishing

L34 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.Igw157LcTor1ResidueVanishing
Documentation

Vanishing of the first Tor of a module with the residue field of the local ring.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
abbrev Igw157LcTor1ResidueVanishing (R : Type u) [CommRing R] [IsLocalRing R]
    (M : Type u) [AddCommGroup M] [Module R M] : Prop
theorem

torLES_tensorRight_shortExact

L42 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
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

L49 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
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

L62 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
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

L72 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
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

L78 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
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

L88 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
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

L96 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
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

L110 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
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

L122 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
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₂

L134 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
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₃

L150 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
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₁

L165 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
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

torFV_resolutionTensor_exactAt

L185 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
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

L192 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
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

L199 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
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

L205 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
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

tor0_opcyclesMap_fromLeftDerivedZero'_naturality

L215 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.tor0_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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section Tor0Nat
variable {R : Type u} [CommRing R]
Lean source · statement
theorem tor0_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

tor0_tor0_map_fromLeftDerivedZero_naturality

L232 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.tor0_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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section Tor0Nat
variable {R : Type u} [CommRing R]
Lean source · statement
theorem tor0_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

kwFF9_tor0_map_mono_of_rTensor_injective

L305 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.kwFF9_tor0_map_mono_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 IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section FF9Engine
variable {R : Type u} [CommRing R]
Lean source · statement
theorem kwFF9_tor0_map_mono_of_rTensor_injective {X X' : ModuleCat.{u} R}
    (f : X ⟶ X') (Y : ModuleCat.{u} R)
    (hinj : Function.Injective (LinearMap.rTensor Y f.hom)) :
    Mono (((Tor (ModuleCat.{u} R) 0).map f).app Y)
theorem

kwFF9_tor1_isZero_of_flat_of_rTensor_inj

L330 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.kwFF9_tor1_isZero_of_flat_of_rTensor_inj
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section FF9Engine
variable {R : Type u} [CommRing R]
Lean source · statement
theorem kwFF9_tor1_isZero_of_flat_of_rTensor_inj
    (S : ShortComplex (ModuleCat.{u} R)) (hS : S.ShortExact) [Module.Flat R S.X₂]
    (Y : ModuleCat.{u} R)
    (hinj : Function.Injective (LinearMap.rTensor Y S.f.hom)) :
    IsZero (((Tor (ModuleCat.{u} R) 1).obj S.X₃).obj Y)
theorem

kwFF9_idealSES_shortExact

L345 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.kwFF9_idealSES_shortExact
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section FF9Engine
variable {R : Type u} [CommRing R]
Lean source · full declaration
theorem kwFF9_idealSES_shortExact {S : Type u} [CommRing S] (I : Ideal S) :
    (ShortComplex.mk (ModuleCat.ofHom I.subtype) (ModuleCat.ofHom (Submodule.mkQ I))
      (by rw [← ModuleCat.ofHom_comp]; exact congrArg _ (LinearMap.ext fun a =>
        (Submodule.Quotient.mk_eq_zero _).mpr a.2))).ShortExact := by
  refine ModuleCat.shortComplex_shortExact _ ?_ ?_ ?_
  · exact (LinearMap.exact_subtype_mkQ I)
  · exact Submodule.injective_subtype I
  · exact Submodule.mkQ_surjective I
theorem

kwFF12_tor1_isZero_of_tor1_of_rTensor_inj

L354 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.kwFF12_tor1_isZero_of_tor1_of_rTensor_inj
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section FF9Engine
variable {R : Type u} [CommRing R]
Lean source · statement
theorem kwFF12_tor1_isZero_of_tor1_of_rTensor_inj
    (S : ShortComplex (ModuleCat.{u} R)) (hS : S.ShortExact) (Y : ModuleCat.{u} R)
    (h2 : IsZero (((Tor (ModuleCat.{u} R) 1).obj S.X₂).obj Y))
    (hinj : Function.Injective (LinearMap.rTensor Y S.f.hom)) :
    IsZero (((Tor (ModuleCat.{u} R) 1).obj S.X₃).obj Y)
abbrev

KwFF3Tor1IdealVanishing

L370 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.KwFF3Tor1IdealVanishing
Documentation

Vanishing of the first Tor of a module with the quotient by a given ideal.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
abbrev KwFF3Tor1IdealVanishing (R : Type u) [CommRing R] (I : Ideal R)
    (M : Type u) [AddCommGroup M] [Module R M] : Prop
abbrev

KwFibralFlatTor1Vanish

L376 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.KwFibralFlatTor1Vanish
Documentation

The Tor vanishing condition for the image of the base maximal ideal in a local tower.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
abbrev KwFibralFlatTor1Vanish : Prop
abbrev

KwFF9IdealRTensorInj

L385 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.KwFF9IdealRTensorInj
Documentation

Injectivity of tensoring the inclusion of the base maximal ideal image in a flat local tower.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
abbrev KwFF9IdealRTensorInj : Prop
theorem

kwFF9_torVanish_of_idealRTensorInj

L394 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.kwFF9_torVanish_of_idealRTensorInj
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
theorem kwFF9_torVanish_of_idealRTensorInj (hInj : KwFF9IdealRTensorInj.{u}) :
    KwFibralFlatTor1Vanish.{u}
abbrev

KwFF10IdealTowerTensorFactor

L403 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.KwFF10IdealTowerTensorFactor
Documentation

A surjective tensor comparison for the base maximal ideal compatible with its inclusions.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
abbrev KwFF10IdealTowerTensorFactor : Prop
theorem

kwFF10_idealRTensorInj_of_towerFactor

L414 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.kwFF10_idealRTensorInj_of_towerFactor
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
theorem kwFF10_idealRTensorInj_of_towerFactor (hFactor : KwFF10IdealTowerTensorFactor.{u}) :
    KwFF9IdealRTensorInj.{u}
theorem

kwFF11_idealTowerTensorFactor_proved

L426 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.kwFF11_idealTowerTensorFactor_proved
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
theorem kwFF11_idealTowerTensorFactor_proved : KwFF10IdealTowerTensorFactor.{u}
theorem

kwFF12_residueQuotSES_shortExact

L477 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.kwFF12_residueQuotSES_shortExact
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · full declaration
theorem kwFF12_residueQuotSES_shortExact {S : Type u} [CommRing S] [IsLocalRing S]
    (I : Ideal S) (hI_le : I ≤ IsLocalRing.maximalIdeal S) :
    (ShortComplex.mk
      (ModuleCat.ofHom
        (Submodule.map (Submodule.mkQ I) (IsLocalRing.maximalIdeal S)).subtype)
      (ModuleCat.ofHom (Submodule.liftQ I
        (Submodule.mkQ (IsLocalRing.maximalIdeal S)) (by rwa [Submodule.ker_mkQ])))
      (by rw [← ModuleCat.ofHom_comp]; exact congrArg _ (LinearMap.ext fun a => by
        obtain ⟨x, hx, hxa⟩ := Submodule.mem_map.mp a.2
        simp only [LinearMap.comp_apply, Submodule.coe_subtype, ← hxa]
        exact (Submodule.Quotient.mk_eq_zero _).mpr hx))).ShortExact := by
  refine ModuleCat.shortComplex_shortExact _ ?_ ?_ ?_
  · exact LinearMap.exact_iff.mpr ((Submodule.ker_liftQ _ _ _).trans
      (by simp only [Submodule.ker_mkQ]; exact (Submodule.range_subtype _).symm))
  · exact Submodule.injective_subtype _
  · exact LinearMap.range_eq_top.mp
      ((Submodule.range_liftQ _ _ _).trans (Submodule.range_mkQ _))
abbrev

KwFF13Stacks10_99_8Pinned

L497 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.KwFF13Stacks10_99_8Pinned
Documentation

The local flatness criterion reducing residue-field Tor vanishing to Tor and flatness over the base residue quotient.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
abbrev KwFF13Stacks10_99_8Pinned : Prop
abbrev

KwFF13ResidueQuotKerTensorInjPinned

L513 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.KwFF13ResidueQuotKerTensorInjPinned
Documentation

Injectivity of the tensor inclusion of the maximal ideal image in the base residue quotient under fibral flatness.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
abbrev KwFF13ResidueQuotKerTensorInjPinned : Prop
theorem

kwFF13_idealMap_restrictScalars_eq_submoduleMap

L532 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.kwFF13_idealMap_restrictScalars_eq_submoduleMap
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section BaseChange
variable {S S' : Type u} [CommRing S] [CommRing S'] [Algebra S S']
variable (I : Ideal S)
Lean source · statement
theorem kwFF13_idealMap_restrictScalars_eq_submoduleMap (J : Ideal S) :
    ((J.map (Ideal.Quotient.mk I) : Ideal (S ⧸ I)) : Submodule (S ⧸ I) (S ⧸ I)).restrictScalars S
      = Submodule.map (Submodule.mkQ I) (J : Submodule S S)
theorem

kwFF13_restrictScalars_subtype_rTensor_inj_of_flat

L540 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.kwFF13_restrictScalars_subtype_rTensor_inj_of_flat
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section BaseChange
variable {S S' : Type u} [CommRing S] [CommRing S'] [Algebra S S']
variable (I : Ideal S)
Lean source · statement
theorem kwFF13_restrictScalars_subtype_rTensor_inj_of_flat
    (K' : Ideal (S ⧸ I)) [Module.Flat (S ⧸ I) ((S ⧸ I) ⊗[S] S')] :
    Function.Injective
      ((Submodule.subtype ((K' : Submodule (S ⧸ I) (S ⧸ I)).restrictScalars S)).rTensor S')
theorem

kwFF13_residueQuotKerTensorInjPinned_proved

L574 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.kwFF13_residueQuotKerTensorInjPinned_proved
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
theorem kwFF13_residueQuotKerTensorInjPinned_proved :
    KwFF13ResidueQuotKerTensorInjPinned.{u}
theorem

kwFF13_stacks10_99_8Pinned_of_KPinned

L596 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.kwFF13_stacks10_99_8Pinned_of_KPinned
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
theorem kwFF13_stacks10_99_8Pinned_of_KPinned
    (hKp : KwFF13ResidueQuotKerTensorInjPinned.{u}) : KwFF13Stacks10_99_8Pinned.{u}
theorem

localCriterion00MK_stub

L608 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ.LocalCritPort.localCriterion00MK_stub
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
theorem localCriterion00MK_stub {R S M : Type u} [CommRing R] [CommRing S]
    [Algebra R S] [IsLocalRing R] [IsLocalRing S] [AddCommGroup M]
    [Module R M] [Module S M] [IsScalarTower R S M]
    (hR : IsNoetherianRing R) (hS : IsNoetherianRing S)
    (hloc : IsLocalHom (algebraMap R S)) (hfin : Module.Finite S M)
    (hκ : Igw157LcTor1ResidueVanishing R M) : Module.Flat R M
theorem

flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ

L623 ↗
IsLocalRing.flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
open LocalCritPort in
Lean source · full declaration
theorem _root_.IsLocalRing.flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
    {R S S' : Type u} [CommRing R] [CommRing S] [CommRing S']
    [Algebra R S] [Algebra S S'] [Algebra R S'] [IsScalarTower R S S']
    [IsLocalRing R] [IsLocalRing S] [IsLocalRing S']
    [IsLocalHom (algebraMap R S)] [IsLocalHom (algebraMap S S')]
    [IsNoetherianRing S] [IsNoetherianRing S'] :
    letI : Algebra (S ⧸ (IsLocalRing.maximalIdeal R).map (algebraMap R S))
        (S' ⧸ (IsLocalRing.maximalIdeal R).map (algebraMap R S')) :=
      Ideal.Quotient.algebraQuotientOfLEComap (Ideal.map_le_iff_le_comap.mp (le_of_eq
        (by rw [Ideal.map_map, ← IsScalarTower.algebraMap_eq R S S'])))
    Module.Flat R S' →
    Module.Flat (S ⧸ (IsLocalRing.maximalIdeal R).map (algebraMap R S))
        (S' ⧸ (IsLocalRing.maximalIdeal R).map (algebraMap R S')) →
    Module.Flat S S' := by
  intro hflat hfib
  exact localCriterion00MK_stub (R := S) (S := S') (M := S') ‹_› ‹_› inferInstance inferInstance
    ((kwFF13_stacks10_99_8Pinned_of_KPinned kwFF13_residueQuotKerTensorInjPinned_proved)
      R S S'
      ((kwFF9_torVanish_of_idealRTensorInj
        (kwFF10_idealRTensorInj_of_towerFactor kwFF11_idealTowerTensorFactor_proved))
        R S S' hflat)
      hfib)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.