Module

ProjectiveCokernelBaseChange.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.ProjectiveCokernelBaseChange

2 declarations indexed from sourceView source ↗

Module documentation

Kernel base change for a map with projective cokernel

Splitting the cokernel makes the image a projective direct summand. Splitting the surjection onto this image makes the kernel a finite projective direct summand and proves its canonical arbitrary base change.

Imports3

Nyll.SchemeTheory.Cohomology.Cech.TwoChartCech
Mathlib.Algebra.Module.Projective
Mathlib.RingTheory.Finiteness.Basic

Imported by2

theorem

exists_subtype_retraction_of_projective_quotient

L27 ↗

TwoChartCech.exists_subtype_retraction_of_projective_quotient

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 exists_subtype_retraction_of_projective_quotient
    {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M]
    (K : Submodule R M) [Module.Projective R (M ⧸ K)] :
    ∃ r : M →ₗ[R] K, r ∘ₗ K.subtype = LinearMap.id

theorem

finite_projective_ker_and_bijective_baseChange_of_projective_coker

L45 ↗

TwoChartCech.finite_projective_ker_and_bijective_baseChange_of_projective_coker

Documentation

Projectivity of the actual cokernel supplies finite projectivity of the kernel and bijectivity of its canonical base-change map over every algebra.