TwoChartCech.isClosed_setOf_le_finrank_ker_baseChange
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_isClosed_setOf_le_finrank_ker_baseChange
universe u
open CategoryTheory AlgebraicGeometry TensorProductLean source · full declaration
theorem _root_.TwoChartCech.isClosed_setOf_le_finrank_ker_baseChange
{R : Type u} [CommRing R] [IsNoetherianRing R]
{C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
[Module.Flat R C0] [Module.Flat R C1] (d : C0 →ₗ[R] C1)
[Module.Finite R (LinearMap.ker d)] [Module.Finite R (C1 ⧸ LinearMap.range d)]
{T : Scheme.{u}} (f : T ⟶ Spec (.of R)) (n : ℕ) :
IsClosed {x : T | n ≤ Module.finrank (show PrimeSpectrum R from f.base x).asIdeal.ResidueField
(LinearMap.ker (d.baseChange (show PrimeSpectrum R from f.base x).asIdeal.ResidueField))} :=
by
obtain ⟨F, hF⟩ := TwoChartCech.exists_fibreH0Family d f
have : {x : T | n ≤ Module.finrank (show PrimeSpectrum R from f.base x).asIdeal.ResidueField
(LinearMap.ker (d.baseChange (show PrimeSpectrum R from f.base x).asIdeal.ResidueField))} =
{x : T | n ≤ F.h0 x} := by
ext x; simp only [Set.mem_ofPred_eq, hF x]
rw [this]
exact F.isClosed_setOf_le_h0 n