TwoChartCech.finite_ker_baseChange_of_finite_ker_of_finite_coker
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.finite_ker_baseChange_of_finite_ker_of_finite_coker
universe u
open scoped TensorProductLean source · statement
theorem _root_.TwoChartCech.finite_ker_baseChange_of_finite_ker_of_finite_coker
{R : Type u} [CommRing R] [IsNoetherianRing R]
{C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
[Module.Flat R C1] (d : C0 →ₗ[R] C1)
[Module.Finite R (LinearMap.ker d)] [Module.Finite R (C1 ⧸ LinearMap.range d)]
(A : Type u) [CommRing A] [Algebra R A] [IsNoetherianRing A] :
Module.Finite A (LinearMap.ker (d.baseChange A))