NYLL
Module

Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
20 declarations indexed from sourceView source ↗

Module documentation

Scheme forall mem iff of subset union preimage or disjoint

Imports8
Imported by3

Declarations

def

T

L54 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.T
Documentation

Right translation by the chosen section in the category of schemes over the base.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
Lean source · statement
def T (a : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) : Over.mk t ⟶ Over.mk t
def

S

L59 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.S
Documentation

Left translation by the chosen section composed with inversion in the group object.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
Lean source · statement
def S (c : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) : Over.mk t ⟶ Over.mk t
def

P

L64 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.P
Documentation

The underlying point of the scheme determined by a section over the base field.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
Lean source · statement
def P (y : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) : X
lemma

toUnit_pt_comp

L70 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.toUnit_pt_comp
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
variable {t}
omit [GrpObj (Over.mk t)] in
Lean source · statement
lemma toUnit_pt_comp (a : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) :
    CartesianMonoidalCategory.toUnit (Over.mk (𝟙 (Spec (CommRingCat.of k)))) ≫ a = a
lemma

pt_comp_T

L76 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.pt_comp_T
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
variable {t}
Lean source · statement
lemma pt_comp_T (y a : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) : y ≫ T t a = y * a
lemma

pt_comp_S

L82 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.pt_comp_S
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
variable {t}
Lean source · statement
lemma pt_comp_S (y c : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) : y ≫ S t c = c * y⁻¹
lemma

T_comp_T

L88 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.T_comp_T
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
variable {t}
Lean source · statement
lemma T_comp_T (a b : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) : T t a ≫ T t b = T t (a *
  b)
lemma

T_one

L98 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.T_one
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
variable {t}
Lean source · statement
lemma T_one : T t (1 : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) = 𝟙 (Over.mk t)
lemma

S_comp_S

L104 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.S_comp_S
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
variable {t}
Lean source · statement
lemma S_comp_S [IsCommMonObj (Over.mk t)] (c : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) :
    S t c ≫ S t c = 𝟙 (Over.mk t)
instance

isIso_T

L117 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.isIso_T
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
variable {t}
Lean source · statement
instance isIso_T (a : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) : IsIso (T t a)
instance

isIso_S

L120 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.isIso_S
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
variable {t}
Lean source · statement
instance isIso_S [IsCommMonObj (Over.mk t)] (c : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶
  Over.mk t) :
    IsIso (S t c)
lemma

P_comp

L126 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.P_comp
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
variable {t}
omit [GrpObj (Over.mk t)] in
Lean source · statement
lemma P_comp (y : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) (φ : Over.mk t ⟶ Over.mk t) :
    P t (y ≫ φ) = φ.left.base (P t y)
lemma

T_base_P

L129 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.T_base_P
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
variable {t}
Lean source · statement
lemma T_base_P (y a : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) :
    (T t a).left.base (P t y) = P t (y * a)
lemma

S_base_P

L133 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.S_base_P
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
variable {t}
Lean source · statement
lemma S_base_P (y c : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) :
    (S t c).left.base (P t y) = P t (c * y⁻¹)
lemma

surjective_left_base

L137 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.surjective_left_base
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
variable {t}
omit [GrpObj (Over.mk t)] in
Lean source · statement
lemma surjective_left_base (φ : Over.mk t ⟶ Over.mk t) [IsIso φ] : Function.Surjective φ.left.base
lemma

compl_preimage

L142 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.compl_preimage
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
variable {t}
omit [GrpObj (Over.mk t)] in
Lean source · statement
lemma compl_preimage (φ : Over.mk t ⟶ Over.mk t) [IsIso φ] {D : Set X} (hD : IsClosed D) (hD' : D ≠
  Set.univ) :
    IsOpen (φ.left.base ⁻¹' D)ᶜ ∧ ((φ.left.base ⁻¹' D)ᶜ).Nonempty
lemma

exists_P_mem

L155 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.exists_P_mem
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
variable {t}
section main
variable [IsAlgClosed k] [LocallyOfFiniteType t] [IsIntegral X] [IsCommMonObj (Over.mk t)]
omit [GrpObj (Over.mk t)] [IsIntegral X] [IsCommMonObj (Over.mk t)] in
Lean source · statement
lemma exists_P_mem {U : Set X} (hU : IsOpen U) (hne : U.Nonempty) :
    ∃ b : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t, P t b ∈ U
