NYLL
Module

FiniteFieldDescent.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.FiniteFieldDescent
2 declarations indexed from sourceView source ↗

Module documentation

Map descent to an actual finite constant extension

Native tensor algebras are compared directly with their categorical pushouts. The original algebra actions are retained throughout, and the literal field inclusion squares follow from the native pushout comparison's naturality.

Imports11
Imported by1

Declarations

theorem

exists_finiteIntermediateField_tensorProduct_algHom

L39 ↗
EtaleFundamentalGroups.exists_finiteIntermediateField_tensorProduct_algHom
Documentation

Native Hom descent preserves the literal coefficient square.

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
open CategoryTheory.CategoricalTensorDescent
Lean source · statement
theorem exists_finiteIntermediateField_tensorProduct_algHom
    (k L R B D : Type u) [Field k] [Field L]
    [CommRing R] [CommRing B] [CommRing D]
    [Algebra k L] [Algebra k R] [Algebra.IsAlgebraic k L]
    [Algebra R B] [Algebra R D]
    [Algebra.FinitePresentation R B]
    (e : ((R ⊗[k] L) ⊗[R] B) →ₐ[R ⊗[k] L] ((R ⊗[k] L) ⊗[R] D)) :
    ∃ F : IntermediateField k L, FiniteDimensional k F ∧
      ∃ eF : ((R ⊗[k] F.toSubalgebra) ⊗[R] B) →ₐ[R ⊗[k] F.toSubalgebra]
        ((R ⊗[k] F.toSubalgebra) ⊗[R] D),
        (Algebra.TensorProduct.map
            (Algebra.TensorProduct.map (R := k) (S := R) (AlgHom.id R R) F.val)
            (AlgHom.id R D)).comp (eF.restrictScalars R) =
          (e.restrictScalars R).comp
            (Algebra.TensorProduct.map
              (Algebra.TensorProduct.map (R := k) (S := R) (AlgHom.id R R) F.val)
              (AlgHom.id R B))
theorem

exists_finiteIntermediateField_tensorProduct_algEquiv

L81 ↗
EtaleFundamentalGroups.exists_finiteIntermediateField_tensorProduct_algEquiv
Documentation

Native isomorphism descent preserves both literal coefficient squares.

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
open CategoryTheory.CategoricalTensorDescent
Lean source · statement
theorem exists_finiteIntermediateField_tensorProduct_algEquiv
    (k L R B D : Type u) [Field k] [Field L]
    [CommRing R] [CommRing B] [CommRing D]
    [Algebra k L] [Algebra k R] [Algebra.IsAlgebraic k L]
    [Algebra R B] [Algebra R D]
    [Algebra.FinitePresentation R B] [Algebra.FinitePresentation R D]
    (e : ((R ⊗[k] L) ⊗[R] B) ≃ₐ[R ⊗[k] L] ((R ⊗[k] L) ⊗[R] D)) :
    ∃ F : IntermediateField k L, FiniteDimensional k F ∧
      ∃ eF : ((R ⊗[k] F.toSubalgebra) ⊗[R] B) ≃ₐ[R ⊗[k] F.toSubalgebra]
        ((R ⊗[k] F.toSubalgebra) ⊗[R] D),
        (Algebra.TensorProduct.map
            (Algebra.TensorProduct.map (R := k) (S := R) (AlgHom.id R R) F.val)
            (AlgHom.id R D)).comp (eF.toAlgHom.restrictScalars R) =
          (e.toAlgHom.restrictScalars R).comp
            (Algebra.TensorProduct.map
              (Algebra.TensorProduct.map (R := k) (S := R) (AlgHom.id R R) F.val)
              (AlgHom.id R B)) ∧
        (Algebra.TensorProduct.map
            (Algebra.TensorProduct.map (R := k) (S := R) (AlgHom.id R R) F.val)
            (AlgHom.id R B)).comp (eF.symm.toAlgHom.restrictScalars R) =
          (e.symm.toAlgHom.restrictScalars R).comp
            (Algebra.TensorProduct.map
              (Algebra.TensorProduct.map (R := k) (S := R) (AlgHom.id R R) F.val)
              (AlgHom.id R D))

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