Module

Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField

39 declarations indexed from sourceView source ↗

Module documentation

Module flat of is Local Hom of finite of is Zero tor one residue Field

Imports35

Lean.Elab.Tactic.Ext
Lean.Elab.Tactic.Omega
Mathlib.Algebra.Category.ModuleCat.Basic
Mathlib.Algebra.Category.ModuleCat.EpiMono
Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Mathlib.Algebra.Category.ModuleCat.Projective
Mathlib.Algebra.Homology.Additive
Mathlib.Algebra.Homology.HomologicalComplexAbelian
Mathlib.Algebra.Homology.HomologySequence
Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Mathlib.Algebra.Homology.ShortComplex.ShortExact
Mathlib.Algebra.Module.Torsion.Basic
Mathlib.CategoryTheory.Abelian.LeftDerived
Mathlib.CategoryTheory.Abelian.Projective.Resolution
Mathlib.CategoryTheory.Monoidal.Braided.Basic
Mathlib.CategoryTheory.Monoidal.Preadditive
Mathlib.CategoryTheory.Monoidal.Tor
Mathlib.LinearAlgebra.TensorProduct.Pi
Mathlib.LinearAlgebra.TensorProduct.RightExactness
Mathlib.RingTheory.Artinian.Module
Mathlib.RingTheory.Filtration
Mathlib.RingTheory.FiniteLength
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.Finiteness.Cardinality
Mathlib.RingTheory.Flat.Basic
Mathlib.RingTheory.Flat.CategoryTheory
Mathlib.RingTheory.Flat.Tensor
Mathlib.RingTheory.LocalRing.ResidueField.Basic
Mathlib.RingTheory.LocalRing.ResidueField.Defs
Mathlib.RingTheory.LocalRing.RingHom.Basic
Mathlib.RingTheory.Noetherian.Basic
Mathlib.RingTheory.SimpleModule.Basic
Mathlib.Tactic.CategoryTheory.Slice
Mathlib.Tactic.Simps.Basic

Imported by2

abbrev

Tor1ResVanishing

L66 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.Tor1ResVanishing

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.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port

Lean source · statement

abbrev Tor1ResVanishing (R : Type u) [CommRing R] [IsLocalRing R]
    (M : Type u) [AddCommGroup M] [Module R M] : Prop

theorem

torLES_tensorRight_shortExact

L74 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.torLES_tensorRight_shortExact

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

L81 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.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.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

L94 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.torLES_resolutionTensorSES_shortExact

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

L104 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.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.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

L110 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.torLES_torMap_app_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

L120 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.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.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

L128 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.torLES_torMap_comp_eq_zero

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

L142 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.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.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

L154 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.torLES_torDelta_comp_eq_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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₂

L166 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.torLES_tor_exact₂

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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₃

L182 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.torLES_tor_exact₃

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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₁

L197 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.torLES_tor_exact₁

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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₂

L212 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.torLES_tor_isZero_X₂

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

L224 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.torFV_resolutionTensor_exactAt

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

L231 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.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.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

L238 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.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.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

L244 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.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.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

L249 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.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.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

L258 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.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.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

L268 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.ar_opcyclesMap_fromLeftDerivedZero'_naturality

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

L285 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.ar_tor0_map_fromLeftDerivedZero_naturality

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
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

ar_rTensor_injective_of_tor1_isZero

L353 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.ar_rTensor_injective_of_tor1_isZero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
section TorZeroBridge
variable {R : Type u} [CommRing R]

Lean source · statement

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

theorem

ar_isSemisimpleModule_of_isTorsionBySet_isMaximal

L405 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.ar_isSemisimpleModule_of_isTorsionBySet_isMaximal

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
section FiniteLengthSupply
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ar_isSemisimpleModule_of_isTorsionBySet_isMaximal
    (I : Ideal R) [I.IsMaximal] (M : Type u) [AddCommGroup M] [Module R M]
    (htor : Module.IsTorsionBySet R M (I : Set R)) :
    IsSemisimpleModule R M

theorem

ar_isFiniteLength_of_finite_of_torsionBySet_pow

