Module

CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0.lean

Nyll.AlgebraicCurves.Cohomology.Cech.CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0

20 declarations indexed from sourceView source ↗

Module documentation

Closedness of fibre zeroth-cohomology dimension bounds, using matrix minors on affine charts.

Imports12

Nyll.AlgebraicCurves.Cohomology.Sheaves.CoherentBaseChangeFamily
Mathlib.LinearAlgebra.Dimension.Constructions
Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Mathlib.LinearAlgebra.Matrix.Rank
Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Mathlib.RingTheory.Finiteness.Prod
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.RingTheory.TensorProduct.Finite
Mathlib.RingTheory.TensorProduct.Free
Mathlib.Data.Fintype.EquivFin

Imported by2

theorem

exists_det_submatrix_ne_zero_of_le_rank

L51 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0.CBCSol.exists_det_submatrix_ne_zero_of_le_rank

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CBCSol
section CoreLemma
variable {K : Type*} [Field K] {m n : Type*} [Finite m] [Fintype n]

Lean source · statement

theorem exists_det_submatrix_ne_zero_of_le_rank
    (M : Matrix m n K) (r : ℕ) (hrk : r + 1 ≤ M.rank) :
    ∃ (s : Fin (r + 1) → m) (t : Fin (r + 1) → n), (M.submatrix s t).det ≠ 0

theorem

rank_le_of_det_submatrix_eq_zero

L101 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0.CBCSol.rank_le_of_det_submatrix_eq_zero

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CBCSol
section CoreLemma
variable {K : Type*} [Field K] {m n : Type*} [Finite m] [Fintype n]

Lean source · statement

theorem rank_le_of_det_submatrix_eq_zero
    (M : Matrix m n K) (r : ℕ)
    (hminors : ∀ (s : Fin (r + 1) → m) (t : Fin (r + 1) → n), (M.submatrix s t).det = 0) :
    M.rank ≤ r

abbrev

κ

L112 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0.CBCSol.κ

Documentation

The residue field at the prime used to form the fibre cohomology.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CBCSol

Lean source · statement

abbrev κ {R : Type u} [CommRing R] (𝔭 : PrimeSpectrum R) : Type u

def

fibreRank

L127 ↗

CoherentBaseChange.TwoTermComplex.fibreRank

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)

Lean source · statement

def _root_.CoherentBaseChange.TwoTermComplex.fibreRank (𝔭 : PrimeSpectrum R) : ℕ

theorem

fibreH0_add_fibreRank

L131 ↗

CoherentBaseChange.TwoTermComplex.fibreH0_add_fibreRank

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex

Lean source · statement

theorem _root_.CoherentBaseChange.TwoTermComplex.fibreH0_add_fibreRank (𝔭 : PrimeSpectrum
    R) :
    G.fibreH0 𝔭 + G.fibreRank 𝔭 = Module.finrank (κ 𝔭) (κ 𝔭 ⊗[R] G.C0)

theorem

setOf_le_fibreH0_eq

L141 ↗

CoherentBaseChange.TwoTermComplex.setOf_le_fibreH0_eq

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex

Lean source · statement

theorem _root_.CoherentBaseChange.TwoTermComplex.setOf_le_fibreH0_eq [StrongRankCondition
    R] (n : ℕ) :
    {𝔭 : PrimeSpectrum R | n ≤ G.fibreH0 𝔭}
      = {𝔭 | G.fibreRank 𝔭 + n ≤ Module.finrank R G.C0}

theorem

isClosed_add_le_const

L153 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0.CoherentBaseChange.TwoTermComplex.isClosed_add_le_const

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex

Lean source · statement

theorem isClosed_add_le_const {X : Type*} [TopologicalSpace X] {f : X → ℕ}
    (hf : ∀ r, IsClosed {x | f x ≤ r}) (n c : ℕ) :
    IsClosed {x | f x + n ≤ c}

abbrev

b0

L164 ↗

CoherentBaseChange.TwoTermComplex.b0

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex

Lean source · statement

abbrev _root_.CoherentBaseChange.TwoTermComplex.b0 : Module.Basis
    (Module.Free.ChooseBasisIndex R G.C0) R G.C0

abbrev

b1

L170 ↗

CoherentBaseChange.TwoTermComplex.b1

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex

Lean source · statement

abbrev _root_.CoherentBaseChange.TwoTermComplex.b1 : Module.Basis
    (Module.Free.ChooseBasisIndex R G.C1) R G.C1

def

Md

L176 ↗

CoherentBaseChange.TwoTermComplex.Md

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex

Lean source · statement

def _root_.CoherentBaseChange.TwoTermComplex.Md : Matrix (Module.Free.ChooseBasisIndex R
    G.C1) (Module.Free.ChooseBasisIndex R G.C0) R

theorem

fibreRank_eq_rank_map

L182 ↗

CoherentBaseChange.TwoTermComplex.fibreRank_eq_rank_map

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex

