NYLL
Module

IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.lean

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

Module documentation

A flatness criterion for a tower of local rings and its residue quotient.

Imports2
Imported by2

Declarations

abbrev

Igw157LcTor1ResidueVanishing

L32 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.Igw157LcTor1ResidueVanishing
Documentation

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

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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
abbrev Igw157LcTor1ResidueVanishing (R : Type) [CommRing R] [IsLocalRing R]
    (M : Type) [AddCommGroup M] [Module R M] : Prop
theorem

torLES_tensorRight_shortExact

L40 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.torLES_tensorRight_shortExact
Source context 8 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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section TorLES
variable {R : Type} [CommRing R]
Lean source · statement
theorem torLES_tensorRight_shortExact {S : ShortComplex (ModuleCat.{0} R)}
    (hS : S.ShortExact) (M : ModuleCat.{0} R) [Module.Flat R M] :
    (S.map (tensorRight M)).ShortExact
def

torLES_resolutionTensorSES

L47 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.torLES_resolutionTensorSES
Documentation

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

Source context 8 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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section TorLES
variable {R : Type} [CommRing R]
Lean source · statement
def torLES_resolutionTensorSES (S : ShortComplex (ModuleCat.{0} R))
    {Y : ModuleCat.{0} R} (P : ProjectiveResolution Y) :
    ShortComplex (HomologicalComplex (ModuleCat.{0} R) (ComplexShape.down ℕ))
theorem

torLES_resolutionTensorSES_shortExact

L60 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.torLES_resolutionTensorSES_shortExact
Source context 8 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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section TorLES
variable {R : Type} [CommRing R]
Lean source · statement
theorem torLES_resolutionTensorSES_shortExact (S : ShortComplex (ModuleCat.{0} R))
    (hS : S.ShortExact) {Y : ModuleCat.{0} R} (P : ProjectiveResolution Y) :
    (torLES_resolutionTensorSES S P).ShortExact
def

torLES_torIso

L70 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.torLES_torIso
Documentation

Identify Tor with the homology of the tensor product with the chosen 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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section TorLES
variable {R : Type} [CommRing R]
variable {Y : ModuleCat.{0} R} (P : ProjectiveResolution Y)
Lean source · statement
def torLES_torIso (X : ModuleCat.{0} R) (n : ℕ) :
    ((Tor (ModuleCat.{0} R) n).obj X).obj Y ≅
      ((((curriedTensor (ModuleCat.{0} R)).obj X).mapHomologicalComplex
        (ComplexShape.down ℕ)).obj P.complex).homology n
theorem

torLES_torMap_app_eq