lemma

key

L168 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.key
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
variable {t}
section main
variable [IsAlgClosed k] [LocallyOfFiniteType t] [IsIntegral X] [IsCommMonObj (Over.mk t)]
Lean source · statement
lemma key {D : Set X} (hD : IsClosed D) (hD' : D ≠ Set.univ) {Z : Set X} (_hZ' : IsIrreducible Z)
    (h : ∀ a b : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t,
      Z ⊆ ((T t a).left.base ⁻¹' D ∪ (T t b).left.base ⁻¹' D ∪ (T t (a * b)⁻¹).left.base ⁻¹' D) ∨
      Disjoint Z ((T t a).left.base ⁻¹' D ∪ (T t b).left.base ⁻¹' D ∪ (T t (a * b)⁻¹).left.base ⁻¹'
        D))
    (z z' d : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) (hz : P t z ∈ Z) (hz' : P t z' ∈ Z)
    (hd : P t d ∈ D) : P t (d * (z⁻¹ * z')) ∈ D
theorem

main

L215 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint.AlgebraicGeometry.Scheme.TranslateCore.main
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TranslateCore
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
  [GrpObj (Over.mk t)]
variable {t}
section main
variable [IsAlgClosed k] [LocallyOfFiniteType t] [IsIntegral X] [IsCommMonObj (Over.mk t)]
Lean source · statement
theorem main (D : Set X) (hD : IsClosed D) (hD' : D ≠ Set.univ) (Z : Set X) (_hZ : IsClosed Z)
    (hZ' : IsIrreducible Z)
    (h : ∀ a b : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t,
      Z ⊆ ((T t a).left.base ⁻¹' D ∪ (T t b).left.base ⁻¹' D ∪ (T t (a * b)⁻¹).left.base ⁻¹' D) ∨
      Disjoint Z ((T t a).left.base ⁻¹' D ∪ (T t b).left.base ⁻¹' D ∪ (T t (a * b)⁻¹).left.base ⁻¹'
        D))
    (z z' : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) (hz : P t z ∈ Z) (hz' : P t z' ∈ Z)
    (d : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) :
    P t d ∈ D ↔ P t (d * (z⁻¹ * z')) ∈ D
theorem

forall_mem_iff_of_subset_union_preimage_or_disjoint

L233 ↗
AlgebraicGeometry.Scheme.forall_mem_iff_of_subset_union_preimage_or_disjoint
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.forall_mem_iff_of_subset_union_preimage_or_disjoint
    (k : Type u) [Field k] [IsAlgClosed k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
    [LocallyOfFiniteType t] [IsIntegral X] [GrpObj (Over.mk t)] [IsCommMonObj (Over.mk t)]
    (D : Set X) (hD : IsClosed D) (hD' : D ≠ Set.univ) (Z : Set X) (hZ : IsClosed Z) (hZ' :
      IsIrreducible Z)
    (h : ∀ a b : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t,
      Z ⊆ ((𝟙 (Over.mk t) * (CartesianMonoidalCategory.toUnit (Over.mk t) ≫ a)).left.base ⁻¹' D ∪
            (𝟙 (Over.mk t) * (CartesianMonoidalCategory.toUnit (Over.mk t) ≫ b)).left.base ⁻¹' D ∪
            (𝟙 (Over.mk t) * (CartesianMonoidalCategory.toUnit (Over.mk t) ≫ (a * b)⁻¹)).left.base
              ⁻¹' D) ∨
      Disjoint Z ((𝟙 (Over.mk t) * (CartesianMonoidalCategory.toUnit (Over.mk t) ≫ a)).left.base
        ⁻¹' D ∪
            (𝟙 (Over.mk t) * (CartesianMonoidalCategory.toUnit (Over.mk t) ≫ b)).left.base ⁻¹' D ∪
            (𝟙 (Over.mk t) * (CartesianMonoidalCategory.toUnit (Over.mk t) ≫ (a * b)⁻¹)).left.base
              ⁻¹' D))
    (z z' : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t)
    (hz : z.left.base (IsLocalRing.closedPoint k) ∈ Z) (hz' : z'.left.base (IsLocalRing.closedPoint
      k) ∈ Z)
    (d : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t) :
    d.left.base (IsLocalRing.closedPoint k) ∈ D ↔ (d * (z⁻¹ * z')).left.base
      (IsLocalRing.closedPoint k) ∈ D

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