Module.isClosed_setOf_le_finrank_cohomology_baseChange_residueField_of_projective
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.CohomologyFinrankClosed
attribute [-simp] CoherentBaseChange.FibreH0Family.mk.sizeOf_spec
CoherentBaseChange.FibreH0Family.mk.injEq
universe u
open TensorProduct
open CategoryTheory AlgebraicGeometryLean source · statement
theorem _root_.Module.isClosed_setOf_le_finrank_cohomology_baseChange_residueField_of_projective
{R : Type u} [CommRing R] [IsNoetherianRing R]
(K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module R (K i)]
[∀ i, Module.Finite R (K i)] [∀ i, Module.Projective R (K i)]
(δ : ∀ i, K i →ₗ[R] K (i + 1)) (hδδ : ∀ i, δ (i + 1) ∘ₗ δ i = 0) (r : ℕ) :
IsClosed {q : PrimeSpectrum R | r ≤ Module.finrank q.asIdeal.ResidueField
↥(LinearMap.ker ((δ 0).baseChange q.asIdeal.ResidueField))} ∧
∀ i : ℕ, IsClosed {q : PrimeSpectrum R |
r + Module.finrank q.asIdeal.ResidueField
↥((LinearMap.range ((δ i).baseChange q.asIdeal.ResidueField)).comap
(LinearMap.ker ((δ (i + 1)).baseChange q.asIdeal.ResidueField)).subtype) ≤
Module.finrank q.asIdeal.ResidueField
↥(LinearMap.ker ((δ (i + 1)).baseChange q.asIdeal.ResidueField))}