Module

CategoricalTensor.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.CategoricalTensor

12 declarations indexed from sourceView source ↗

Module documentation

The native categorical tensor owner and its pushout comparison

The tensor functor is Mathlib's existing CommRingCat.tensorProd. Its native maps and functor laws are retained. Descent is transported across the proved tensorProdIsoPushout, without calling the former raw descent theorem.

Imports5

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.CategoricalDescent
Mathlib.Algebra.Category.CommAlgCat.Basic
Mathlib.Algebra.Category.Ring.FinitePresentation
Mathlib.Algebra.Category.Ring.Under.Basic
Mathlib.RingTheory.TensorProduct.Basic

Imported by2

def

tensorFunctor

L36 ↗

EtaleFundamentalGroups.CategoricalTensor.tensorFunctor

Documentation

The coefficient arrow supplies the unique algebra used by the existing categorical tensor functor.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
open CategoryTheory.CategoricalTensorDescent
variable {R : CommRingCat.{u}}

Lean source · statement

def tensorFunctor (S : Under R) : Under R ⥤ Under S.right

def

tensorFunctorIsoPushout

L42 ↗

EtaleFundamentalGroups.CategoricalTensor.tensorFunctorIsoPushout

Documentation

The existing tensor/pushout comparison, normalized to the coefficient's original arrow.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
open CategoryTheory.CategoricalTensorDescent
variable {R : CommRingCat.{u}}

Lean source · statement

def tensorFunctorIsoPushout (S : Under R) : tensorFunctor S ≅ Under.pushout S.hom

def

comparison

L53 ↗

EtaleFundamentalGroups.CategoricalTensor.comparison

Documentation

The actual tensor model and its categorical pushout are canonically isomorphic over the same coefficient ring.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
open CategoryTheory.CategoricalTensorDescent
variable {R : CommRingCat.{u}}

Lean source · statement

def comparison (S B : Under R) : (tensorFunctor S).obj B ≅ model S B

def

homEquiv

L57 ↗

EtaleFundamentalGroups.CategoricalTensor.homEquiv

Documentation

Transport arbitrary model morphisms through the proved comparison.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
open CategoryTheory.CategoricalTensorDescent
variable {R : CommRingCat.{u}}

Lean source · full declaration

def homEquiv (S B D : Under R) :
    ((tensorFunctor S).obj B ⟶ (tensorFunctor S).obj D) ≃
      (model S B ⟶ model S D) where
  toFun f := (comparison S B).inv ≫ f ≫ (comparison S D).hom
  invFun f := (comparison S B).hom ≫ f ≫ (comparison S D).inv
  left_inv f := by
    simp only [Category.assoc, Iso.hom_inv_id_assoc, Iso.hom_inv_id, Category.comp_id]
  right_inv f := by
    simp only [Category.assoc, Iso.inv_hom_id_assoc, Iso.inv_hom_id, Category.comp_id]

def

extendHom

L69 ↗

EtaleFundamentalGroups.CategoricalTensor.extendHom

Documentation

Coefficient extension is the pushout extension conjugated by the existing native tensor comparison.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
open CategoryTheory.CategoricalTensorDescent
variable {R : CommRingCat.{u}}

Lean source · statement

def extendHom {S T : Under R} (h : S ⟶ T) {B D : Under R}
    (f : (tensorFunctor S).obj B ⟶ (tensorFunctor S).obj D) :
    (tensorFunctor T).obj B ⟶ (tensorFunctor T).obj D

def

tensorLeg

L75 ↗

EtaleFundamentalGroups.CategoricalTensor.tensorLeg

Documentation

The underlying coefficient leg on native tensor objects.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
open CategoryTheory.CategoricalTensorDescent
variable {R : CommRingCat.{u}}

Lean source · statement

def tensorLeg {S T : Under R} (h : S ⟶ T) (B : Under R) :
    ((tensorFunctor S).obj B).right ⟶ ((tensorFunctor T).obj B).right

theorem

extendHom_square

L81 ↗

EtaleFundamentalGroups.CategoricalTensor.extendHom_square

Documentation

The tensor coefficient square is the literal underlying ring square of the native model morphisms and the canonical coefficient leg.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
open CategoryTheory.CategoricalTensorDescent
variable {R : CommRingCat.{u}}

Lean source · statement

theorem extendHom_square {S T : Under R} (h : S ⟶ T) {B D : Under R}
    (f : (tensorFunctor S).obj B ⟶ (tensorFunctor S).obj D) :
    tensorLeg h B ≫ (extendHom h f).right = f.right ≫ tensorLeg h D

theorem

finitelyPresentable

L104 ↗

EtaleFundamentalGroups.CategoricalTensor.finitelyPresentable

Documentation

Algebraic finite presentation supplies categorical finite presentability for the original model, with no additional compactness premise.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
open CategoryTheory.CategoricalTensorDescent
variable {R : CommRingCat.{u}}

