Module

NativeTensorDescent.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.NativeTensorDescent

14 declarations indexed from sourceView source ↗

Module documentation

Descent comparisons retaining the original native tensor actions

The native tensor product is compared directly with the categorical pushout. The comparison uses the original algebra instances, never the algebras reconstructed from an Under object. Its coefficient naturality is proved from the two tensor coprojections. This keeps action normalization out of the finite-field descent proofs.

Imports9

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.CategoricalDescent
Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.NativeTensorCorrespondence
Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.NativeTensorPushout
Mathlib.Algebra.Algebra.Equiv
Mathlib.Algebra.Category.CommAlgCat.Basic
Mathlib.Algebra.Category.Ring.Constructions
Mathlib.Algebra.Category.Ring.Under.Basic
Mathlib.CategoryTheory.HomCongr
Mathlib.RingTheory.TensorProduct.Maps

Imported by2

def

modelIso

L43 ↗

EtaleFundamentalGroups.NativeTensorDescent.modelIso

Documentation

The original tensor algebra and the chosen pushout model have the same coefficient arrow. The native algebra actions are retained in this constructor.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.NativeTensorDescent
open CategoryTheory.CategoricalTensorDescent
open EtaleFundamentalGroups.CategoricalTensor
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]

Lean source · statement

def modelIso (B : Type u) [CommRing B] [Algebra R B] :
    CommRingCat.mkUnder (CommRingCat.of S) (S ⊗[R] B) ≅
      model (CommRingCat.mkUnder (CommRingCat.of R) S)
        (CommRingCat.mkUnder (CommRingCat.of R) B)

theorem

nativeIso_inl_hom

L51 ↗

EtaleFundamentalGroups.NativeTensorDescent.nativeIso_inl_hom

Documentation

The model projection of the actual named native comparison.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.NativeTensorDescent
open CategoryTheory.CategoricalTensorDescent
open EtaleFundamentalGroups.CategoricalTensor
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]

Lean source · statement

theorem nativeIso_inl_hom (B : Type u) [CommRing B] [Algebra R B] :
    CommRingCat.ofHom
        (Algebra.TensorProduct.includeRight : B →ₐ[R] S ⊗[R] B).toRingHom ≫
        (nativeTensorPushoutIso R S B).hom =
      pushout.inl (CommRingCat.ofHom (algebraMap R B))
        (CommRingCat.ofHom (algebraMap R S))

theorem

nativeIso_inr_hom

L60 ↗

EtaleFundamentalGroups.NativeTensorDescent.nativeIso_inr_hom

Documentation

The coefficient projection of the same native comparison.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.NativeTensorDescent
open CategoryTheory.CategoricalTensorDescent
open EtaleFundamentalGroups.CategoricalTensor
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]

Lean source · statement

theorem nativeIso_inr_hom (B : Type u) [CommRing B] [Algebra R B] :
    CommRingCat.ofHom (algebraMap S (S ⊗[R] B)) ≫
        (nativeTensorPushoutIso R S B).hom =
      pushout.inr (CommRingCat.ofHom (algebraMap R B))
        (CommRingCat.ofHom (algebraMap R S))

theorem

modelIso_hom_right

L68 ↗

EtaleFundamentalGroups.NativeTensorDescent.modelIso_hom_right

Documentation

Reading the Under comparison keeps the same native ring Iso homomorphism.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.NativeTensorDescent
open CategoryTheory.CategoricalTensorDescent
open EtaleFundamentalGroups.CategoricalTensor
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]

Lean source · statement

theorem modelIso_hom_right (B : Type u) [CommRing B] [Algebra R B] :
    (modelIso R S B).hom.right = (nativeTensorPushoutIso R S B).hom

theorem

modelIso_inv_right

L73 ↗

EtaleFundamentalGroups.NativeTensorDescent.modelIso_inv_right

Documentation

Reading its inverse likewise keeps the existing native ring Iso.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.NativeTensorDescent
open CategoryTheory.CategoricalTensorDescent
open EtaleFundamentalGroups.CategoricalTensor
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]

Lean source · statement

