Module

exists_isFinite_to_proj_of_completeOrthogonalIdempotents.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_isFinite_to_proj_of_completeOrthogonalIdempotents

27 declarations indexed from sourceView source ↗

Module documentation

exists is Finite to proj of complete Orthogonal Idempotents

Imports21

Mathlib.Algebra.BigOperators.Pi
Mathlib.Algebra.DirectSum.Basic
Mathlib.Algebra.DirectSum.Decomposition
Mathlib.Algebra.DirectSum.Ring
Mathlib.AlgebraicGeometry.Gluing
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.Morphisms.Basic
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Mathlib.RingTheory.Idempotents
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.Tactic.Choose

Imported by2

def

grading

L55 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.grading

Documentation

The product grading whose homogeneous elements are homogeneous in every factor.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]

Lean source · full declaration

def grading (n : ℕ) : AddSubgroup (Π i, A i) where
  carrier := {a | ∀ i, a i ∈ 𝒜 i n}
  add_mem' ha hb i := add_mem (ha i) (hb i)
  zero_mem' _i := zero_mem _
  neg_mem' ha i := neg_mem (ha i)

lemma

mem_grading

L63 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.mem_grading

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]
variable {A σ 𝒜} in
omit [Fintype ι'] [DecidableEq ι'] [(i : ι') → GradedRing (𝒜 i)] in

Lean source · statement

lemma mem_grading {n : ℕ} {a : Π i, A i} : a ∈ grading A σ 𝒜 n ↔ ∀ i, a i ∈ 𝒜 i n

lemma

single_mem_grading

L65 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.single_mem_grading

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]
variable {A σ 𝒜} in
omit [Fintype ι'] [(i : ι') → GradedRing (𝒜 i)] in

Lean source · statement

lemma single_mem_grading {n : ℕ} (i : ι') {x : A i} (hx : x ∈ 𝒜 i n) :
    Pi.single i x ∈ grading A σ 𝒜 n

instance

(anonymous instance)

L72 ↗

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]
variable {A σ 𝒜} in

Lean source · full declaration

instance : SetLike.GradedMonoid (grading A σ 𝒜) where
  one_mem _i := SetLike.one_mem_graded _
  mul_mem _ _ _ _ ha hb k := SetLike.mul_mem_graded (ha k) (hb k)

def

singlePiece

L77 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.singlePiece

Documentation

The additive map inserting one homogeneous component into the product grading.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]
variable {A σ 𝒜} in

Lean source · full declaration

def singlePiece (i : ι') (n : ℕ) : 𝒜 i n →+ grading A σ 𝒜 n where
  toFun x := ⟨Pi.single i (x : A i), single_mem_grading A σ 𝒜 i x.2⟩
  map_zero' := by ext : 1; simp
  map_add' x y := by ext : 1; simp [Pi.single_add]

lemma

coe_singlePiece

L82 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.coe_singlePiece

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]
variable {A σ 𝒜} in
omit [Fintype ι'] [(i : ι') → GradedRing (𝒜 i)] in

Lean source · statement

lemma coe_singlePiece (i : ι') (n : ℕ) (x : 𝒜 i n) :
    (singlePiece A σ 𝒜 i n x : Π i, A i) = Pi.single i (x : A i)

def

decomposeAux

L86 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.decomposeAux

Documentation

The homogeneous decomposition of an element of the product ring.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]
variable {A σ 𝒜} in

Lean source · statement

def decomposeAux : (Π i, A i) →+ ⨁ n, grading A σ 𝒜 n

lemma

coe_comp_map_singlePiece

L90 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.coe_comp_map_singlePiece

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]
variable {A σ 𝒜} in
omit [Fintype ι'] [(i : ι') → GradedRing (𝒜 i)] in

Lean source · statement

lemma coe_comp_map_singlePiece (i : ι') :
    (DirectSum.coeAddMonoidHom (grading A σ 𝒜)).comp (DirectSum.map (singlePiece A σ 𝒜 i)) =
      (AddMonoidHom.single A i).comp (DirectSum.coeAddMonoidHom (𝒜 i))

lemma

decomposeAux_apply

L96 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.decomposeAux_apply

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]
variable {A σ 𝒜} in

Lean source · statement

lemma decomposeAux_apply (a : Π i, A i) :
    decomposeAux A σ 𝒜 a = ∑ i, DirectSum.map (singlePiece A σ 𝒜 i) (decompose (𝒜 i) (a i))

