Nyll.EtaleFundamentalGroups.Kummer.Normalization.EtaleBaseChangeProductSurjectivity

Module documentation

From generic composita to integral etale base changes

A selected generic tensor component is already generated by the two function fields. For an etale map of domains, its image is also generated by the smaller etale algebra and the old function field: that image is a finite-dimensional domain over the old field, hence a field and therefore contains the whole new fraction field.

theorem

etaleBaseChangeProductMap_surjective_of_fractionFieldProductMap_surjective

L29 ↗

EtaleFundamentalGroups.etaleBaseChangeProductMap_surjective_of_fractionFieldProductMap_surjective

Documentation

Surjectivity of the product map on fraction fields descends to the product map formed with the original etale algebra.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem etaleBaseChangeProductMap_surjective_of_fractionFieldProductMap_surjective
    {A C F KC L M : Type u}
    [CommRing A] [IsDomain A]
    [CommRing C] [IsDomain C] [Algebra A C] [Algebra.Etale A C]
    [Field F] [Algebra A F] [IsFractionRing A F]
    [Field KC] [Algebra C KC] [IsFractionRing C KC]
    [Algebra A KC] [IsScalarTower A C KC]
    [Algebra F KC] [IsScalarTower A F KC]
    [Field L] [Algebra F L] [Algebra A L] [IsScalarTower A F L]
    [Field M] [Algebra KC M] [Algebra C M]
    [Algebra L M] [Algebra F M] [Algebra A M]
    [IsScalarTower C KC M] [IsScalarTower F KC M]
    [IsScalarTower F L M] [IsScalarTower A C M]
    [IsScalarTower A L M]
    (hgeneric : Function.Surjective
      (Algebra.TensorProduct.productMap
        (IsScalarTower.toAlgHom F KC M)
        (IsScalarTower.toAlgHom F L M))) :
    Function.Surjective
      (etaleBaseChangeProductMap (A := A) (C := C) (L := L) (M := M))

Module documentation

From generic composita to integral etale base changes

Declarations

etaleBaseChangeProductMap_surjective_of_fractionFieldProductMap_surjective