theorem modelIso_inv_right (B : Type u) [CommRing B] [Algebra R B] :
    (modelIso R S B).inv.right = (nativeTensorPushoutIso R S B).inv

def

homEquiv

L79 ↗

EtaleFundamentalGroups.NativeTensorDescent.homEquiv

Documentation

Arbitrary native algebra maps correspond to maps of the actual pushout models. Both directions share the same constructed comparison.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.NativeTensorDescent
open CategoryTheory.CategoricalTensorDescent
open EtaleFundamentalGroups.CategoricalTensor
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]

Lean source · statement

def homEquiv (B D : Type u) [CommRing B] [CommRing D] [Algebra R B] [Algebra R D] :
    ((S ⊗[R] B) →ₐ[S] (S ⊗[R] D)) ≃
      (model (CommRingCat.mkUnder (CommRingCat.of R) S)
          (CommRingCat.mkUnder (CommRingCat.of R) B) ⟶
        model (CommRingCat.mkUnder (CommRingCat.of R) S)
          (CommRingCat.mkUnder (CommRingCat.of R) D))

theorem

homEquiv_right

L91 ↗

EtaleFundamentalGroups.NativeTensorDescent.homEquiv_right

Documentation

The ring map of the Hom correspondence uses precisely the two native comparison maps. This computation is closed before a coefficient square is formed.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.NativeTensorDescent
open CategoryTheory.CategoricalTensorDescent
open EtaleFundamentalGroups.CategoricalTensor
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]

Lean source · statement

theorem homEquiv_right (B D : Type u) [CommRing B] [CommRing D]
    [Algebra R B] [Algebra R D] (f : (S ⊗[R] B) →ₐ[S] (S ⊗[R] D)) :
    (homEquiv R S B D f).right =
      (nativeTensorPushoutIso R S B).inv ≫ CommRingCat.ofHom f.toRingHom ≫
        (nativeTensorPushoutIso R S D).hom

def

isoEquiv

L99 ↗

EtaleFundamentalGroups.NativeTensorDescent.isoEquiv

Documentation

The same comparison transports arbitrary native algebra equivalences.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.NativeTensorDescent
open CategoryTheory.CategoricalTensorDescent
open EtaleFundamentalGroups.CategoricalTensor
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]

Lean source · statement

def isoEquiv (B D : Type u) [CommRing B] [CommRing D] [Algebra R B] [Algebra R D] :
    ((S ⊗[R] B) ≃ₐ[S] (S ⊗[R] D)) ≃
      (model (CommRingCat.mkUnder (CommRingCat.of R) S)
          (CommRingCat.mkUnder (CommRingCat.of R) B) ≅
        model (CommRingCat.mkUnder (CommRingCat.of R) S)
          (CommRingCat.mkUnder (CommRingCat.of R) D))

theorem

isoEquiv_hom

L109 ↗

EtaleFundamentalGroups.NativeTensorDescent.isoEquiv_hom

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.NativeTensorDescent
open CategoryTheory.CategoricalTensorDescent
open EtaleFundamentalGroups.CategoricalTensor
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]

Lean source · statement

theorem isoEquiv_hom (B D : Type u) [CommRing B] [CommRing D]
    [Algebra R B] [Algebra R D] (e : (S ⊗[R] B) ≃ₐ[S] (S ⊗[R] D)) :
    (isoEquiv R S B D e).hom = homEquiv R S B D e.toAlgHom

theorem

isoEquiv_inv

L114 ↗

EtaleFundamentalGroups.NativeTensorDescent.isoEquiv_inv

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.NativeTensorDescent
open CategoryTheory.CategoricalTensorDescent
open EtaleFundamentalGroups.CategoricalTensor
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]

Lean source · statement

theorem isoEquiv_inv (B D : Type u) [CommRing B] [CommRing D]
    [Algebra R B] [Algebra R D] (e : (S ⊗[R] B) ≃ₐ[S] (S ⊗[R] D)) :
    (isoEquiv R S B D e).inv = homEquiv R S D B e.symm.toAlgHom

theorem

nativeIso_leg

L123 ↗

EtaleFundamentalGroups.NativeTensorDescent.nativeIso_leg