instance

(anonymous instance)

L100 ↗

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]
variable {A σ 𝒜} in

Lean source · full declaration

instance : GradedRing (grading A σ 𝒜) where
  decompose' := decomposeAux A σ 𝒜
  left_inv a := by
    rw [decomposeAux_apply, map_sum]
    conv_rhs => rw [← Finset.univ_sum_single a]
    refine Finset.sum_congr rfl fun i _ => ?_
    have := congrArg (fun φ => φ (decompose (𝒜 i) (a i))) (coe_comp_map_singlePiece A σ 𝒜 i)
    simp only [AddMonoidHom.coe_comp, Function.comp_apply, AddMonoidHom.single_apply] at this
    rw [this]
    congr 1
    exact (decompose (𝒜 i)).symm_apply_apply (a i)
  right_inv y := by
    induction y using DirectSum.induction_on with
    | zero => simp
    | add y z hy hz => rw [map_add, map_add, hy, hz]
    | of n b =>
      rw [DirectSum.coeAddMonoidHom_of, decomposeAux_apply]
      have : ∀ i, decompose (𝒜 i) ((b : Π i, A i) i) = DirectSum.of _ n ⟨(b : Π i, A i) i, b.2 i⟩ :=
        fun i => decompose_of_mem _ (b.2 i)
      simp_rw [this, DirectSum.map_of, ← map_sum]
      congr 1
      ext : 1
      simp only [AddSubgroup.val_finsetSum, coe_singlePiece]
      exact Finset.univ_sum_single _

def

π

L126 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.π

Documentation

The graded ring projection from the product grading to one factor.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]
variable {A σ 𝒜} in

Lean source · full declaration

def π (k : ι') : grading A σ 𝒜 →+*ᵍ 𝒜 k where
  __ := Pi.evalRingHom A k
  map_mem hx := hx k

lemma

π_apply

L130 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.π_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]
variable {A σ 𝒜} in
omit [Fintype ι'] [DecidableEq ι'] [(i : ι') → GradedRing (𝒜 i)] in

Lean source · statement

lemma π_apply (k : ι') (a : Π i, A i) : π A σ 𝒜 k a = a k

lemma

irrelevant_le_map_π

L132 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.irrelevant_le_map_π

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]
variable {A σ 𝒜} in

Lean source · statement

lemma irrelevant_le_map_π (k : ι') :
    HomogeneousIdeal.irrelevant (𝒜 k) ≤
      (HomogeneousIdeal.irrelevant (grading A σ 𝒜)).map (π A σ 𝒜 k)

lemma

awayMap_π_single_bijective

L144 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.awayMap_π_single_bijective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]
variable {A σ 𝒜} in

Lean source · statement

lemma awayMap_π_single_bijective (k : ι') {d : ℕ} (t : A k) (ht : t ∈ 𝒜 k d) :
    Function.Bijective (HomogeneousLocalization.Away.map (π A σ 𝒜 k) (Pi.single k t))

def

ChartIdx

L191 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.ChartIdx

Documentation

The homogeneous elements of positive degree used to index the projective charts.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]

Lean source · statement

def ChartIdx : Type u

def

chartFn

L194 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.chartFn

Documentation

The homogeneous chart element supported in the selected factor.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]

Lean source · statement

def chartFn : ChartIdx A σ 𝒜 → Π i, A i

lemma

chartFn_deg

L196 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.chartFn_deg

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]
omit [Fintype ι'] [(i : ι') → GradedRing (𝒜 i)] in

Lean source · statement

lemma chartFn_deg (c : ChartIdx A σ 𝒜) : chartFn A σ 𝒜 c ∈ grading A σ 𝒜 (c.2.1 : ℕ)

lemma

irrelevant_le_span_chartFn

L199 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.irrelevant_le_span_chartFn

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]

Lean source · statement

lemma irrelevant_le_span_chartFn :
    (HomogeneousIdeal.irrelevant (grading A σ 𝒜)).toIdeal ≤
      Ideal.span (Set.range (chartFn A σ 𝒜))

def

chartCover

L209 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.chartCover

Documentation

The affine cover of the projective spectrum from the supported homogeneous chart elements.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]

Lean source · statement

def chartCover : (Proj (grading A σ 𝒜)).AffineOpenCover

abbrev

incl

L215 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.incl

Documentation

