NYLL
Module

NativeTensorCorrespondence.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.NativeTensorCorrespondence
9 declarations indexed from sourceView source ↗

Module documentation

Correspondence with the original native algebras

Each tensor product is constructed with its original algebra instances in a one-tensor scope. The categorical interface is then identified with that native object. The equivalence below has arbitrary native algebra equivalences as its inverse input, and proves both round trips.

Imports5
Imported by3

Declarations

def

nativeTensorObject

L34 ↗
EtaleFundamentalGroups.CategoricalTensor.nativeTensorObject
Documentation

The actual native tensor algebra, retaining both stored base actions.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
variable {R : Type u} [CommRing R]
Lean source · statement
def nativeTensorObject (S B : CommAlgCat.{u} R) : CommAlgCat.{u} S.carrier
abbrev

nativeCoefficientObject

L39 ↗
EtaleFundamentalGroups.CategoricalTensor.nativeCoefficientObject
Documentation

Read one coefficient arrow as the actual commutative algebra it defines. The object stores the ring and that same algebra map exactly once.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
variable {R : Type u} [CommRing R]
Lean source · full declaration
abbrev nativeCoefficientObject (S : Under (CommRingCat.of R)) : CommAlgCat.{u} R where
  carrier := S.right.carrier
  commRing := inferInstance
  algebra := S.hom.hom.toAlgebra
theorem

nativeCoefficientObject_mkUnder

L46 ↗
EtaleFundamentalGroups.CategoricalTensor.nativeCoefficientObject_mkUnder
Documentation

Reconstructing the original algebra from its native algebra map gives the original stored owner. No tensor is formed in this normalization.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
variable {R : Type u} [CommRing R]
Lean source · statement
theorem nativeCoefficientObject_mkUnder (S : CommAlgCat.{u} R) :
    nativeCoefficientObject (CommRingCat.mkUnder (CommRingCat.of R) S.carrier) = S
theorem

tensorFunctor_obj_coefficientObjects

L57 ↗
EtaleFundamentalGroups.CategoricalTensor.tensorFunctor_obj_coefficientObjects
Documentation

The existing tensor functor forms precisely the native tensor of the two algebras owned by its inputs. This checks only those constructors, not any tensor relation, map law, or universal-property proof.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
variable {R : Type u} [CommRing R]
Lean source · statement
theorem tensorFunctor_obj_coefficientObjects (S B : Under (CommRingCat.of R)) :
    (tensorFunctor S).obj B =
      CommRingCat.mkUnder S.right
        (nativeTensorObject (nativeCoefficientObject S) (nativeCoefficientObject B)).carrier
theorem

tensorFunctor_obj_native

L66 ↗
EtaleFundamentalGroups.CategoricalTensor.tensorFunctor_obj_native
Documentation

The categorical tensor constructor reconstructs exactly the original native tensor algebra. Each input normalization was proved before this scope, so no raw tensor dictionary is reconstructed alongside the functor interface.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
variable {R : Type u} [CommRing R]
Lean source · statement
theorem tensorFunctor_obj_native (S B : CommAlgCat.{u} R) :
    (tensorFunctor (CommRingCat.mkUnder (CommRingCat.of R) S.carrier)).obj
        (CommRingCat.mkUnder (CommRingCat.of R) B.carrier) =
      CommRingCat.mkUnder (CommRingCat.of S.carrier) (nativeTensorObject S B).carrier
def

nativeUnderHom

L85 ↗
EtaleFundamentalGroups.CategoricalTensor.nativeUnderHom
Documentation

Read a morphism under the base into the original native algebra actions. Its scalar compatibility is the defining Under square.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
variable {R : Type u} [CommRing R]
Lean source · full declaration
def nativeUnderHom (B D : CommAlgCat.{u} R)
    (f : CommRingCat.mkUnder (CommRingCat.of R) B.carrier ⟶
      CommRingCat.mkUnder (CommRingCat.of R) D.carrier) :
    B.carrier →ₐ[R] D.carrier where
  __ := f.right.hom
  commutes' r := congrArg
    (fun h : CommRingCat.of R ⟶ CommRingCat.of D.carrier ↦ h.hom r) f.w
def

nativeUnderHomEquivAlgHom

L95 ↗
EtaleFundamentalGroups.CategoricalTensor.nativeUnderHomEquivAlgHom
Documentation

Arbitrary native algebra homomorphisms are precisely the corresponding Under morphisms, with both round trips proved using the original actions.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
variable {R : Type u} [CommRing R]
Lean source · full declaration
def nativeUnderHomEquivAlgHom (B D : CommAlgCat.{u} R) :
    (CommRingCat.mkUnder (CommRingCat.of R) B.carrier ⟶
      CommRingCat.mkUnder (CommRingCat.of R) D.carrier) ≃
        (B.carrier →ₐ[R] D.carrier) where
  toFun := nativeUnderHom B D
  invFun f := f.toUnder
  left_inv f := by
    apply Under.UnderMorphism.ext
    rfl
  right_inv f := by
    apply AlgHom.ext
    intro b
    rfl
def

nativeUnderIsoEquivAlgEquiv

L111 ↗
EtaleFundamentalGroups.CategoricalTensor.nativeUnderIsoEquivAlgEquiv
Documentation

Native algebra equivalences and isomorphisms under the base have the same arbitrary data. Neither direction assumes a comparison equation.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
variable {R : Type u} [CommRing R]
Lean source · full declaration
def nativeUnderIsoEquivAlgEquiv (B D : CommAlgCat.{u} R) :
    (CommRingCat.mkUnder (CommRingCat.of R) B.carrier ≅
      CommRingCat.mkUnder (CommRingCat.of R) D.carrier) ≃
        (B.carrier ≃ₐ[R] D.carrier) where
  toFun e :=
    { toRingEquiv := ((Under.forget (CommRingCat.of R)).mapIso e).commRingCatIsoToRingEquiv
      commutes' := (nativeUnderHom B D e.hom).commutes' }
  invFun e := e.toUnder
  left_inv e := by
    apply Iso.ext
    apply Under.UnderMorphism.ext
    rfl
  right_inv e := by
    apply AlgEquiv.ext
    intro b
    rfl
theorem

native_finitePresentation

L130 ↗
EtaleFundamentalGroups.CategoricalTensor.native_finitePresentation
Documentation

Original algebraic finite presentation supplies the native Under model's ring-hom finite presentation.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.CategoricalTensor
variable {R : Type u} [CommRing R]
Lean source · statement
theorem native_finitePresentation (B : CommAlgCat.{u} R)
    [Algebra.FinitePresentation R B.carrier] :
    (CommRingCat.mkUnder (CommRingCat.of R) B.carrier).hom.hom.FinitePresentation

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