Module

Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart

58 declarations indexed from sourceView source ↗

Module documentation

Scheme exists is Open Immersion presheaf over Total of is Open of chart

Imports12

Mathlib.AlgebraicGeometry.Sites.BigZariski
Mathlib.AlgebraicGeometry.Gluing
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.ResidueField
Mathlib.CategoryTheory.MorphismProperty.Representable
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Mathlib.CategoryTheory.Limits.Types.Pullbacks
Mathlib.CategoryTheory.Sites.LocallySurjective
Mathlib.CategoryTheory.Sites.Sheaf
Mathlib.CategoryTheory.Yoneda
Mathlib.Tactic.Choose
Nyll.SchemeTheory.CategoryTheory.OverTotalPresheaf

Imported by2

abbrev

strMap

L49 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.strMap

Documentation

The spectrum morphism associated with the given algebra structure.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]

Lean source · statement

abbrev strMap (A : Type) [CommRing A] [Algebra R A] :
    Spec (CommRingCat.of A) ⟶ Spec (CommRingCat.of R)

lemma

spec_comp_strMap

L55 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.spec_comp_strMap

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}

Lean source · statement

lemma spec_comp_strMap {A B : Type} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    (φ : A →ₐ[R] B) : Spec.map (CommRingCat.ofHom φ.toRingHom) ≫ strMap R A = strMap R B

def

algOf

L62 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.algOf

Documentation

The algebra structure corresponding to a morphism between affine spectra.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}

Lean source · statement

def algOf {A : Type} [CommRing A] (t : Spec (CommRingCat.of A) ⟶ Spec
  (CommRingCat.of R)) :
    Algebra R A

lemma

strMap_algOf

L67 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.strMap_algOf

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}

Lean source · statement

lemma strMap_algOf {A : Type} [CommRing A] (t : Spec (CommRingCat.of A) ⟶ Spec (CommRingCat.of R)) :
    @strMap R _ A _ (algOf t) = t

lemma

algebra_ext_of_strMap_eq

L73 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.algebra_ext_of_strMap_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}

Lean source · statement

lemma algebra_ext_of_strMap_eq {A : Type} [CommRing A] (i₁ i₂ : Algebra R A)
    (h : @strMap R _ A _ i₁ = @strMap R _ A _ i₂) : i₁ = i₂

def

algHomOfSpec

L84 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.algHomOfSpec

Documentation

The algebra homomorphism corresponding contravariantly to a morphism of affine schemes over the base.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}

Lean source · statement

def algHomOfSpec {A B : Type} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    (a : Spec (CommRingCat.of B) ⟶ Spec (CommRingCat.of A)) (ha : a ≫ strMap R A = strMap R B) :
    A →ₐ[R] B

lemma

algHomOfSpec_toRingHom

L95 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.algHomOfSpec_toRingHom

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}

Lean source · statement

lemma algHomOfSpec_toRingHom {A B : Type} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    (a : Spec (CommRingCat.of B) ⟶ Spec (CommRingCat.of A)) (ha : a ≫ strMap R A = strMap R B) :
    (algHomOfSpec a ha).toRingHom = (Spec.preimage a).hom

lemma

spec_algHomOfSpec

L99 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.spec_algHomOfSpec

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}

Lean source · statement

lemma spec_algHomOfSpec {A B : Type} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    (a : Spec (CommRingCat.of B) ⟶ Spec (CommRingCat.of A)) (ha : a ≫ strMap R A = strMap R B) :
    Spec.map (CommRingCat.ofHom (algHomOfSpec a ha).toRingHom) = a

lemma

range_comap_eq

L104 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.range_comap_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}

Lean source · statement

lemma range_comap_eq {A B : Type} [CommRing A] [CommRing B] (φ : A →+* B) :
    Set.range (PrimeSpectrum.comap φ) = Set.range (Spec.map (CommRingCat.ofHom φ))

structure

Ctx

L111 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx

Documentation

A functor with a sheaf realization and a covering family of representable open chart conditions.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}

Lean source · full declaration