The projective spectrum morphism induced by the projection onto one graded factor.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]

Lean source · statement

abbrev incl (k : ι') : Proj (𝒜 k) ⟶ Proj (grading A σ 𝒜)

lemma

mem_basicOpen_incl_iff

L218 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.mem_basicOpen_incl_iff

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]

Lean source · statement

lemma mem_basicOpen_incl_iff {k : ι'} (q : Proj (𝒜 k)) (a : Π i, A i) :
    incl A σ 𝒜 k q ∈ Proj.basicOpen (grading A σ 𝒜) a ↔ q ∈ Proj.basicOpen (𝒜 k) (a k)

lemma

chart_same

L225 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.chart_same

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]

Lean source · statement

lemma chart_same (k : ι') {d : ℕ} (hd : 0 < d) (t : A k) (ht : t ∈ 𝒜 k d) :
    IsOpenImmersion (pullback.snd (incl A σ 𝒜 k)
      (Proj.awayι (grading A σ 𝒜) (Pi.single k t) (single_mem_grading A σ 𝒜 k ht) hd)) ∧
    Set.range (Proj.awayι (grading A σ 𝒜) (Pi.single k t) (single_mem_grading A σ 𝒜 k ht) hd) ⊆
      Set.range (incl A σ 𝒜 k)

lemma

chart_ne

L257 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.chart_ne

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]

Lean source · statement

lemma chart_ne {k j : ι'} (hjk : j ≠ k) {d : ℕ} (hd : 0 < d) (t : A j) (ht : t ∈ 𝒜 j d) :
    IsEmpty ↑(pullback (incl A σ 𝒜 k)
      (Proj.awayι (grading A σ 𝒜) (Pi.single j t) (single_mem_grading A σ 𝒜 j ht) hd))

instance

isOpenImmersion_incl

L268 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.isOpenImmersion_incl

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]

Lean source · statement

instance isOpenImmersion_incl (k : ι') : IsOpenImmersion (incl A σ 𝒜 k)

lemma

exists_incl_eq

L279 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.exists_incl_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]

Lean source · statement

lemma exists_incl_eq (p : Proj (grading A σ 𝒜)) : ∃ k q, incl A σ 𝒜 k q = p

lemma

eq_of_incl_eq

L284 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isFinite_to_proj_of_completeOrthogonalIdempotents.PiGradedAux.eq_of_incl_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
namespace PiGradedAux
variable {ι' : Type} [Fintype ι'] [DecidableEq ι']
  (A : ι' → Type u) [∀ i, CommRing (A i)] (σ : ι' → Type u) [∀ i, SetLike (σ i) (A i)]
  [∀ i, AddSubgroupClass (σ i) (A i)] (𝒜 : ∀ i, ℕ → σ i) [∀ i, GradedRing (𝒜 i)]

Lean source · statement

lemma eq_of_incl_eq {k l : ι'} (q : Proj (𝒜 k)) (q' : Proj (𝒜 l))
    (h : incl A σ 𝒜 k q = incl A σ 𝒜 l q') : k = l

theorem

exists_isFinite_to_proj_of_completeOrthogonalIdempotents

L307 ↗

AlgebraicGeometry.exists_isFinite_to_proj_of_completeOrthogonalIdempotents

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isFinite_to_proj_of_completeOrthogonalIdempotents
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry DirectSum HomogeneousIdeal
open PiGradedAux in

Lean source · statement

theorem _root_.AlgebraicGeometry.exists_isFinite_to_proj_of_completeOrthogonalIdempotents
    {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {m : ℕ} (e : Fin m → R)
    (he : CompleteOrthogonalIdempotents e)
    (hfin : ∀ i : Fin m, ∃ (A σ : Type u) (_ : CommRing A) (_ : SetLike σ A) (_ : AddSubgroupClass
      σ A) (𝒜 : ℕ → σ)
      (_ : GradedRing 𝒜)
      (ι : pullback f (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away (e i))))) ⟶
        Proj 𝒜),
      IsFinite ι) :
    ∃ (A σ : Type u) (_ : CommRing A) (_ : SetLike σ A) (_ : AddSubgroupClass σ A) (𝒜 : ℕ → σ)
      (_ : GradedRing 𝒜) (ι : X ⟶ Proj 𝒜), IsFinite ι

Module documentation

exists is Finite to proj of complete Orthogonal Idempotents

Declarations