NYLL
Module

OrderedAffineCoverComap.lean

Nyll.AlgebraicCurves.Geometry.Schemes.OrderedAffineCoverComap
18 declarations indexed from sourceView source ↗

Module documentation

Ordered Affine Cover Comap

Imports3
Imported by71

Declarations

theorem

preimage_iInf_fin

L29 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.preimage_iInf_fin
Source context 4 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
Lean source · statement
theorem preimage_iInf_fin {Y Z : Scheme.{u}} (f : Y ⟶ Z) {n : ℕ} (W : Fin (n + 1) → Z.Opens) :
    f ⁻¹ᵁ (⨅ j, W j) = ⨅ j, f ⁻¹ᵁ (W j)
def

comap

L48 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.comap
Documentation

The ordered affine cover pulled back along an affine morphism.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
section Comap
variable {X Y : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (f : Y ⟶ X) [IsAffineHom f]
Lean source · full declaration
def comap : Y.OrderedAffineCover where
  ι := 𝒰.ι
  instFintype := 𝒰.instFintype
  instLinearOrder := 𝒰.instLinearOrder
  U i := f ⁻¹ᵁ 𝒰.U i
  isAffineOpen i := (𝒰.isAffineOpen i).preimage f
  iSup_eq_top := by rw [← Scheme.Hom.preimage_iSup, 𝒰.iSup_eq_top]; rfl
theorem

comap_ι

L56 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.comap_ι
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
section Comap
variable {X Y : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (f : Y ⟶ X) [IsAffineHom f]
Lean source · statement
theorem comap_ι : (𝒰.comap f).ι = 𝒰.ι
theorem

comap_U

L58 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.comap_U
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
section Comap
variable {X Y : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (f : Y ⟶ X) [IsAffineHom f]
Lean source · statement
theorem comap_U (i : 𝒰.ι) : (𝒰.comap f).U i = f ⁻¹ᵁ 𝒰.U i
theorem

comap_Idx

L60 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.comap_Idx
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
section Comap
variable {X Y : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (f : Y ⟶ X) [IsAffineHom f]
Lean source · statement
theorem comap_Idx (i : ℕ) : (𝒰.comap f).Idx i = 𝒰.Idx i
theorem

comap_face

L62 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.comap_face
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
section Comap
variable {X Y : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (f : Y ⟶ X) [IsAffineHom f]
Lean source · statement
theorem comap_face {i : ℕ} (s : 𝒰.Idx (i + 1)) (j : Fin (i + 2)) : (𝒰.comap f).face s j = 𝒰.face s
  j
theorem

comap_inter

L65 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.comap_inter
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
section Comap
variable {X Y : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (f : Y ⟶ X) [IsAffineHom f]
Lean source · statement
theorem comap_inter {i : ℕ} (s : 𝒰.Idx i) : (𝒰.comap f).inter s = f ⁻¹ᵁ 𝒰.inter s
theorem

comap_inter_le

L68 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.comap_inter_le
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
section Comap
variable {X Y : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (f : Y ⟶ X) [IsAffineHom f]
Lean source · statement
theorem comap_inter_le {i : ℕ} (s : 𝒰.Idx i) : (𝒰.comap f).inter s ≤ f ⁻¹ᵁ 𝒰.inter s
theorem

le_comap_inter

L71 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.le_comap_inter
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
section Comap
variable {X Y : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (f : Y ⟶ X) [IsAffineHom f]
Lean source · statement
theorem le_comap_inter {i : ℕ} (s : 𝒰.Idx i) : f ⁻¹ᵁ 𝒰.inter s ≤ (𝒰.comap f).inter s
abbrev

baseChange

L83 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.baseChange
Documentation

The ordered affine cover obtained by extending the base ring.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
section BaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (π : X ⟶ Spec (.of
  R))
  (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
abbrev baseChange : (Limits.pullback π (specMap R A)).OrderedAffineCover
theorem

baseChange_ι

L87 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.baseChange_ι
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
section BaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (π : X ⟶ Spec (.of
  R))
  (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem baseChange_ι : (𝒰.baseChange π A).ι = 𝒰.ι
theorem

baseChange_U

L89 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.baseChange_U
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
section BaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (π : X ⟶ Spec (.of
  R))
  (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem baseChange_U (i : 𝒰.ι) :
    (𝒰.baseChange π A).U i = (Limits.pullback.fst π (specMap R A)) ⁻¹ᵁ 𝒰.U i
theorem

baseChange_Idx

L92 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.baseChange_Idx
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
section BaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (π : X ⟶ Spec (.of
  R))
  (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem baseChange_Idx (i : ℕ) : (𝒰.baseChange π A).Idx i = 𝒰.Idx i
theorem

baseChange_face

L94 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.baseChange_face
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
section BaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (π : X ⟶ Spec (.of
  R))
  (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem baseChange_face {i : ℕ} (s : 𝒰.Idx (i + 1)) (j : Fin (i + 2)) :
    (𝒰.baseChange π A).face s j = 𝒰.face s j
theorem

baseChange_inter

L97 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.baseChange_inter
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
section BaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (π : X ⟶ Spec (.of
  R))
  (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem baseChange_inter {i : ℕ} (s : 𝒰.Idx i) :
    (𝒰.baseChange π A).inter s = (Limits.pullback.fst π (specMap R A)) ⁻¹ᵁ 𝒰.inter s
theorem

baseChange_inter_le

L102 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.baseChange_inter_le
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
section BaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (π : X ⟶ Spec (.of
  R))
  (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem baseChange_inter_le {i : ℕ} (s : 𝒰.Idx i) :
    (𝒰.baseChange π A).inter s ≤ (Limits.pullback.fst π (specMap R A)) ⁻¹ᵁ 𝒰.inter s
theorem

le_baseChange_inter

L106 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.le_baseChange_inter
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace Scheme.TwoAffineOpenCover
section BaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (π : X ⟶ Spec (.of
  R))
  (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem le_baseChange_inter {i : ℕ} (s : 𝒰.Idx i) :
    (Limits.pullback.fst π (specMap R A)) ⁻¹ᵁ 𝒰.inter s ≤ (𝒰.baseChange π A).inter s
theorem

toOrderedAffineCover_pullback

L122 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.toOrderedAffineCover_pullback
Source context 5 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (π : X ⟶ Spec (.of
  R))
  (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem toOrderedAffineCover_pullback :
    (𝒱.pullback π A).toOrderedAffineCover = 𝒱.toOrderedAffineCover.baseChange π A

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.