L413 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.ar_isFiniteLength_of_finite_of_torsionBySet_pow

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
section FiniteLengthSupply
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ar_isFiniteLength_of_finite_of_torsionBySet_pow
    [IsLocalRing R] [IsNoetherianRing R] (n : ℕ) (M : Type u) [AddCommGroup M]
    [Module R M] [Module.Finite R M]
    (htor : Module.IsTorsionBySet R M ((IsLocalRing.maximalIdeal R ^ n : Ideal R) : Set R)) :
    IsFiniteLength R M

theorem

ar_isFiniteLength_quotient_pow_smul

L473 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.ar_isFiniteLength_quotient_pow_smul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
section FiniteLengthSupply
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ar_isFiniteLength_quotient_pow_smul [IsLocalRing R] [IsNoetherianRing R]
    (n : ℕ) :
    IsFiniteLength R
      (R ⧸ ((IsLocalRing.maximalIdeal R ^ n : Ideal R) • ⊤ : Submodule R R))

theorem

ar_tmul_mem_smul_top

L495 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.ar_tmul_mem_smul_top

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
section DepthBookkeeping
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ar_tmul_mem_smul_top {B M : Type u} [AddCommGroup B] [Module R B]
    [AddCommGroup M] [Module R M] (a : Ideal R) (P : Submodule R B) {v : B}
    (hv : v ∈ a • P) (m : M) (hvP : v ∈ P) :
    ((⟨v, hvP⟩ : ↥P) ⊗ₜ[R] m) ∈ a • (⊤ : Submodule R (↥P ⊗[R] M))

theorem

ar_rTensor_inclusion_apply_mem_smul

L512 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.ar_rTensor_inclusion_apply_mem_smul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
section DepthBookkeeping
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ar_rTensor_inclusion_apply_mem_smul {B M : Type u} [AddCommGroup B]
    [Module R B] [AddCommGroup M] [Module R M] (a : Ideal R) {N P : Submodule R B}
    (hNP : N ≤ P) (hNa : N ≤ a • P) (y : ↥N ⊗[R] M) :
    LinearMap.rTensor M (Submodule.inclusion hNP) y ∈
      a • (⊤ : Submodule R (↥P ⊗[R] M))

theorem

ar_mem_smul_pow_extend

L523 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.ar_mem_smul_pow_extend

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
section DepthBookkeeping
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ar_mem_smul_pow_extend {S : Type v} [CommRing S] [Algebra R S]
    [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] {W : Type u}
    [AddCommGroup W] [Module R W] [Module S W] [IsScalarTower R S W] (k : ℕ) {z : W}
    (hz : z ∈ ((IsLocalRing.maximalIdeal R ^ k : Ideal R) • ⊤ : Submodule R W)) :
    z ∈ ((IsLocalRing.maximalIdeal S ^ k : Ideal S) • ⊤ : Submodule S W)

theorem

ar_finite_tensorProduct_left

L537 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.ar_finite_tensorProduct_left

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
section DepthBookkeeping
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ar_finite_tensorProduct_left (S : Type v) [CommRing S] [Algebra R S]
    (M N : Type u) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [AddCommGroup N] [Module R N] [Module.Finite S M] [Module.Finite R N] :
    Module.Finite S (M ⊗[R] N)

theorem

ar_mem_range_rTensor_inf_of_ker

L563 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.ar_mem_range_rTensor_inf_of_ker

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
section ArtinReesTail
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ar_mem_range_rTensor_inf_of_ker {M : Type u} [AddCommGroup M]
    [Module R M] (I : Ideal R) (J : Submodule R R)
    (htor1 : ∀ W : Submodule R (R ⧸ J),
      IsZero (((Tor (ModuleCat.{u} R) 1).obj (ModuleCat.of R ((R ⧸ J) ⧸ W))).obj
        (ModuleCat.of R M)))
    {x : ↥I ⊗[R] M} (hx : LinearMap.rTensor M (Submodule.subtype I) x = 0) :
    x ∈ Set.range (LinearMap.rTensor M
      (Submodule.inclusion (inf_le_right : J ⊓ (I : Submodule R R) ≤ I)))

theorem

ar_flat_of_finiteLength_tor1_isZero

