Nyll.EtaleFundamentalGroups.FiniteEtale.LocalKernelBaseChange

Module documentation

Local H⁰ base change from surjectivity on the closed fibre

For a map between finite free modules over a local ring, surjectivity of the kernel comparison on the residue field forces both its kernel and cokernel to split. In particular, its kernel is finite projective and commutes with arbitrary scalar extension.

theorem

finite_projective_ker_and_bijective_baseChange_of_residue_surjective

L29 ↗

TwoChartCech.finite_projective_ker_and_bijective_baseChange_of_residue_surjective

Documentation

Closed-fibre surjectivity for a finite free two-term complex gives a finite projective kernel and arbitrary kernel base change.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace TwoChartCech
universe u

Lean source · statement

theorem finite_projective_ker_and_bijective_baseChange_of_residue_surjective
    {R M N : Type u} [CommRing R] [IsLocalRing R]
    [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M]
    [AddCommGroup N] [Module R N] [Module.Finite R N] [Module.Free R N]
    (d : M →ₗ[R] N)
    (hsurj : Function.Surjective (kerBaseChangeHom d (IsLocalRing.ResidueField R))) :
    Module.Finite R (LinearMap.ker d) ∧ Module.Projective R (LinearMap.ker d) ∧
      ∀ (A : Type u) [CommRing A] [Algebra R A],
        Function.Bijective (kerBaseChangeHom d A)

Module documentation

Local H⁰ base change from surjectivity on the closed fibre

Declarations

finite_projective_ker_and_bijective_baseChange_of_residue_surjective