Module

CoconeLeg.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.CoconeLeg

8 declarations indexed from sourceView source ↗

Module documentation

Literal tensor-product legs of algebra cocones

The categorical base-change functor stores its objects with the algebra structure induced by an object of Under. Downstream algebra calculations use the canonical tensor-product algebra structure instead. This file is the single boundary between those two presentations: it exposes literal canonical algebra homomorphisms, proves that their Under morphisms are the mapped cocone legs, and records naturality and the tensor-symmetry square.

Imports3

Mathlib.Algebra.Category.Ring.Under.Basic
Mathlib.CategoryTheory.Limits.Cones
Mathlib.RingTheory.TensorProduct.Maps

Imported by8

instance

underCommRingCatAlgebra

L33 ↗

EtaleFundamentalGroups.underCommRingCatAlgebra

Documentation

The algebra structure carried by an object under CommRingCat.of R, spelled with the underlying type R.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u

Lean source · statement

instance underCommRingCatAlgebra
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A

def

filteredTensorToColimitAlgHom

L39 ↗

EtaleFundamentalGroups.filteredTensorToColimitAlgHom

Documentation

The literal tensor-product map induced by a leg of a cocone of R-algebras, with the stage algebra in the left tensor coordinate.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
/-- The algebra structure carried by an object under `CommRingCat.of R`,
spelled with the underlying type `R`. -/
local instance underCommRingCatAlgebra
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A :=
  RingHom.toAlgebra A.hom.hom

Lean source · statement

def filteredTensorToColimitAlgHom
    {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    {J : Type u} [SmallCategory J]
    {F : J ⥤ Under (CommRingCat.of R)} (c : Cocone F) (i : J) :
    (F.obj i ⊗[R] A) →ₐ[R] (c.pt ⊗[R] A)

theorem

filteredTensorToColimitAlgHom_tmul

L48 ↗

EtaleFundamentalGroups.filteredTensorToColimitAlgHom_tmul

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
/-- The algebra structure carried by an object under `CommRingCat.of R`,
spelled with the underlying type `R`. -/
local instance underCommRingCatAlgebra
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A :=
  RingHom.toAlgebra A.hom.hom

Lean source · statement

theorem filteredTensorToColimitAlgHom_tmul
    {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    {J : Type u} [SmallCategory J]
    {F : J ⥤ Under (CommRingCat.of R)} (c : Cocone F) (i : J)
    (x : F.obj i) (a : A) :
    filteredTensorToColimitAlgHom c i (x ⊗ₜ[R] a) =
      CommRingCat.toAlgHom (c.ι.app i) x ⊗ₜ[R] a

def

filteredBaseChangeCoconeLegAlgHom

L59 ↗

EtaleFundamentalGroups.filteredBaseChangeCoconeLegAlgHom

Documentation

The same cocone leg in the orientation used by categorical base change: the fixed algebra is the left tensor coordinate and hence the scalar ring.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
/-- The algebra structure carried by an object under `CommRingCat.of R`,
spelled with the underlying type `R`. -/
local instance underCommRingCatAlgebra
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A :=
  RingHom.toAlgebra A.hom.hom

Lean source · statement

def filteredBaseChangeCoconeLegAlgHom
    {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    {J : Type u} [SmallCategory J]
    {F : J ⥤ Under (CommRingCat.of R)} (c : Cocone F) (i : J) :
    (A ⊗[R] F.obj i) →ₐ[A] (A ⊗[R] c.pt)

theorem

filteredBaseChangeCoconeLegAlgHom_tmul

L68 ↗

EtaleFundamentalGroups.filteredBaseChangeCoconeLegAlgHom_tmul

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
/-- The algebra structure carried by an object under `CommRingCat.of R`,
spelled with the underlying type `R`. -/
local instance underCommRingCatAlgebra
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A :=
  RingHom.toAlgebra A.hom.hom

Lean source · statement

theorem filteredBaseChangeCoconeLegAlgHom_tmul
    {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    {J : Type u} [SmallCategory J]
    {F : J ⥤ Under (CommRingCat.of R)} (c : Cocone F) (i : J)
    (a : A) (x : F.obj i) :
    filteredBaseChangeCoconeLegAlgHom c i (a ⊗ₜ[R] x) =
      a ⊗ₜ[R] CommRingCat.toAlgHom (c.ι.app i) x

theorem

filteredBaseChangeCoconeLegAlgHom_toUnder

L79 ↗

EtaleFundamentalGroups.filteredBaseChangeCoconeLegAlgHom_toUnder

Documentation

The literal base-change leg is exactly the leg of the categorically mapped cocone after forgetting back to Under.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
/-- The algebra structure carried by an object under `CommRingCat.of R`,
spelled with the underlying type `R`. -/
local instance underCommRingCatAlgebra
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A :=
  RingHom.toAlgebra A.hom.hom

Lean source · statement

theorem filteredBaseChangeCoconeLegAlgHom_toUnder
    {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    {J : Type u} [SmallCategory J]
    {F : J ⥤ Under (CommRingCat.of R)} (c : Cocone F) (i : J) :
    (filteredBaseChangeCoconeLegAlgHom c i).toUnder =
      ((CommRingCat.tensorProd (CommRingCat.of R) (CommRingCat.of A)).mapCocone c).ι.app i

theorem

filteredBaseChangeCoconeLegAlgHom_naturality

L88 ↗

EtaleFundamentalGroups.filteredBaseChangeCoconeLegAlgHom_naturality

Documentation

Naturality of the literal base-change cocone legs.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
/-- The algebra structure carried by an object under `CommRingCat.of R`,
spelled with the underlying type `R`. -/
local instance underCommRingCatAlgebra
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A :=
  RingHom.toAlgebra A.hom.hom

Lean source · statement

theorem filteredBaseChangeCoconeLegAlgHom_naturality
    {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    {J : Type u} [SmallCategory J]
    {F : J ⥤ Under (CommRingCat.of R)} (c : Cocone F)
    {i j : J} (f : i ⟶ j) :
    (filteredBaseChangeCoconeLegAlgHom c j).comp
        (Algebra.TensorProduct.map (AlgHom.id A A)
          (CommRingCat.toAlgHom (F.map f))) =
      filteredBaseChangeCoconeLegAlgHom c i

theorem

filteredBaseChangeCoconeLegAlgHom_comm

L107 ↗

EtaleFundamentalGroups.filteredBaseChangeCoconeLegAlgHom_comm

Documentation

Swapping tensor factors intertwines the two literal versions of a cocone leg.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
/-- The algebra structure carried by an object under `CommRingCat.of R`,
spelled with the underlying type `R`. -/
local instance underCommRingCatAlgebra
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A :=
  RingHom.toAlgebra A.hom.hom

Lean source · statement

theorem filteredBaseChangeCoconeLegAlgHom_comm
    {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    {J : Type u} [SmallCategory J]
    {F : J ⥤ Under (CommRingCat.of R)} (c : Cocone F) (i : J)
    (z : F.obj i ⊗[R] A) :
    filteredBaseChangeCoconeLegAlgHom c i
        ((Algebra.TensorProduct.comm R (F.obj i) A) z) =
      (Algebra.TensorProduct.comm R c.pt A)
        (filteredTensorToColimitAlgHom c i z)

Module documentation

Literal tensor-product legs of algebra cocones

Declarations