Lean source · statement

theorem finitelyPresentable (B : Under R) (hB : B.hom.hom.FinitePresentation) :
    IsFinitelyPresentable.{u} B

theorem

exists_hom_stage_of_isFinitelyPresentable

L109 ↗

EtaleFundamentalGroups.CategoricalTensor.exists_hom_stage_of_isFinitelyPresentable

Documentation

Categorical tensor Hom descent from the original finite presentation.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
open CategoryTheory.CategoricalTensorDescent
variable {R : CommRingCat.{u}}

Lean source · statement

theorem exists_hom_stage_of_isFinitelyPresentable
    {J : Type u} [SmallCategory J] [IsFiltered J]
    (B D : Under R) [IsFinitelyPresentable.{u} B]
    (F : J ⥤ Under R) (c : Cocone F) (hc : IsColimit c)
    (f : (tensorFunctor c.pt).obj B ⟶ (tensorFunctor c.pt).obj D) :
    ∃ (i : J) (fi : (tensorFunctor (F.obj i)).obj B ⟶ (tensorFunctor (F.obj i)).obj D),
      tensorLeg (c.ι.app i) B ≫ f.right = fi.right ≫ tensorLeg (c.ι.app i) D

theorem

exists_iso_stage_of_isFinitelyPresentable

L129 ↗

EtaleFundamentalGroups.CategoricalTensor.exists_iso_stage_of_isFinitelyPresentable

Documentation

Categorical tensor isomorphism descent preserves both coefficient squares of the arbitrary input isomorphism.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
open CategoryTheory.CategoricalTensorDescent
variable {R : CommRingCat.{u}}

Lean source · statement

theorem exists_iso_stage_of_isFinitelyPresentable
    {J : Type u} [SmallCategory J] [IsFiltered J]
    (B D : Under R) [IsFinitelyPresentable.{u} B] [IsFinitelyPresentable.{u} D]
    (F : J ⥤ Under R) (c : Cocone F) (hc : IsColimit c)
    (e : (tensorFunctor c.pt).obj B ≅ (tensorFunctor c.pt).obj D) :
    ∃ (i : J) (ei : (tensorFunctor (F.obj i)).obj B ≅ (tensorFunctor (F.obj i)).obj D),
      tensorLeg (c.ι.app i) B ≫ e.hom.right = ei.hom.right ≫ tensorLeg (c.ι.app i) D ∧
      tensorLeg (c.ι.app i) D ≫ e.inv.right = ei.inv.right ≫ tensorLeg (c.ι.app i) B

theorem

exists_hom_stage

L159 ↗

EtaleFundamentalGroups.CategoricalTensor.exists_hom_stage

Documentation

Categorical tensor Hom descent from the original finite presentation.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
open CategoryTheory.CategoricalTensorDescent
variable {R : CommRingCat.{u}}

Lean source · statement

theorem exists_hom_stage
    {J : Type u} [SmallCategory J] [IsFiltered J]
    (B D : Under R) (hB : B.hom.hom.FinitePresentation)
    (F : J ⥤ Under R) (c : Cocone F) (hc : IsColimit c)
    (f : (tensorFunctor c.pt).obj B ⟶ (tensorFunctor c.pt).obj D) :
    ∃ (i : J) (fi : (tensorFunctor (F.obj i)).obj B ⟶ (tensorFunctor (F.obj i)).obj D),
      tensorLeg (c.ι.app i) B ≫ f.right = fi.right ≫ tensorLeg (c.ι.app i) D

theorem

exists_iso_stage

L171 ↗

EtaleFundamentalGroups.CategoricalTensor.exists_iso_stage

Documentation

Categorical tensor isomorphism descent preserves both coefficient squares of the arbitrary input isomorphism.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
open CategoryTheory.CategoricalTensorDescent
variable {R : CommRingCat.{u}}

Lean source · statement

theorem exists_iso_stage
    {J : Type u} [SmallCategory J] [IsFiltered J]
    (B D : Under R) (hB : B.hom.hom.FinitePresentation) (hD : D.hom.hom.FinitePresentation)
    (F : J ⥤ Under R) (c : Cocone F) (hc : IsColimit c)
    (e : (tensorFunctor c.pt).obj B ≅ (tensorFunctor c.pt).obj D) :
    ∃ (i : J) (ei : (tensorFunctor (F.obj i)).obj B ≅ (tensorFunctor (F.obj i)).obj D),
      tensorLeg (c.ι.app i) B ≫ e.hom.right = ei.hom.right ≫ tensorLeg (c.ι.app i) D ∧
      tensorLeg (c.ι.app i) D ≫ e.inv.right = ei.inv.right ≫ tensorLeg (c.ι.app i) B

Module documentation

The native categorical tensor owner and its pushout comparison

Declarations