Module

NativeTensorPushout.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.NativeTensorPushout

3 declarations indexed from sourceView source ↗

Module documentation

Native ring models for tensor-product pushouts

Imports4

Mathlib.Algebra.Category.Ring.Colimits
Mathlib.Algebra.Category.Ring.Constructions
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Mathlib.RingTheory.TensorProduct.Basic

Imported by2

def

nativeModelInclusion

L38 ↗

EtaleFundamentalGroups.CategoricalTensor.nativeModelInclusion

Documentation

The literal model coprojection, retained as a RingHom before entering the Under categories. Only this construction exposes its R-AlgHom owner.

Source context 6 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
variable (R S B : Type u) [CommRing R] [CommRing S] [CommRing B]
    [Algebra R S] [Algebra R B]

Lean source · statement

def nativeModelInclusion : B →+* S ⊗[R] B

def

nativeTensorPushoutIso

L43 ↗

EtaleFundamentalGroups.CategoricalTensor.nativeTensorPushoutIso

Documentation

The concrete tensor/pushout Iso in CommRingCat, with the model leg first. Its public interface has no coefficient-algebra structure on the tensor.

Source context 6 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
variable (R S B : Type u) [CommRing R] [CommRing S] [CommRing B]
    [Algebra R S] [Algebra R B]

Lean source · statement

def nativeTensorPushoutIso : CommRingCat.of (S ⊗[R] B) ≅
    pushout (CommRingCat.ofHom (algebraMap R B))
      (CommRingCat.ofHom (algebraMap R S))

lemma

nativeModelInclusion_eq_pushout_inl

L50 ↗

EtaleFundamentalGroups.CategoricalTensor.nativeModelInclusion_eq_pushout_inl

Documentation

The native Iso carries the categorical model coprojection to the literal right tensor inclusion. This is the actual tensor pushout universal property.

Source context 6 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
variable (R S B : Type u) [CommRing R] [CommRing S] [CommRing B]
    [Algebra R S] [Algebra R B]

Lean source · statement

lemma nativeModelInclusion_eq_pushout_inl :
    CommRingCat.ofHom (nativeModelInclusion R S B) =
      pushout.inl (CommRingCat.ofHom (algebraMap R B))
        (CommRingCat.ofHom (algebraMap R S)) ≫
          (nativeTensorPushoutIso R S B).inv

Module documentation

Native ring models for tensor-product pushouts

Declarations

nativeModelInclusion

nativeTensorPushoutIso

nativeModelInclusion_eq_pushout_inl