L76 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.torLES_torMap_app_eq
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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section TorLES
variable {R : Type} [CommRing R]
variable {Y : ModuleCat.{0} R} (P : ProjectiveResolution Y)
Lean source · statement
theorem torLES_torMap_app_eq {X X' : ModuleCat.{0} R} (f : X ⟶ X') (n : ℕ) :
    ((Tor (ModuleCat.{0} R) n).map f).app Y =
      (torLES_torIso P X n).hom ≫
        HomologicalComplex.homologyMap
          ((NatTrans.mapHomologicalComplex ((curriedTensor (ModuleCat.{0} R)).map f)
            (ComplexShape.down ℕ)).app P.complex) n ≫
        (torLES_torIso P X' n).inv
def

torLES_torDelta

L86 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.torLES_torDelta
Documentation

The connecting map in the Tor long exact sequence, computed using the chosen 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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section TorLES
variable {R : Type} [CommRing R]
variable {Y : ModuleCat.{0} R} (P : ProjectiveResolution Y)
Lean source · statement
def torLES_torDelta (S : ShortComplex (ModuleCat.{0} R))
    (hS : S.ShortExact) (n : ℕ) :
    ((Tor (ModuleCat.{0} R) (n + 1)).obj S.X₃).obj Y ⟶
      ((Tor (ModuleCat.{0} R) n).obj S.X₁).obj Y
theorem

torLES_torMap_comp_eq_zero

L94 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.torLES_torMap_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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section TorLES
variable {R : Type} [CommRing R]
variable {Y : ModuleCat.{0} R} (P : ProjectiveResolution Y)
include P in
Lean source · statement
theorem torLES_torMap_comp_eq_zero (S : ShortComplex (ModuleCat.{0} R)) (n : ℕ) :
    ((Tor (ModuleCat.{0} R) n).map S.f).app Y ≫
      ((Tor (ModuleCat.{0} R) n).map S.g).app Y = 0
theorem

torLES_torMap_comp_torDelta_eq_zero

L108 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.torLES_torMap_comp_torDelta_eq_zero
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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section TorLES
variable {R : Type} [CommRing R]
variable {Y : ModuleCat.{0} R} (P : ProjectiveResolution Y)
Lean source · statement
theorem torLES_torMap_comp_torDelta_eq_zero (S : ShortComplex (ModuleCat.{0} R))
    (hS : S.ShortExact) (n : ℕ) :
    ((Tor (ModuleCat.{0} R) (n + 1)).map S.g).app Y ≫ torLES_torDelta P S hS n = 0
theorem

torLES_torDelta_comp_eq_zero

L120 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.torLES_torDelta_comp_eq_zero
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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section TorLES
variable {R : Type} [CommRing R]
variable {Y : ModuleCat.{0} R} (P : ProjectiveResolution Y)
Lean source · statement
theorem torLES_torDelta_comp_eq_zero (S : ShortComplex (ModuleCat.{0} R))
    (hS : S.ShortExact) (n : ℕ) :
    torLES_torDelta P S hS n ≫ ((Tor (ModuleCat.{0} R) n).map S.f).app Y = 0
theorem

torLES_tor_exact₂

L132 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.torLES_tor_exact₂
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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section TorLES
variable {R : Type} [CommRing R]
variable {Y : ModuleCat.{0} R} (P : ProjectiveResolution Y)
Lean source · statement
theorem torLES_tor_exact₂ (S : ShortComplex (ModuleCat.{0} R)) (hS : S.ShortExact)
    (n : ℕ) :
    (ShortComplex.mk (((Tor (ModuleCat.{0} R) n).map S.f).app Y)
      (((Tor (ModuleCat.{0} R) n).map S.g).app Y)
      (torLES_torMap_comp_eq_zero P S n)).Exact
theorem

torLES_tor_exact₃

L148 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.torLES_tor_exact₃
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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section TorLES
variable {R : Type} [CommRing R]
variable {Y : ModuleCat.{0} R} (P : ProjectiveResolution Y)
Lean source · statement
theorem torLES_tor_exact₃ (S : ShortComplex (ModuleCat.{0} R)) (hS : S.ShortExact)
    (n : ℕ) :
    (ShortComplex.mk (((Tor (ModuleCat.{0} 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₁

L163 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.torLES_tor_exact₁
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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section TorLES
variable {R : Type} [CommRing R]
variable {Y : ModuleCat.{0} R} (P : ProjectiveResolution Y)
Lean source · statement
theorem torLES_tor_exact₁ (S : ShortComplex (ModuleCat.{0} R)) (hS : S.ShortExact)
    (n : ℕ) :
    (ShortComplex.mk (torLES_torDelta P S hS n)
      (((Tor (ModuleCat.{0} R) n).map S.f).app Y)
      (torLES_torDelta_comp_eq_zero P S hS n)).Exact
theorem

torFV_resolutionTensor_exactAt

L183 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.torFV_resolutionTensor_exactAt
Source context 8 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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section TorFV
variable {R : Type} [CommRing R]
Lean source · statement
theorem torFV_resolutionTensor_exactAt (M : ModuleCat.{0} R) [Module.Flat R M]
    {Y : ModuleCat.{0} R} (P : ProjectiveResolution Y) (n : ℕ) :
    ((((curriedTensor (ModuleCat.{0} R)).obj M).mapHomologicalComplex
      (ComplexShape.down ℕ)).obj P.complex).ExactAt (n + 1)
theorem

torFV_tor_succ_isZero_of_flat_res

L190 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.torFV_tor_succ_isZero_of_flat_res
Source context 8 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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section TorFV
variable {R : Type} [CommRing R]
Lean source · statement
theorem torFV_tor_succ_isZero_of_flat_res (M : ModuleCat.{0} R) [Module.Flat R M]
    {Y : ModuleCat.{0} R} (P : ProjectiveResolution Y) (n : ℕ) :
    IsZero (((Tor (ModuleCat.{0} R) (n + 1)).obj M).obj Y)
theorem

torFV_tor_succ_isZero_of_flat

L197 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.torFV_tor_succ_isZero_of_flat
Source context 8 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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section TorFV
variable {R : Type} [CommRing R]
Lean source · statement
theorem torFV_tor_succ_isZero_of_flat (M : ModuleCat.{0} R) [Module.Flat R M]
    (Y : ModuleCat.{0} R) (n : ℕ) :
    IsZero (((Tor (ModuleCat.{0} R) (n + 1)).obj M).obj Y)
theorem

torFV_tor_one_isZero_of_flat

L203 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.torFV_tor_one_isZero_of_flat
Source context 8 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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section TorFV
variable {R : Type} [CommRing R]
Lean source · statement
theorem torFV_tor_one_isZero_of_flat (M : ModuleCat.{0} R) [Module.Flat R M]
    (Y : ModuleCat.{0} R) :
    IsZero (((Tor (ModuleCat.{0} R) 1).obj M).obj Y)
theorem

tor0_opcyclesMap_fromLeftDerivedZero'_naturality

L213 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.tor0_opcyclesMap_fromLeftDerivedZero'_naturality
Source context 8 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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section Tor0Nat
variable {R : Type} [CommRing R]
Lean source · statement
theorem tor0_opcyclesMap_fromLeftDerivedZero'_naturality
    {Y : ModuleCat.{0} R} (P : ProjectiveResolution Y) {X X' : ModuleCat.{0} R}
    (f : X ⟶ X') :
    HomologicalComplex.opcyclesMap
        ((NatTrans.mapHomologicalComplex ((curriedTensor (ModuleCat.{0} R)).map f)
          (ComplexShape.down ℕ)).app P.complex) 0 ≫
        P.fromLeftDerivedZero' ((curriedTensor (ModuleCat.{0} R)).obj X') =
      P.fromLeftDerivedZero' ((curriedTensor (ModuleCat.{0} R)).obj X) ≫
        ((curriedTensor (ModuleCat.{0} R)).map f).app Y
theorem

tor0_tor0_map_fromLeftDerivedZero_naturality

L230 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.tor0_tor0_map_fromLeftDerivedZero_naturality
Source context 8 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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section Tor0Nat
variable {R : Type} [CommRing R]
Lean source · statement
theorem tor0_tor0_map_fromLeftDerivedZero_naturality
    {Y : ModuleCat.{0} R} (P : ProjectiveResolution Y) {X X' : ModuleCat.{0} R}
    (f : X ⟶ X') :
    ((Tor (ModuleCat.{0} R) 0).map f).app Y ≫
        ((curriedTensor (ModuleCat.{0} R)).obj X').fromLeftDerivedZero.app Y =
      ((curriedTensor (ModuleCat.{0} R)).obj X).fromLeftDerivedZero.app Y ≫
        ((curriedTensor (ModuleCat.{0} R)).map f).app Y
theorem

kwFF9_tor0_map_mono_of_rTensor_injective

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

kwFF9_tor1_isZero_of_flat_of_rTensor_inj

L328 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.kwFF9_tor1_isZero_of_flat_of_rTensor_inj
Source context 8 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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section FF9Engine
variable {R : Type} [CommRing R]
Lean source · statement
theorem kwFF9_tor1_isZero_of_flat_of_rTensor_inj
    (S : ShortComplex (ModuleCat.{0} R)) (hS : S.ShortExact) [Module.Flat R S.X₂]
    (Y : ModuleCat.{0} R)
    (hinj : Function.Injective (LinearMap.rTensor Y S.f.hom)) :
    IsZero (((Tor (ModuleCat.{0} R) 1).obj S.X₃).obj Y)
theorem

kwFF9_idealSES_shortExact

L343 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.kwFF9_idealSES_shortExact
Source context 8 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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section FF9Engine
variable {R : Type} [CommRing R]
Lean source · full declaration
theorem kwFF9_idealSES_shortExact {S : Type} [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

L352 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.kwFF12_tor1_isZero_of_tor1_of_rTensor_inj
Source context 8 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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section FF9Engine
variable {R : Type} [CommRing R]
Lean source · statement
theorem kwFF12_tor1_isZero_of_tor1_of_rTensor_inj
    (S : ShortComplex (ModuleCat.{0} R)) (hS : S.ShortExact) (Y : ModuleCat.{0} R)
    (h2 : IsZero (((Tor (ModuleCat.{0} R) 1).obj S.X₂).obj Y))
    (hinj : Function.Injective (LinearMap.rTensor Y S.f.hom)) :
    IsZero (((Tor (ModuleCat.{0} R) 1).obj S.X₃).obj Y)
abbrev

KwFF3Tor1IdealVanishing

L368 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.KwFF3Tor1IdealVanishing
Documentation

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

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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
abbrev KwFF3Tor1IdealVanishing (R : Type) [CommRing R] (I : Ideal R)
    (M : Type) [AddCommGroup M] [Module R M] : Prop
abbrev

KwFibralFlatTor1Vanish

L374 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.KwFibralFlatTor1Vanish
Documentation

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

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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
abbrev KwFibralFlatTor1Vanish : Prop
abbrev

KwFF9IdealRTensorInj

L383 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.KwFF9IdealRTensorInj
Documentation

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

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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
abbrev KwFF9IdealRTensorInj : Prop
theorem

kwFF9_torVanish_of_idealRTensorInj

L392 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.kwFF9_torVanish_of_idealRTensorInj
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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
theorem kwFF9_torVanish_of_idealRTensorInj (hInj : KwFF9IdealRTensorInj) :
    KwFibralFlatTor1Vanish
abbrev

KwFF10IdealTowerTensorFactor

L401 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.KwFF10IdealTowerTensorFactor
Documentation

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

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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
abbrev KwFF10IdealTowerTensorFactor : Prop
theorem

kwFF10_idealRTensorInj_of_towerFactor

L412 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.kwFF10_idealRTensorInj_of_towerFactor
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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
theorem kwFF10_idealRTensorInj_of_towerFactor (hFactor : KwFF10IdealTowerTensorFactor) :
    KwFF9IdealRTensorInj
theorem

kwFF11_idealTowerTensorFactor_proved

L424 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.kwFF11_idealTowerTensorFactor_proved
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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
theorem kwFF11_idealTowerTensorFactor_proved : KwFF10IdealTowerTensorFactor
theorem

kwFF12_residueQuotSES_shortExact

L475 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.kwFF12_residueQuotSES_shortExact
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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · full declaration
theorem kwFF12_residueQuotSES_shortExact {S : Type} [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

L495 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.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 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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
abbrev KwFF13Stacks10_99_8Pinned : Prop
abbrev

KwFF13ResidueQuotKerTensorInjPinned

L511 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.KwFF13ResidueQuotKerTensorInjPinned
Documentation

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

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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
abbrev KwFF13ResidueQuotKerTensorInjPinned : Prop
theorem

kwFF13_idealMap_restrictScalars_eq_submoduleMap

L530 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.kwFF13_idealMap_restrictScalars_eq_submoduleMap
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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section BaseChange
variable {S S' : Type} [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

L538 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.kwFF13_restrictScalars_subtype_rTensor_inj_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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
section BaseChange
variable {S S' : Type} [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

L572 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.kwFF13_residueQuotKerTensorInjPinned_proved
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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
theorem kwFF13_residueQuotKerTensorInjPinned_proved :
    KwFF13ResidueQuotKerTensorInjPinned
theorem

kwFF13_stacks10_99_8Pinned_of_KPinned

L594 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.kwFF13_stacks10_99_8Pinned_of_KPinned
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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
theorem kwFF13_stacks10_99_8Pinned_of_KPinned
    (hKp : KwFF13ResidueQuotKerTensorInjPinned) : KwFF13Stacks10_99_8Pinned
theorem

localCriterion00MK_stub

L606 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map.LocalCritPort.localCriterion00MK_stub
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
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace LocalCritPort
Lean source · statement
theorem localCriterion00MK_stub {R S M : Type} [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

L621 ↗
IsLocalRing.flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map
Source context 5 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
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
    {R S S' : Type} [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.