Documentation

The direct native comparison commutes with the literal tensor map of a coefficient homomorphism. Only the two coprojection equations are used.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.NativeTensorDescent
open CategoryTheory.CategoricalTensorDescent
open EtaleFundamentalGroups.CategoricalTensor
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
variable {S}

Lean source · statement

theorem nativeIso_leg (T B : Type u) [CommRing T] [CommRing B]
    [Algebra R T] [Algebra R B] (f : S →ₐ[R] T) :
    (nativeTensorPushoutIso R S B).hom ≫
        leg f.toUnder (CommRingCat.mkUnder (CommRingCat.of R) B) =
      CommRingCat.ofHom (Algebra.TensorProduct.map f (AlgHom.id R B)).toRingHom ≫
        (nativeTensorPushoutIso R T B).hom

theorem

modelIso_leg

L182 ↗

EtaleFundamentalGroups.NativeTensorDescent.modelIso_leg

Documentation

The underlying Under model square follows from the established native ring square, without unfolding either pushout universal-property proof.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.NativeTensorDescent
open CategoryTheory.CategoricalTensorDescent
open EtaleFundamentalGroups.CategoricalTensor
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
variable {S}

Lean source · statement

theorem modelIso_leg (T B : Type u) [CommRing T] [CommRing B]
    [Algebra R T] [Algebra R B] (f : S →ₐ[R] T) :
    (modelIso R S B).hom.right ≫
        leg f.toUnder (CommRingCat.mkUnder (CommRingCat.of R) B) =
      CommRingCat.ofHom (Algebra.TensorProduct.map f (AlgHom.id R B)).toRingHom ≫
        (modelIso R T B).hom.right

theorem

square_of_conjugated_square

L191 ↗

EtaleFundamentalGroups.NativeTensorDescent.square_of_conjugated_square

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.NativeTensorDescent
open CategoryTheory.CategoricalTensorDescent
open EtaleFundamentalGroups.CategoricalTensor
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
variable {S}

Lean source · statement

theorem square_of_conjugated_square
    {C : Type u} [Category C]
    {A B A' B' X Y X' Y' : C}
    (a : A ≅ X) (b : B ≅ Y) (a' : A' ≅ X') (b' : B' ≅ Y')
    (l : A ⟶ A') (r : B ⟶ B') (L : X ⟶ X') (M : Y ⟶ Y')
    (f : A ⟶ B) (g : A' ⟶ B')
    (hl : a.hom ≫ L = l ≫ a'.hom) (hr : b.hom ≫ M = r ≫ b'.hom)
    (h : L ≫ (a'.inv ≫ g ≫ b'.hom) = (a.inv ≫ f ≫ b.hom) ≫ M) :
    l ≫ g = f ≫ r

theorem

hom_square

L212 ↗

EtaleFundamentalGroups.NativeTensorDescent.hom_square

Documentation

A coefficient square between categorical models gives the original native algebra-hom square, without reopening reconstructed module actions.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups.NativeTensorDescent
open CategoryTheory.CategoricalTensorDescent
open EtaleFundamentalGroups.CategoricalTensor
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
variable {S}

Lean source · statement

theorem hom_square (T B D : Type u) [CommRing T] [CommRing B] [CommRing D]
    [Algebra R T] [Algebra R B] [Algebra R D]
    (q : S →ₐ[R] T)
    (f : (S ⊗[R] B) →ₐ[S] (S ⊗[R] D))
    (g : (T ⊗[R] B) →ₐ[T] (T ⊗[R] D))
    (h : leg q.toUnder (CommRingCat.mkUnder (CommRingCat.of R) B) ≫
        (homEquiv R T B D g).right =
      (homEquiv R S B D f).right ≫
        leg q.toUnder (CommRingCat.mkUnder (CommRingCat.of R) D)) :
    (Algebra.TensorProduct.map q (AlgHom.id R D)).comp (f.restrictScalars R) =
      (g.restrictScalars R).comp (Algebra.TensorProduct.map q (AlgHom.id R B))

Module documentation

Descent comparisons retaining the original native tensor actions

Declarations