NYLL
Module

TensorExactness.lean

Nyll.SchemeTheory.RingTheory.Flat.TensorExactness
27 declarations indexed from sourceView source ↗

Module documentation

Tensor exactness and covering diagrams

The tensor functor retains independent base-ring, tensor-factor and source universes. Its right exactness follows from an explicitly constructed tensor-Hom adjunction in the larger module universe and a proved natural comparison with universe lifting.

The categorical covering diagrams construct their kernel lifts and cokernel descents. They can be used without reopening the concrete module instances of every diagram object.

Imports11
  • Mathlib.Algebra.Category.ModuleCat.Ulift
  • Mathlib.Algebra.Category.ModuleCat.EpiMono
  • Mathlib.Algebra.Homology.ShortComplex.Exact
  • Mathlib.CategoryTheory.Adjunction.Limits
  • Mathlib.CategoryTheory.Limits.Preserves.Finite
  • Mathlib.LinearAlgebra.TensorProduct.Basic
  • Mathlib.LinearAlgebra.TensorProduct.Map
  • Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
  • Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  • Mathlib.CategoryTheory.Abelian.Basic
Imported by1

Declarations

def

tensorFunctor

L39 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorFunctor
Documentation

The same concrete tensor functor, polymorphic in the source carrier universe.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · full declaration
def tensorFunctor {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M] :
    ModuleCat.{w} R ⥤ ModuleCat.{max v w} R where
  obj N := ModuleCat.of R (M ⊗[R] N)
  map f := ModuleCat.ofHom (f.hom.lTensor M)
  map_id N := by
    apply ModuleCat.hom_ext
    exact LinearMap.lTensor_id M N
  map_comp f g := by
    apply ModuleCat.hom_ext
    exact LinearMap.lTensor_comp M g.hom f.hom
def

postcompose

L59 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.postcompose
Documentation

The actual linear map of postcomposition on a Hom module.

Source context 9 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
section NativeHomFactories
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]
variable {X : Type a} [AddCommGroup X] [Module R X]
variable {Y : Type b} [AddCommGroup Y] [Module R Y]
Lean source · full declaration
def postcompose (f : X →ₗ[R] Y) : (M →ₗ[R] X) →ₗ[R] (M →ₗ[R] Y) where
  toFun g := f ∘ₗ g
  map_add' g h := LinearMap.comp_add g h f
  map_smul' r g := LinearMap.comp_smul f r g
def

curryFlip

L65 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.curryFlip
Documentation

Curry in the orientation needed for M ⊗ - ⊣ Hom(M,-).

Source context 9 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
section NativeHomFactories
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]
variable {X : Type a} [AddCommGroup X] [Module R X]
variable {Y : Type b} [AddCommGroup Y] [Module R Y]
Lean source · statement
def curryFlip (f : M ⊗[R] X →ₗ[R] Y) : X →ₗ[R] M →ₗ[R] Y
def

uncurryFlip

L69 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.uncurryFlip
Documentation

The actual bilinear lift inverse to curryFlip.

Source context 9 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
section NativeHomFactories
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]
variable {X : Type a} [AddCommGroup X] [Module R X]
variable {Y : Type b} [AddCommGroup Y] [Module R Y]
Lean source · statement
def uncurryFlip (f : X →ₗ[R] M →ₗ[R] Y) : M ⊗[R] X →ₗ[R] Y
theorem

uncurryFlip_curryFlip

L72 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.uncurryFlip_curryFlip
Source context 9 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
section NativeHomFactories
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]
variable {X : Type a} [AddCommGroup X] [Module R X]
variable {Y : Type b} [AddCommGroup Y] [Module R Y]
Lean source · statement
theorem uncurryFlip_curryFlip (f : M ⊗[R] X →ₗ[R] Y) :
    uncurryFlip (curryFlip f) = f
theorem

curryFlip_uncurryFlip

L78 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.curryFlip_uncurryFlip
Source context 9 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
section NativeHomFactories
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]
variable {X : Type a} [AddCommGroup X] [Module R X]
variable {Y : Type b} [AddCommGroup Y] [Module R Y]
Lean source · statement
theorem curryFlip_uncurryFlip (f : X →ₗ[R] M →ₗ[R] Y) :
    curryFlip (uncurryFlip f) = f
def

tensorHomObject

L89 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorHomObject
Documentation

The actual Hom module object, constructed once at its own owner boundary.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · statement
def tensorHomObject {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M] (X : ModuleCat.{max u v} R) :
    ModuleCat.{max u v} R
def

tensorHomMap

L94 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorHomMap
Documentation