structure Ctx (R : Type) [CommRing R] (ι : Type) (S : ι → Type) [∀ i, CommRing (S i)]
    [∀ i, Algebra R (S i)] : Type 1 where
  /-- The value of the functor on each commutative algebra over the base. -/
  F : ∀ (A : Type) [CommRing A] [Algebra R A], Type
  /-- The map on functor elements induced by an algebra homomorphism. -/
  Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B],
      (A →ₐ[R] B) → F A → F B
  /-- The identity algebra homomorphism acts as the identity. -/
  Fmap_id : ∀ (A : Type) [CommRing A] [Algebra R A] (s : F A), Fmap A A (AlgHom.id R A) s = s
  /-- Functor maps preserve composition of algebra homomorphisms. -/
  Fmap_comp : ∀ (A B C : Type) [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B]
      [Algebra R C] (φ : A →ₐ[R] B) (ψ : B →ₐ[R] C) (s : F A),
      Fmap A C (ψ.comp φ) s = Fmap B C ψ (Fmap A B φ s)
  /-- The presheaf on schemes over the base realizing the algebra-valued functor. -/
  G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type
  /-- The equivalence between functor elements and sections on affine schemes over the base. -/
  ev : ∀ (A : Type) [CommRing A] [Algebra R A],
      F A ≃ G.obj (op (Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A)))))
  /-- The total presheaf satisfies the Zariski sheaf condition. -/
  hG : Presheaf.IsSheaf Scheme.zariskiTopology G.overTotal
  /-- The affine realization equivalences commute with algebra homomorphisms. -/
  hev : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (s : F
    A)
      (h : Spec.map (CommRingCat.ofHom φ.toRingHom) ≫ Spec.map (CommRingCat.ofHom (algebraMap R A))
        =
        Spec.map (CommRingCat.ofHom (algebraMap R B))),
      ev B (Fmap A B φ s) =
        G.map (Over.homMk (Spec.map (CommRingCat.ofHom φ.toRingHom)) h :
          Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R B))) ⟶
            Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A)))).op (ev A s)
  /-- The condition defining each proposed affine chart. -/
  P : ι → ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop
  /-- Each chart condition is represented by an open subset after pullback to an affine point. -/
  isOpen : ∀ (i : ι) (A : Type) [CommRing A] [Algebra R A] (s : F A),
      ∃ U : Set (PrimeSpectrum A), IsOpen U ∧
        ∀ (B : Type) [CommRing B] [Algebra R B] (φ : A →ₐ[R] B),
          P i B (Fmap A B φ s) ↔ Set.range (PrimeSpectrum.comap φ.toRingHom) ⊆ U
  /-- The chart subfunctor is represented by its specified coordinate algebra. -/
  chart : ∀ (i : ι) (A : Type) [CommRing A] [Algebra R A], {s : F A // P i A s} ≃ (S i →ₐ[R] A)
  /-- The chart equivalence commutes with extension of the coefficient algebra. -/
  chart_natural : ∀ (i : ι) (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
      (φ : A →ₐ[R] B) (s : {s : F A // P i A s}) (h : P i B (Fmap A B φ s.1)),
      chart i B ⟨Fmap A B φ s.1, h⟩ = φ.comp (chart i A s)
  /-- Every field-valued point belongs to at least one chart. -/
  cover : ∀ (K : Type) [Field K] [Algebra R K] (s : F K), ∃ i, P i K s

abbrev

Sec

L162 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.Sec

Documentation

The sections of the sheaf realization on an affine spectrum.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

abbrev Sec (A : Type) [CommRing A] : Type

lemma

map_comp_apply'

L164 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.map_comp_apply'

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma map_comp_apply' {T T' T'' : Scheme.{0}} (a : T ⟶ T') (b : T' ⟶ T'') (ξ : X.G.overTotal.obj
  (op T'')) :
    X.G.overTotal.map (a ≫ b).op ξ = X.G.overTotal.map a.op (X.G.overTotal.map b.op ξ)

lemma

map_fst

L169 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.map_fst

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma map_fst {T T' : Scheme.{0}} (a : T ⟶ T') (ξ : X.G.overTotal.obj (op T')) :
    (X.G.overTotal.map a.op ξ).1 = a ≫ ξ.1

def

secOf

L175 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.secOf

Documentation

The section of the sheaf realization corresponding to an element of the algebra-valued functor.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

def secOf {A : Type} [CommRing A] [Algebra R A] (s : X.F A) : X.Sec A

lemma

secOf_fst

L178 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.secOf_fst

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma secOf_fst {A : Type} [CommRing A] [Algebra R A] (s : X.F A) : (X.secOf s).1 =
  strMap R A

def

rd

L185 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.rd

Documentation

Recover an element of the algebra-valued functor from a section with the specified base morphism.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

def rd {A : Type} [CommRing A] [Algebra R A] (b : X.Sec A) (hb : b.1 = strMap R A) :
  X.F A

lemma

rd_secOf

L189 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.rd_secOf

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma rd_secOf {A : Type} [CommRing A] [Algebra R A] (s : X.F A) : X.rd (X.secOf s) rfl = s

lemma

secOf_rd

L194 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.secOf_rd

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma secOf_rd {A : Type} [CommRing A] [Algebra R A] (b : X.Sec A) (hb : b.1 = strMap R A) :
    X.secOf (X.rd b hb) = b

lemma

secOf_injective

L201 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.secOf_injective

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma secOf_injective {A : Type} [CommRing A] [Algebra R A] : Function.Injective (X.secOf (A := A))

lemma

exists_eq_secOf

L206 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.exists_eq_secOf

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · full declaration

lemma exists_eq_secOf {A : Type} [CommRing A] (b : X.Sec A) :
    ∃ inst : Algebra R A, letI := inst; ∃ s : X.F A, X.secOf s = b := by
  let := algOf b.1
  exact ⟨algOf b.1, X.rd b (strMap_algOf b.1).symm, X.secOf_rd b _⟩

lemma

map_secOf

L211 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.map_secOf

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma map_secOf {A B : Type} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    (φ : A →ₐ[R] B) (s : X.F A) :
    X.G.overTotal.map (Spec.map (CommRingCat.ofHom φ.toRingHom)).op (X.secOf s) =
      X.secOf (X.Fmap A B φ s)

lemma

map_secOf'

L225 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.map_secOf'

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma map_secOf' {A B : Type} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    (a : Spec (CommRingCat.of B) ⟶ Spec (CommRingCat.of A)) (ha : a ≫ strMap R A = strMap R B) (s :
      X.F A) :
    X.G.overTotal.map a.op (X.secOf s) = X.secOf (X.Fmap A B (algHomOfSpec a ha) s)

def

Q

L235 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.Q

Documentation

A section belongs to the chosen chart for some compatible algebra structure on its coefficient ring.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

def Q (i : ι) {A : Type} [CommRing A] (b : X.Sec A) : Prop

lemma

Q_secOf

L238 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.Q_secOf

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma Q_secOf (i : ι) {A : Type} [CommRing A] [inst : Algebra R A] (s : X.F A) :
    X.Q i (X.secOf s) ↔ X.P i A s

lemma

Q_iff

L248 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.Q_iff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma Q_iff (i : ι) {A : Type} [CommRing A] [Algebra R A] (b : X.Sec A) (hb : b.1 = strMap R A) :
    X.Q i b ↔ X.P i A (X.rd b hb)

lemma

P_map

L252 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.P_map

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma P_map (i : ι) {A B : Type} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R]
  B)
    {s : X.F A} (hs : X.P i A s) : X.P i B (X.Fmap A B φ s)

lemma

P_of_field

L263 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.P_of_field

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma P_of_field (i : ι) {K L : Type} [Field K] [CommRing L] [Nontrivial L] [Algebra R K] [Algebra
  R L]
    (φ : K →ₐ[R] L) {s : X.F K} (hs : X.P i L (X.Fmap K L φ s)) : X.P i K s

lemma

Q_map

L276 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.Q_map

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma Q_map (i : ι) {A B : Type} [CommRing A] [CommRing B]
    (a : Spec (CommRingCat.of B) ⟶ Spec (CommRingCat.of A)) {b : X.Sec A} (hb : X.Q i b) :
    X.Q i (X.G.overTotal.map a.op b)

lemma

Q_iff_of_field

L285 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.Q_iff_of_field

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma Q_iff_of_field (i : ι) {K L : Type} [Field K] [Field L]
    (c : Spec (CommRingCat.of L) ⟶ Spec (CommRingCat.of K)) (b : X.Sec K) :
    X.Q i (X.G.overTotal.map c.op b) ↔ X.Q i b

def

ptSec

L296 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.ptSec

Documentation

The restriction of a sheaf section to the residue-field point.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

def ptSec {T : Scheme.{0}} (ξ : X.G.overTotal.obj (op T)) (x : T) : X.Sec
  (T.residueField x)

def

mem

L301 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.mem

Documentation

The chart condition at a point, tested on the section over its residue field.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

def mem (i : ι) {T : Scheme.{0}} (ξ : X.G.overTotal.obj (op T)) (x : T) : Prop

lemma

mem_map

L304 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.mem_map

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma mem_map (i : ι) {Y T : Scheme.{0}} (a : Y ⟶ T) (ξ : X.G.overTotal.obj (op T)) (y : Y) :
    X.mem i (X.G.overTotal.map a.op ξ) y ↔ X.mem i ξ (a y)

def

U

L312 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.U

Documentation

The open subset of an affine spectrum supplied by the chart condition.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

def U (i : ι) {A : Type} [CommRing A] [Algebra R A] (s : X.F A) : Set (PrimeSpectrum
  A)

lemma

isOpen_U

L316 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.isOpen_U

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma isOpen_U (i : ι) {A : Type} [CommRing A] [Algebra R A] (s : X.F A) : IsOpen (X.U i s)

lemma

U_spec

L319 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.U_spec

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma U_spec (i : ι) {A : Type} [CommRing A] [Algebra R A] (s : X.F A) (B : Type) [CommRing B]
    [Algebra R B] (φ : A →ₐ[R] B) :
    X.P i B (X.Fmap A B φ s) ↔ Set.range (PrimeSpectrum.comap φ.toRingHom) ⊆ X.U i s

lemma

Q_map_secOf_iff

L324 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.Q_map_secOf_iff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma Q_map_secOf_iff (i : ι) {A K : Type} [CommRing A] [Algebra R A] [Field K]
    (c : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of A)) (s : X.F A) :
    X.Q i (X.G.overTotal.map c.op (X.secOf s)) ↔ Set.range c ⊆ X.U i s

lemma

mem_secOf_iff

L332 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.mem_secOf_iff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma mem_secOf_iff (i : ι) {A : Type} [CommRing A] [Algebra R A] (s : X.F A)
    (p : Spec (CommRingCat.of A)) : X.mem i (X.secOf s) p ↔ p ∈ X.U i s

lemma

forall_mem_secOf_iff

L339 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.forall_mem_secOf_iff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma forall_mem_secOf_iff (i : ι) {A : Type} [CommRing A] [Algebra R A] (s : X.F A) :
    (∀ p : Spec (CommRingCat.of A), X.mem i (X.secOf s) p) ↔ X.P i A s

lemma

isOpen_setOf_mem_sec

L350 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.isOpen_setOf_mem_sec

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma isOpen_setOf_mem_sec (i : ι) {A : CommRingCat.{0}} (b : X.G.overTotal.obj (op (Spec A))) :
    IsOpen {p : Spec A | X.mem i b p}

lemma

isOpen_setOf_mem

L356 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.isOpen_setOf_mem

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma isOpen_setOf_mem (i : ι) {T : Scheme.{0}} (ξ : X.G.overTotal.obj (op T)) :
    IsOpen {x : T | X.mem i ξ x}

def

W

L369 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.W

Documentation

The open subspace where the residue-field sections satisfy the chart condition.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

def W (i : ι) {T : Scheme.{0}} (ξ : X.G.overTotal.obj (op T)) : T.Opens

lemma

mem_W_iff

L372 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.mem_W_iff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma mem_W_iff (i : ι) {T : Scheme.{0}} (ξ : X.G.overTotal.obj (op T)) (x : T) :
    x ∈ X.W i ξ ↔ X.mem i ξ x

def

u

L376 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.u

Documentation

The universal element of the chart corresponding to the identity algebra homomorphism.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

def u (i : ι) : {s : X.F (S i) // X.P i (S i) s}

def

univSec

L380 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.univSec

Documentation

The sheaf section corresponding to the universal chart element.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

def univSec (i : ι) : X.Sec (S i)

lemma

chart_Fmap_u

L382 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.chart_Fmap_u

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma chart_Fmap_u (i : ι) {A : Type} [CommRing A] [Algebra R A] (φ : S i →ₐ[R] A)
    (h : X.P i A (X.Fmap (S i) A φ (X.u i).1)) : X.chart i A ⟨X.Fmap (S i) A φ (X.u i).1, h⟩ = φ

lemma

Fmap_chart

L389 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.Fmap_chart

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma Fmap_chart (i : ι) {A : Type} [CommRing A] [Algebra R A] (s : {s : X.F A // X.P i A s}) :
    X.Fmap (S i) A (X.chart i A s) (X.u i).1 = s.1

lemma

mem_univSec

L395 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.mem_univSec

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma mem_univSec (i : ι) (p : Spec (CommRingCat.of (S i))) : X.mem i (X.univSec i) p

lemma

eq_of_map_univSec_eq_affine

L398 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.eq_of_map_univSec_eq_affine

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma eq_of_map_univSec_eq_affine (i : ι) {A : CommRingCat.{0}}
    (b b' : Spec A ⟶ Spec (CommRingCat.of (S i)))
    (h : X.G.overTotal.map b.op (X.univSec i) = X.G.overTotal.map b'.op (X.univSec i)) : b = b'

lemma

eq_of_map_univSec_eq

L419 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.eq_of_map_univSec_eq

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma eq_of_map_univSec_eq (i : ι) {Y : Scheme.{0}} (b b' : Y ⟶ Spec (CommRingCat.of (S i)))
    (h : X.G.overTotal.map b.op (X.univSec i) = X.G.overTotal.map b'.op (X.univSec i)) : b = b'

lemma

exists_map_univSec_eq_affine

L427 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.exists_map_univSec_eq_affine

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma exists_map_univSec_eq_affine (i : ι) {A : CommRingCat.{0}} (b : X.G.overTotal.obj (op (Spec
  A)))
    (h : ∀ p, X.mem i b p) :
    ∃ c : Spec A ⟶ Spec (CommRingCat.of (S i)), X.G.overTotal.map c.op (X.univSec i) = b

lemma

exists_map_univSec_eq

L437 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.exists_map_univSec_eq

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma exists_map_univSec_eq (i : ι) {Y : Scheme.{0}} (ζ : X.G.overTotal.obj (op Y))
    (h : ∀ y, X.mem i ζ y) :
    ∃ φ : Y ⟶ Spec (CommRingCat.of (S i)), X.G.overTotal.map φ.op (X.univSec i) = ζ

def

f

L463 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.f

Documentation

The natural transformation from the represented affine chart to the sheaf realization.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

def f (i : ι) : yoneda.obj (Spec (CommRingCat.of (S i))) ⟶ X.G.overTotal

lemma

f_app

L466 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.f_app

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma f_app (i : ι) {T : Scheme.{0}} (b : T ⟶ Spec (CommRingCat.of (S i))) :
    (X.f i).app (op T) b = X.G.overTotal.map b.op (X.univSec i)

theorem

isOpenImmersion_presheaf

L469 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.isOpenImmersion_presheaf

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

theorem isOpenImmersion_presheaf (i : ι) : IsOpenImmersion.presheaf (X.f i)

theorem

isLocallySurjective

L504 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.isLocallySurjective

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

theorem isLocallySurjective :
    Presheaf.IsLocallySurjective Scheme.zariskiTopology (Sigma.desc X.f)

lemma

f_app_id

L532 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.f_app_id

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

lemma f_app_id (i : ι) :
    (X.f i).app (op (Spec (CommRingCat.of (S i)))) (𝟙 (Spec (CommRingCat.of (S i)))) =
      ⟨strMap R (S i), X.ev (S i) ((X.chart i (S i)).symm (AlgHom.id R (S i))).1⟩

theorem

main

L538 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart.GrassH2.Ctx.main

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassH2
universe u
variable (R : Type) [CommRing R]
variable {R}
variable {ι : Type} {S : ι → Type} [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)] (X : Ctx R ι S)
namespace Ctx

Lean source · statement

theorem main : ∃ f : ∀ i, yoneda.obj (Spec (CommRingCat.of (S i))) ⟶ X.G.overTotal,
    (∀ i, IsOpenImmersion.presheaf (f i)) ∧
    Presheaf.IsLocallySurjective Scheme.zariskiTopology (Sigma.desc f) ∧
    ∀ i, (f i).app (op (Spec (CommRingCat.of (S i)))) (𝟙 (Spec (CommRingCat.of (S i)))) =
      ⟨strMap R (S i), X.ev (S i) ((X.chart i (S i)).symm (AlgHom.id R (S i))).1⟩

theorem

exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart

L557 ↗

AlgebraicGeometry.Scheme.exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
attribute [local simp] GrassH2.Ctx.map_fst
attribute [local simp] GrassH2.Ctx.secOf_fst

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
    (R : Type) [CommRing R]
    (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
    (Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B],
      (A →ₐ[R] B) → F A → F B)
    (Fmap_id : ∀ (A : Type) [CommRing A] [Algebra R A] (s : F A), Fmap A A (AlgHom.id R A) s = s)
    (Fmap_comp : ∀ (A B C : Type) [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B]
      [Algebra R C] (φ : A →ₐ[R] B) (ψ : B →ₐ[R] C) (s : F A),
      Fmap A C (ψ.comp φ) s = Fmap B C ψ (Fmap A B φ s))
    (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type)
    (ev : ∀ (A : Type) [CommRing A] [Algebra R A],
      F A ≃ G.obj (op (Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A))))))
    (hG : Presheaf.IsSheaf Scheme.zariskiTopology G.overTotal)
    (hev : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (s
      : F A)
      (h : Spec.map (CommRingCat.ofHom φ.toRingHom) ≫ Spec.map (CommRingCat.ofHom (algebraMap R A))
        =
        Spec.map (CommRingCat.ofHom (algebraMap R B))),
      ev B (Fmap A B φ s) =
        G.map (Over.homMk (Spec.map (CommRingCat.ofHom φ.toRingHom)) h :
          Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R B))) ⟶
            Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A)))).op (ev A s))
    (ι : Type) (P : ι → ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop)
    (isOpen : ∀ (i : ι) (A : Type) [CommRing A] [Algebra R A] (s : F A),
      ∃ U : Set (PrimeSpectrum A), IsOpen U ∧
        ∀ (B : Type) [CommRing B] [Algebra R B] (φ : A →ₐ[R] B),
          P i B (Fmap A B φ s) ↔ Set.range (PrimeSpectrum.comap φ.toRingHom) ⊆ U)
    (S : ι → Type) [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)]
    (chart : ∀ (i : ι) (A : Type) [CommRing A] [Algebra R A], {s : F A // P i A s} ≃ (S i →ₐ[R] A))
    (chart_natural : ∀ (i : ι) (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
      (φ : A →ₐ[R] B) (s : {s : F A // P i A s}) (h : P i B (Fmap A B φ s.1)),
      chart i B ⟨Fmap A B φ s.1, h⟩ = φ.comp (chart i A s))
    (cover : ∀ (K : Type) [Field K] [Algebra R K] (s : F K), ∃ i, P i K s) :
    ∃ f : ∀ i, yoneda.obj (Spec (CommRingCat.of (S i))) ⟶ G.overTotal,
      (∀ i, IsOpenImmersion.presheaf (f i)) ∧
      Presheaf.IsLocallySurjective Scheme.zariskiTopology (Sigma.desc f) ∧
      ∀ i, (f i).app (op (Spec (CommRingCat.of (S i)))) (𝟙 (Spec (CommRingCat.of (S i)))) =
        ⟨Spec.map (CommRingCat.ofHom (algebraMap R (S i))),
          ev (S i) ((chart i (S i)).symm (AlgHom.id R (S i))).1⟩

Module documentation

Scheme exists is Open Immersion presheaf over Total of is Open of chart

Declarations