L596 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.ar_flat_of_finiteLength_tor1_isZero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
section ArtinReesTail
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ar_flat_of_finiteLength_tor1_isZero (R' : Type u) (S : Type v) (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)
    (htor : ∀ (N : Type u) [AddCommGroup N] [Module R' N], IsFiniteLength R' N →
      IsZero (((Tor (ModuleCat.{u} R') 1).obj (ModuleCat.of R' N)).obj
        (ModuleCat.of R' M))) :
    Module.Flat R' M

theorem

ar_flat_of_finiteLength_tor1_isZero_00MK

L664 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.ar_flat_of_finiteLength_tor1_isZero_00MK

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
section ArtinReesTail
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ar_flat_of_finiteLength_tor1_isZero_00MK (R' : Type u) (S : Type v) (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)
    (htor : ∀ (N : Type u) [AddCommGroup N] [Module R' N], IsFiniteLength R' N →
      IsZero (((Tor (ModuleCat R') 1).obj (ModuleCat.of R' N)).obj
        (ModuleCat.of R' M))) :
    Module.Flat R' M

theorem

dv_tor_isZero_of_iso

L681 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.dv_tor_isZero_of_iso

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
section Devissage
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

dv_simple_equiv_residueField

L686 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.dv_simple_equiv_residueField

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
section Devissage
variable {R : Type u} [CommRing R]

Lean source · statement

theorem dv_simple_equiv_residueField (R : Type u) [CommRing R] [IsLocalRing R]
    (S : Type u) [AddCommGroup S] [Module R S] [IsSimpleModule R S] :
    Nonempty (S ≃ₗ[R] IsLocalRing.ResidueField R)

theorem

dv_tor1_simple_isZero

L693 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.dv_tor1_simple_isZero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
section Devissage
variable {R : Type u} [CommRing R]

Lean source · statement

theorem dv_tor1_simple_isZero (R : Type u) [CommRing R] [IsLocalRing R]
    {M : Type u} [AddCommGroup M] [Module R M]
    (hκ : IsZero (((Tor (ModuleCat.{u} R) 1).obj
      (ModuleCat.of R (IsLocalRing.ResidueField R))).obj (ModuleCat.of R M)))
    (S : Type u) [AddCommGroup S] [Module R S] [IsSimpleModule R S] :
    IsZero (((Tor (ModuleCat.{u} R) 1).obj (ModuleCat.of R S)).obj (ModuleCat.of R M))

theorem

dv_tor1_isZero_of_isFiniteLength

L702 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.dv_tor1_isZero_of_isFiniteLength

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
section Devissage
variable {R : Type u} [CommRing R]

Lean source · statement

theorem dv_tor1_isZero_of_isFiniteLength {R : Type u} [CommRing R] [IsLocalRing R]
    {M : Type u} [AddCommGroup M] [Module R M]
    (hκ : IsZero (((Tor (ModuleCat.{u} R) 1).obj
      (ModuleCat.of R (IsLocalRing.ResidueField R))).obj (ModuleCat.of R M)))
    (N : Type u) [AddCommGroup N] [Module R N] (hN : IsFiniteLength R N) :
    IsZero (((Tor (ModuleCat.{u} R) 1).obj (ModuleCat.of R N)).obj (ModuleCat.of R M))

theorem

dv_tor1_isZero_of_isFiniteLength_00MK

L721 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField.MK00Port.dv_tor1_isZero_of_isFiniteLength_00MK

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
noncomputable section
namespace MK00Port
section Devissage
variable {R : Type u} [CommRing R]

Lean source · statement

theorem dv_tor1_isZero_of_isFiniteLength_00MK (R M : Type u) [CommRing R]
    [IsLocalRing R] [AddCommGroup M] [Module R M]
    (hκ : Tor1ResVanishing R M)
    (N : Type u) [AddCommGroup N] [Module R N] (hN : IsFiniteLength R N) :
    IsZero (((Tor (ModuleCat R) 1).obj (ModuleCat.of R N)).obj (ModuleCat.of R M))

theorem

flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField

L734 ↗

Module.flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
universe u v
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory TensorProduct
open CategoryTheory CategoryTheory.Limits MK00Port IsLocalRing in

Lean source · statement

theorem _root_.Module.flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
    {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
    [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)]
    [IsNoetherianRing R] [IsNoetherianRing S]
    {M : Type u} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [Module.Finite S M]
    (hκ : IsZero (((Tor (ModuleCat.{u} R) 1).obj
      (ModuleCat.of R (ResidueField R))).obj (ModuleCat.of R M))) :
    Module.Flat R M

Module documentation

Module flat of is Local Hom of finite of is Zero tor one residue Field

Declarations