The actual native postcomposition arrow between the constructed Hom objects.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · statement
def tensorHomMap {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    {X Y : ModuleCat.{max u v} R} (f : X ⟶ Y) :
    tensorHomObject M X ⟶ tensorHomObject M Y
def

tensorHomFunctor

L101 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorHomFunctor
Documentation

Hom(M,-) in a universe large enough to contain M and all its values.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · full declaration
def tensorHomFunctor {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M] :
    ModuleCat.{max u v} R ⥤ ModuleCat.{max u v} R where
  obj N := tensorHomObject M N
  map f := tensorHomMap M f
  map_id N := by
    change tensorHomMap M (𝟙 N) = 𝟙 (tensorHomObject M N)
    rfl
  map_comp f g := by
    change tensorHomMap M (f ≫ g) = tensorHomMap M f ≫ tensorHomMap M g
    rfl
def

tensorCurryHom

L114 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorCurryHom
Documentation

The actual forward arrow of the tensor-Hom correspondence.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · statement
def tensorCurryHom {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    {X Y : ModuleCat.{max u v} R} (f : (tensorFunctor M).obj X ⟶ Y) :
    X ⟶ (tensorHomFunctor M).obj Y
def

tensorUncurryHom

L121 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorUncurryHom
Documentation

The actual inverse arrow of the tensor-Hom correspondence.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · statement
def tensorUncurryHom {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    {X Y : ModuleCat.{max u v} R} (f : X ⟶ (tensorHomFunctor M).obj Y) :
    (tensorFunctor M).obj X ⟶ Y
theorem

tensorUncurryHom_curry

L127 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorUncurryHom_curry
Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · statement
theorem tensorUncurryHom_curry {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    {X Y : ModuleCat.{max u v} R} (f : (tensorFunctor M).obj X ⟶ Y) :
    tensorUncurryHom M (tensorCurryHom M f) = f
theorem

tensorCurryHom_uncurry

L133 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorCurryHom_uncurry
Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · statement
theorem tensorCurryHom_uncurry {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    {X Y : ModuleCat.{max u v} R} (f : X ⟶ (tensorHomFunctor M).obj Y) :
    tensorCurryHom M (tensorUncurryHom M f) = f
theorem

tensorUncurryHom_naturality_left

L140 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorUncurryHom_naturality_left
Documentation

Naturality of the actual inverse arrows, before any Equiv applications are present.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · statement
theorem tensorUncurryHom_naturality_left {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    {X' X Y : ModuleCat.{max u v} R} (f : X' ⟶ X)
    (g : X ⟶ (tensorHomFunctor M).obj Y) :
    tensorUncurryHom M (f ≫ g) = (tensorFunctor M).map f ≫ tensorUncurryHom M g
theorem

tensorCurryHom_naturality_right

L151 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorCurryHom_naturality_right
Documentation

Naturality of the actual forward arrows, with its own two-variable linear owner.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · statement
theorem tensorCurryHom_naturality_right {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    {X Y Y' : ModuleCat.{max u v} R} (f : (tensorFunctor M).obj X ⟶ Y)
    (g : Y ⟶ Y') :
    tensorCurryHom M (f ≫ g) = tensorCurryHom M f ≫ (tensorHomFunctor M).map g
def

tensorHomEquiv

L163 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorHomEquiv
Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · full declaration
def tensorHomEquiv {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    (X Y : ModuleCat.{max u v} R) :
    ((tensorFunctor M).obj X ⟶ Y) ≃ (X ⟶ (tensorHomFunctor M).obj Y) where
  toFun f := tensorCurryHom M f
  invFun f := tensorUncurryHom M f
  left_inv f := tensorUncurryHom_curry M f
  right_inv f := tensorCurryHom_uncurry M f
def

tensorHomAdjunction

L173 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorHomAdjunction
Documentation

The large-source adjunction assembles already proved native arrow computations.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · statement
def tensorHomAdjunction {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M] :
    (tensorFunctor M : ModuleCat.{max u v} R ⥤ ModuleCat.{max u v} R) ⊣
      tensorHomFunctor M
def

tensorUliftComponent

L183 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorUliftComponent
Documentation

The actual comparison on one universe-lifted source object.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · statement
def tensorUliftComponent {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M] (X : ModuleCat.{u} R) :
    (tensorFunctor M).obj ((ModuleCat.uliftFunctor.{v, u} R).obj X) ≅
      (tensorFunctor M).obj X
def

tensorUliftIso

L191 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorUliftIso
Documentation

The small-source tensor functor is obtained from the large one via a proved comparison.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · statement
def tensorUliftIso {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M] :
    ModuleCat.uliftFunctor.{v, u} R ⋙
        (tensorFunctor M : ModuleCat.{max u v} R ⥤ ModuleCat.{max u v} R) ≅
      (tensorFunctor M : ModuleCat.{u} R ⥤ ModuleCat.{max u v} R)
theorem

tensorFunctor_preservesColimits_large

L204 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorFunctor_preservesColimits_large
Documentation

The constructed large-source adjunction preserves colimits of every index size.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · statement
theorem tensorFunctor_preservesColimits_large {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M] :
    PreservesColimitsOfSize.{a, b}
      (tensorFunctor M : ModuleCat.{max u v} R ⥤ ModuleCat.{max u v} R)
theorem

tensorFunctor_preservesFiniteColimits

L211 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorFunctor_preservesFiniteColimits
Documentation

Right exactness is inherited through an actual adjunction and the proved ULift comparison.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · statement
theorem tensorFunctor_preservesFiniteColimits {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M] :
    PreservesFiniteColimits
      (tensorFunctor M : ModuleCat.{u} R ⥤ ModuleCat.{max u v} R)
instance

tensorFunctor_preservesZeroMorphisms

L227 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorFunctor_preservesZeroMorphisms
Documentation

Zero-map preservation is supplied by the constructed preservation of initial objects.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · statement
instance tensorFunctor_preservesZeroMorphisms {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M] :
    (tensorFunctor M : ModuleCat.{u} R ⥤ ModuleCat.{max u v} R).PreservesZeroMorphisms
theorem

tensorFunctor_map_exact

L236 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.tensorFunctor_map_exact
Documentation

The actual tensor functor preserves exactness of a right exact complex.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v w a b c
Lean source · statement
theorem tensorFunctor_map_exact {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    (S : ShortComplex (ModuleCat.{u} R)) (hS : S.Exact) (hg : Epi S.g) :
    (S.map (tensorFunctor M)).Exact
theorem

mono_of_cover

L263 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.mono_of_cover
Documentation

Descent of a monomorphism through an exact covering row. The upper row only needs to be a complex with an epimorphic last map.

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v
variable {C : Type u} [Category.{v} C] [Abelian C]
Lean source · statement
theorem mono_of_cover
    {K L G X Y : C} (f : X ⟶ Y) (p : G ⟶ Y) (i : L ⟶ G)
    (q : L ⟶ X) (k : K ⟶ G) (j : K ⟶ L)
    (hq : Epi q) (hcomm : i ≫ p = q ≫ f)
    (w : k ≫ p = 0) (hk : (ShortComplex.mk k p w).Exact)
    (hji : j ≫ i = k) (hjq : j ≫ q = 0) (hi : Mono i) : Mono f
theorem

mono_middle_of_exact_subquotient

L281 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.mono_middle_of_exact_subquotient
Documentation

In a morphism of complexes, monic left and right vertical maps and a monic lower-left map make the middle vertical map monic when the upper row is exact.

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v
variable {C : Type u} [Category.{v} C] [Abelian C]
Lean source · statement
theorem mono_middle_of_exact_subquotient
    {S T : ShortComplex C} (φ : S ⟶ T) (hS : S.Exact)
    (hleft : Mono T.f) (hvertical : Mono φ.τ₁)
    (hright : Mono φ.τ₃) : Mono φ.τ₂
theorem

map_epi_of_finite_colimits

L310 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.map_epi_of_finite_colimits
Documentation

A functor preserving the actual kernel cokernel cofork sends an epi to an epi.

Source context 9 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v u' v'
variable {C : Type u} [Category.{v} C] [Abelian C]
variable {D : Type u'} [Category.{v'} D] [Abelian D]
variable (F : C ⥤ D) [PreservesFiniteColimits F] [F.PreservesZeroMorphisms]
Lean source · statement
theorem map_epi_of_finite_colimits {X Y : C} (p : X ⟶ Y) (hp : Epi p) :
    Epi (F.map p)
theorem

mono_map_of_pullback

L319 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor.mono_map_of_pullback
Documentation

The actual kernel lift and the exact covering diagram prove descent of a mapped mono.

Source context 9 commands

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

open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.FlatTensor
universe u v u' v'
variable {C : Type u} [Category.{v} C] [Abelian C]
variable {D : Type u'} [Category.{v'} D] [Abelian D]
variable (F : C ⥤ D) [PreservesFiniteColimits F] [F.PreservesZeroMorphisms]
Lean source · statement
theorem mono_map_of_pullback {X Y G : C}
    (f : X ⟶ Y) (p : G ⟶ Y) (s : PullbackCone p f) (hs : IsLimit s)
    (hp : Epi p) (hi : Mono (F.map s.fst)) : Mono (F.map f)

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