Lean source · statement

theorem _root_.CoherentBaseChange.TwoTermComplex.fibreRank_eq_rank_map (𝔭 : PrimeSpectrum
    R) :
    G.fibreRank 𝔭 = (G.Md.map (algebraMap R (κ 𝔭))).rank

def

minors

L198 ↗

CoherentBaseChange.TwoTermComplex.minors

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex

Lean source · statement

def _root_.CoherentBaseChange.TwoTermComplex.minors (r : ℕ) : Set R

theorem

det_map_submatrix

L205 ↗

CoherentBaseChange.TwoTermComplex.det_map_submatrix

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex

Lean source · statement

theorem _root_.CoherentBaseChange.TwoTermComplex.det_map_submatrix (r : ℕ) (𝔭 :
    PrimeSpectrum R)
    (s : Fin (r + 1) → Module.Free.ChooseBasisIndex R G.C1)
    (t : Fin (r + 1) → Module.Free.ChooseBasisIndex R G.C0) :
    ((G.Md.map (algebraMap R (κ 𝔭))).submatrix s t).det
      = algebraMap R (κ 𝔭) ((G.Md.submatrix s t).det)

theorem

minors_subset_of_fibreRank_le

L217 ↗

CoherentBaseChange.TwoTermComplex.minors_subset_of_fibreRank_le

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex

Lean source · statement

theorem _root_.CoherentBaseChange.TwoTermComplex.minors_subset_of_fibreRank_le (r : ℕ) (𝔭
    : PrimeSpectrum R)
    (hrk : G.fibreRank 𝔭 ≤ r) :
    G.minors r ⊆ (𝔭.asIdeal : Set R)

theorem

setOf_fibreRank_le_eq_zeroLocus

L239 ↗

CoherentBaseChange.TwoTermComplex.setOf_fibreRank_le_eq_zeroLocus

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex

Lean source · statement

theorem _root_.CoherentBaseChange.TwoTermComplex.setOf_fibreRank_le_eq_zeroLocus (r : ℕ) :
    {𝔭 : PrimeSpectrum R | G.fibreRank 𝔭 ≤ r} = PrimeSpectrum.zeroLocus (G.minors r)

theorem

isClosed_fibreRank_le

L254 ↗

CoherentBaseChange.TwoTermComplex.isClosed_fibreRank_le

Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex

Lean source · statement

theorem _root_.CoherentBaseChange.TwoTermComplex.isClosed_fibreRank_le (r : ℕ) :
    IsClosed {𝔭 : PrimeSpectrum R | G.fibreRank 𝔭 ≤ r}

theorem

isClosed_le_fibreH0

L261 ↗

CoherentBaseChange.TwoTermComplex.isClosed_le_fibreH0

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex

Lean source · statement

theorem _root_.CoherentBaseChange.TwoTermComplex.isClosed_le_fibreH0 (n : ℕ) :
    IsClosed {𝔭 : PrimeSpectrum R | n ≤ G.fibreH0 𝔭}

theorem

isClosed_le_h0_perAffine

L283 ↗

CoherentBaseChange.FibreH0Family.isClosed_le_h0_perAffine

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace FibreH0Family
open _root_.CoherentBaseChange.FibreH0Family
open _root_.CoherentBaseChange.FibreH0Family
open _root_.CoherentBaseChange
variable {T : Scheme.{u}} (F : FibreH0Family T)

Lean source · statement

theorem _root_.CoherentBaseChange.FibreH0Family.isClosed_le_h0_perAffine (U : T.Opens) (hU
    : IsAffineOpen U) (n : ℕ) :
    IsClosed {t : U | n ≤ F.h0 t}

theorem

isClosed_le_h0_impl

L294 ↗

CoherentBaseChange.FibreH0Family.isClosed_le_h0_impl

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace FibreH0Family
open _root_.CoherentBaseChange.FibreH0Family
open _root_.CoherentBaseChange.FibreH0Family
open _root_.CoherentBaseChange
variable {T : Scheme.{u}} (F : FibreH0Family T)
open _root_.CoherentBaseChange.FibreH0Family

Lean source · statement

theorem _root_.CoherentBaseChange.FibreH0Family.isClosed_le_h0_impl (n : ℕ) :
    IsClosed {t : T | n ≤ F.h0 t}

theorem

isClosed_setOf_le_h0

L303 ↗

CoherentBaseChange.FibreH0Family.isClosed_setOf_le_h0

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
noncomputable section
universe u v
open scoped TensorProduct
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.Opposite
open _root_.CoherentBaseChange

Lean source · statement

theorem _root_.CoherentBaseChange.FibreH0Family.isClosed_setOf_le_h0 {T : Scheme.{u}}
    (F : FibreH0Family T) (n : ℕ) :
    IsClosed {t : T | n ≤ F.h0 t}

Module documentation

Declarations