Module

RelativeFiniteFieldTensorDiagram.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.RelativeFiniteFieldTensorDiagram

8 declarations indexed from sourceView source ↗

Module documentation

Relative finite constant-extension tensor diagrams

Fix an actual finite intermediate field F₀. The upper interval of finite fields containing F₀ is Under F₀, since the original index is a preorder. Each stage is the literal tensor ring R ⊗[k] E, read under R ⊗[k] F₀ through the tensor map of the actual field inclusion. Finality of the upper interval preserves the existing tensor colimit; no coefficient lifting or injectivity argument is repeated.

Imports7

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.FiniteFieldTensorDiagram
Mathlib.CategoryTheory.Comma.Over.Basic
Mathlib.CategoryTheory.Filtered.Connected
Mathlib.CategoryTheory.Filtered.Final
Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Mathlib.CategoryTheory.Limits.Final
Mathlib.RingTheory.TensorProduct.Maps

Imported by2

def

finiteIntermediateFieldTensorRingDiagram

L38 ↗

EtaleFundamentalGroups.finiteIntermediateFieldTensorRingDiagram

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
variable (k L R : Type u) [Field k] [Field L] [CommRing R]
variable [Algebra k L] [Algebra k R]

Lean source · statement

def finiteIntermediateFieldTensorRingDiagram :
    FiniteIntermediateFieldIndex k L ⥤ CommRingCat.{u}

def

finiteIntermediateFieldTensorRingCocone

L42 ↗

EtaleFundamentalGroups.finiteIntermediateFieldTensorRingCocone

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
variable (k L R : Type u) [Field k] [Field L] [CommRing R]
variable [Algebra k L] [Algebra k R]

Lean source · statement

def finiteIntermediateFieldTensorRingCocone :
    Cocone (finiteIntermediateFieldTensorRingDiagram k L R)

def

relativeFiniteIntermediateFieldTensorDiagram

L49 ↗

EtaleFundamentalGroups.relativeFiniteIntermediateFieldTensorDiagram

Documentation

The actual finite constant extensions containing the fixed field F₀, read as a diagram of algebras under its tensor 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
variable (k L R : Type u) [Field k] [Field L] [CommRing R]
variable [Algebra k L] [Algebra k R]

Lean source · statement

def relativeFiniteIntermediateFieldTensorDiagram (F₀ : FiniteIntermediateFieldIndex k L) :
    Under F₀ ⥤ Under (CommRingCat.of (R ⊗[k] F₀.val.toSubalgebra))

def

relativeFiniteIntermediateFieldTensorCocone

L55 ↗

EtaleFundamentalGroups.relativeFiniteIntermediateFieldTensorCocone

Documentation

The literal inclusions of all larger finite constant extensions into R ⊗[k] L, with the fixed F₀-tensor ring as their base.

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
variable (k L R : Type u) [Field k] [Field L] [CommRing R]
variable [Algebra k L] [Algebra k R]

Lean source · statement

def relativeFiniteIntermediateFieldTensorCocone (F₀ : FiniteIntermediateFieldIndex k L) :
    Cocone (relativeFiniteIntermediateFieldTensorDiagram k L R F₀)

def

relativeFiniteIntermediateFieldTensorCoconeIsColimit

L61 ↗

EtaleFundamentalGroups.relativeFiniteIntermediateFieldTensorCoconeIsColimit

Documentation

The relative constant-extension cocone is colimiting, by restricting the existing finite-field tensor colimit to the final upper interval.

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
variable (k L R : Type u) [Field k] [Field L] [CommRing R]
variable [Algebra k L] [Algebra k R]

Lean source · statement

def relativeFiniteIntermediateFieldTensorCoconeIsColimit [Algebra.IsAlgebraic k L]
    (F₀ : FiniteIntermediateFieldIndex k L) :
    IsColimit (relativeFiniteIntermediateFieldTensorCocone k L R F₀)

theorem

relativeFiniteIntermediateFieldTensorDiagram_obj_hom

L71 ↗

EtaleFundamentalGroups.relativeFiniteIntermediateFieldTensorDiagram_obj_hom

Documentation

The relative stage algebra map is the literal tensor map of F₀ ≤ E.

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
variable (k L R : Type u) [Field k] [Field L] [CommRing R]
variable [Algebra k L] [Algebra k R]

Lean source · full declaration

theorem relativeFiniteIntermediateFieldTensorDiagram_obj_hom
    (F₀ : FiniteIntermediateFieldIndex k L) (E : Under F₀) :
    ((relativeFiniteIntermediateFieldTensorDiagram k L R F₀).obj E).hom.hom =
      (Algebra.TensorProduct.map (AlgHom.id R R)
        (Subalgebra.inclusion
          (show F₀.val.toSubalgebra ≤ E.right.val.toSubalgebra from E.hom.le))).toRingHom := by
  rfl

theorem

relativeFiniteIntermediateFieldTensorCocone_pt_hom

L80 ↗

EtaleFundamentalGroups.relativeFiniteIntermediateFieldTensorCocone_pt_hom

Documentation

The relative colimit point carries the literal tensor inclusion of F₀ into L.

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
variable (k L R : Type u) [Field k] [Field L] [CommRing R]
variable [Algebra k L] [Algebra k R]

Lean source · statement

theorem relativeFiniteIntermediateFieldTensorCocone_pt_hom
    (F₀ : FiniteIntermediateFieldIndex k L) :
    (relativeFiniteIntermediateFieldTensorCocone k L R F₀).pt.hom.hom =
      (Algebra.TensorProduct.map (AlgHom.id R R) F₀.val.toSubalgebra.val).toRingHom

theorem

relativeFiniteIntermediateFieldTensorCocone_leg_hom

L87 ↗

EtaleFundamentalGroups.relativeFiniteIntermediateFieldTensorCocone_leg_hom

Documentation

The relative cocone leg is the literal tensor inclusion of the stage field into L.

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
variable (k L R : Type u) [Field k] [Field L] [CommRing R]
variable [Algebra k L] [Algebra k R]

Lean source · statement

theorem relativeFiniteIntermediateFieldTensorCocone_leg_hom
    (F₀ : FiniteIntermediateFieldIndex k L) (E : Under F₀) :
    ((relativeFiniteIntermediateFieldTensorCocone k L R F₀).ι.app E).right.hom =
      (Algebra.TensorProduct.map (AlgHom.id R R) E.right.val.toSubalgebra.val).toRingHom

Module documentation

Relative finite constant-extension tensor diagrams

Declarations