Nyll.EtaleFundamentalGroups.GaloisCovers.TensorProductSurjectivityTransport

Module documentation

Transporting tensor-product surjectivity

This file provides a small algebraic bridge used when a geometric pullback describes a tensor product in the order opposite to the desired function- field tensor product. Surjectivity is transported using equivalences of the two factors and of the target; compatibility only has to be checked on pure tensors.

theorem

productMap_surjective_of_surjective_reversed_tensor

L30 ↗

Algebra.TensorProduct.productMap_surjective_of_surjective_reversed_tensor

Documentation

A surjective map out of a reversed tensor product gives surjectivity of the desired product map, provided the factor identifications agree on pure tensors.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace Algebra.TensorProduct
universe u₁ u₂ u₃ u₄ u₅ u₆ u₇ u₈

Lean source · statement

theorem productMap_surjective_of_surjective_reversed_tensor
    {R : Type u₁} {A : Type u₂} {B : Type u₃} {C : Type u₄}
    {R' : Type u₅} {A' : Type u₆} {B' : Type u₇} {C' : Type u₈}
    [CommRing R] [CommRing A] [CommRing B] [CommRing C]
    [CommRing R'] [CommRing A'] [CommRing B'] [CommRing C']
    [Algebra R A] [Algebra R B] [Algebra R C]
    [Algebra R' A'] [Algebra R' B']
    (f : A →ₐ[R] C) (g : B →ₐ[R] C)
    (q : B' ⊗[R'] A' →+* C')
    (eA : A ≃+* A') (eB : B ≃+* B') (eC : C' ≃+* C)
    (hq : Function.Surjective q)
    (hpure : ∀ (a : A) (b : B),
      eC (q (eB b ⊗ₜ[R'] eA a)) = f a * g b) :
    Function.Surjective (productMap f g)

Module documentation

Transporting tensor-product surjectivity

Declarations

productMap_surjective_of_surjective_reversed_tensor