NYLL
Module

SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi.lean

Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
16 declarations indexed from sourceView source ↗

Module documentation

Smooth Proper Curve exists sections injective of tensor Product alg Equiv pi

Imports2
Imported by3

Declarations

def

proj

L48 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi.AlgebraicGeometry.SmoothProperCurve.SplitSectionsImpl.proj
Documentation

Projection to a chosen factor of the split base-changed algebra.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace SplitSectionsImpl
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section Ring
variable {R₀ R' B : Type u} [CommRing R₀] [CommRing R'] [CommRing B] [Algebra R₀ B] [Algebra R₀ R']
  {d : ℕ} (φ : (R' ⊗[R₀] B) ≃ₐ[R'] (Fin d → R'))
Lean source · statement
def proj (m : Fin d) : (R' ⊗[R₀] B) →ₐ[R'] R'
theorem

proj_apply

L51 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi.AlgebraicGeometry.SmoothProperCurve.SplitSectionsImpl.proj_apply
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace SplitSectionsImpl
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section Ring
variable {R₀ R' B : Type u} [CommRing R₀] [CommRing R'] [CommRing B] [Algebra R₀ B] [Algebra R₀ R']
  {d : ℕ} (φ : (R' ⊗[R₀] B) ≃ₐ[R'] (Fin d → R'))
Lean source · statement
theorem proj_apply (m : Fin d) (z : R' ⊗[R₀] B) : proj φ m z = φ z m
def

coord

L54 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi.AlgebraicGeometry.SmoothProperCurve.SplitSectionsImpl.coord
Documentation

The coordinate ring homomorphism obtained from the chosen factor of the split algebra.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace SplitSectionsImpl
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section Ring
variable {R₀ R' B : Type u} [CommRing R₀] [CommRing R'] [CommRing B] [Algebra R₀ B] [Algebra R₀ R']
  {d : ℕ} (φ : (R' ⊗[R₀] B) ≃ₐ[R'] (Fin d → R'))
Lean source · statement
def coord (m : Fin d) : B →+* R'
theorem

coord_apply

L58 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi.AlgebraicGeometry.SmoothProperCurve.SplitSectionsImpl.coord_apply
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace SplitSectionsImpl
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section Ring
variable {R₀ R' B : Type u} [CommRing R₀] [CommRing R'] [CommRing B] [Algebra R₀ B] [Algebra R₀ R']
  {d : ℕ} (φ : (R' ⊗[R₀] B) ≃ₐ[R'] (Fin d → R'))
Lean source · statement
theorem coord_apply (m : Fin d) (b : B) : coord φ m b = φ (1 ⊗ₜ[R₀] b) m
theorem

proj_tmul

L60 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi.AlgebraicGeometry.SmoothProperCurve.SplitSectionsImpl.proj_tmul
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace SplitSectionsImpl
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section Ring
variable {R₀ R' B : Type u} [CommRing R₀] [CommRing R'] [CommRing B] [Algebra R₀ B] [Algebra R₀ R']
  {d : ℕ} (φ : (R' ⊗[R₀] B) ≃ₐ[R'] (Fin d → R'))
Lean source · statement
theorem proj_tmul (m : Fin d) (a : R') (b : B) : proj φ m (a ⊗ₜ[R₀] b) = a * coord φ m b
theorem

coord_algebraMap

L69 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi.AlgebraicGeometry.SmoothProperCurve.SplitSectionsImpl.coord_algebraMap
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace SplitSectionsImpl
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section Ring
variable {R₀ R' B : Type u} [CommRing R₀] [CommRing R'] [CommRing B] [Algebra R₀ B] [Algebra R₀ R']
  {d : ℕ} (φ : (R' ⊗[R₀] B) ≃ₐ[R'] (Fin d → R'))
Lean source · statement
theorem coord_algebraMap (m : Fin d) (x : R₀) : coord φ m (algebraMap R₀ B x) = algebraMap R₀ R' x
theorem

coord_comp_algebraMap

L79 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi.AlgebraicGeometry.SmoothProperCurve.SplitSectionsImpl.coord_comp_algebraMap
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace SplitSectionsImpl
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section Ring
variable {R₀ R' B : Type u} [CommRing R₀] [CommRing R'] [CommRing B] [Algebra R₀ B] [Algebra R₀ R']
  {d : ℕ} (φ : (R' ⊗[R₀] B) ≃ₐ[R'] (Fin d → R'))
Lean source · statement
theorem coord_comp_algebraMap (m : Fin d) : (coord φ m).comp (algebraMap R₀ B) = algebraMap R₀ R'
theorem

eq_of_apply_coord_eq

L82 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi.AlgebraicGeometry.SmoothProperCurve.SplitSectionsImpl.eq_of_apply_coord_eq
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace SplitSectionsImpl
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section Ring
variable {R₀ R' B : Type u} [CommRing R₀] [CommRing R'] [CommRing B] [Algebra R₀ B] [Algebra R₀ R']
  {d : ℕ} (φ : (R' ⊗[R₀] B) ≃ₐ[R'] (Fin d → R'))
Lean source · statement
theorem eq_of_apply_coord_eq {T : Type u} [CommRing T] [Nontrivial T] (t : R' →+* T) {i j : Fin d}
    (h : ∀ b : B, t (coord φ i b) = t (coord φ j b)) : i = j
abbrev

specCoord

L107 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi.AlgebraicGeometry.SmoothProperCurve.SplitSectionsImpl.specCoord
Documentation

The morphism of spectra corresponding to the chosen coordinate homomorphism.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace SplitSectionsImpl
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section Scheme
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  {R₀ : Type u} [CommRing R₀] [Algebra R R₀] {B : Type u} [CommRing B] [Algebra R₀ B]
  (ι : Spec (CommRingCat.of B) ⟶ pullback c (specMap R R₀))
  (hι : ι ≫ baseChange R c R₀ = specMap R₀ B)
  {R' : Type u} [CommRing R'] [Algebra R R'] [Algebra R₀ R'] [IsScalarTower R R₀ R']
  {d : ℕ} (φ : (R' ⊗[R₀] B) ≃ₐ[R'] (Fin d → R'))
Lean source · statement
abbrev specCoord (m : Fin d) : Spec (CommRingCat.of R') ⟶ Spec (CommRingCat.of B)
theorem

specCoord_comp_specMap

L110 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi.AlgebraicGeometry.SmoothProperCurve.SplitSectionsImpl.specCoord_comp_specMap
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace SplitSectionsImpl
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section Scheme
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  {R₀ : Type u} [CommRing R₀] [Algebra R R₀] {B : Type u} [CommRing B] [Algebra R₀ B]
  (ι : Spec (CommRingCat.of B) ⟶ pullback c (specMap R R₀))
  (hι : ι ≫ baseChange R c R₀ = specMap R₀ B)
  {R' : Type u} [CommRing R'] [Algebra R R'] [Algebra R₀ R'] [IsScalarTower R R₀ R']
  {d : ℕ} (φ : (R' ⊗[R₀] B) ≃ₐ[R'] (Fin d → R'))
Lean source · statement
theorem specCoord_comp_specMap (m : Fin d) : specCoord φ m ≫ specMap R₀ B = specMap R₀ R'
def

secTop

L116 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi.AlgebraicGeometry.SmoothProperCurve.SplitSectionsImpl.secTop
Documentation

The curve-valued point obtained from a factor of the split affine algebra.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace SplitSectionsImpl
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section Scheme
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  {R₀ : Type u} [CommRing R₀] [Algebra R R₀] {B : Type u} [CommRing B] [Algebra R₀ B]
  (ι : Spec (CommRingCat.of B) ⟶ pullback c (specMap R R₀))
  (hι : ι ≫ baseChange R c R₀ = specMap R₀ B)
  {R' : Type u} [CommRing R'] [Algebra R R'] [Algebra R₀ R'] [IsScalarTower R R₀ R']
  {d : ℕ} (φ : (R' ⊗[R₀] B) ≃ₐ[R'] (Fin d → R'))
Lean source · statement
def secTop (m : Fin d) : Spec (CommRingCat.of R') ⟶ C
theorem

secTop_comp

L119 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi.AlgebraicGeometry.SmoothProperCurve.SplitSectionsImpl.secTop_comp
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace SplitSectionsImpl
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section Scheme
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  {R₀ : Type u} [CommRing R₀] [Algebra R R₀] {B : Type u} [CommRing B] [Algebra R₀ B]
  (ι : Spec (CommRingCat.of B) ⟶ pullback c (specMap R R₀))
  (hι : ι ≫ baseChange R c R₀ = specMap R₀ B)
  {R' : Type u} [CommRing R'] [Algebra R R'] [Algebra R₀ R'] [IsScalarTower R R₀ R']
  {d : ℕ} (φ : (R' ⊗[R₀] B) ≃ₐ[R'] (Fin d → R'))
include hι in
Lean source · statement
theorem secTop_comp (m : Fin d) : secTop c ι φ m ≫ c = specMap R R'
def

sec

L129 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi.AlgebraicGeometry.SmoothProperCurve.SplitSectionsImpl.sec
Documentation

The section of the base-changed curve determined by the chosen split factor.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace SplitSectionsImpl
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section Scheme
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  {R₀ : Type u} [CommRing R₀] [Algebra R R₀] {B : Type u} [CommRing B] [Algebra R₀ B]
  (ι : Spec (CommRingCat.of B) ⟶ pullback c (specMap R R₀))
  (hι : ι ≫ baseChange R c R₀ = specMap R₀ B)
  {R' : Type u} [CommRing R'] [Algebra R R'] [Algebra R₀ R'] [IsScalarTower R R₀ R']
  {d : ℕ} (φ : (R' ⊗[R₀] B) ≃ₐ[R'] (Fin d → R'))
Lean source · statement
def sec (m : Fin d) : SchemeHomOver (𝟙 (Spec (CommRingCat.of R'))) (baseChange R c
  R')
theorem

sec_fst

L134 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi.AlgebraicGeometry.SmoothProperCurve.SplitSectionsImpl.sec_fst
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace SplitSectionsImpl
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section Scheme
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  {R₀ : Type u} [CommRing R₀] [Algebra R R₀] {B : Type u} [CommRing B] [Algebra R₀ B]
  (ι : Spec (CommRingCat.of B) ⟶ pullback c (specMap R R₀))
  (hι : ι ≫ baseChange R c R₀ = specMap R₀ B)
  {R' : Type u} [CommRing R'] [Algebra R R'] [Algebra R₀ R'] [IsScalarTower R R₀ R']
  {d : ℕ} (φ : (R' ⊗[R₀] B) ≃ₐ[R'] (Fin d → R'))
Lean source · statement
theorem sec_fst (m : Fin d) : (sec c ι hι φ m).1 ≫ pullback.fst c (specMap R R') = secTop c ι φ m
theorem

sec_injective

L137 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi.AlgebraicGeometry.SmoothProperCurve.SplitSectionsImpl.sec_injective
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace SplitSectionsImpl
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section Scheme
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  {R₀ : Type u} [CommRing R₀] [Algebra R R₀] {B : Type u} [CommRing B] [Algebra R₀ B]
  (ι : Spec (CommRingCat.of B) ⟶ pullback c (specMap R R₀))
  (hι : ι ≫ baseChange R c R₀ = specMap R₀ B)
  {R' : Type u} [CommRing R'] [Algebra R R'] [Algebra R₀ R'] [IsScalarTower R R₀ R']
  {d : ℕ} (φ : (R' ⊗[R₀] B) ≃ₐ[R'] (Fin d → R'))
Lean source · full declaration
theorem sec_injective [IsClosedImmersion ι] (k : Type u) [Field k]
    (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R')) :
    Function.Injective fun m => s ≫ (sec c ι hι φ m).1 := by
  intro i j h
  have hι' : ι ≫ pullback.snd c (specMap R R₀) = specMap R₀ B := hι
  have h1 : s ≫ secTop c ι φ i = s ≫ secTop c ι φ j := by
    have := congrArg (· ≫ pullback.fst c (specMap R R')) h
    simpa only [Category.assoc, sec_fst] using this
  have h2 : (s ≫ specCoord φ i) ≫ ι = (s ≫ specCoord φ j) ≫ ι := by
    apply pullback.hom_ext
    · simpa only [secTop, Category.assoc] using h1
    · simp only [Category.assoc, hι', specCoord_comp_specMap φ]
  have h3 : s ≫ specCoord φ i = s ≫ specCoord φ j := (cancel_mono ι).mp h2
  obtain ⟨θ, rfl⟩ : ∃ θ, Spec.map θ = s := ⟨Spec.preimage s, Spec.map_preimage s⟩
  rw [← Spec.map_comp, ← Spec.map_comp] at h3
  have h4 := Spec.map_injective h3
  have E : ∀ b : B, θ.hom (coord φ i b) = θ.hom (coord φ j b) := fun b => by
    have := congrArg (fun f : CommRingCat.of B ⟶ CommRingCat.of k => f.hom b) h4
    simpa using this
  exact eq_of_apply_coord_eq φ θ.hom E
theorem

exists_sections_injective_of_tensorProduct_algEquiv_pi

L163 ↗
AlgebraicGeometry.SmoothProperCurve.exists_sections_injective_of_tensorProduct_algEquiv_pi
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open AlgebraicGeometry.SmoothProperCurve.SplitSectionsImpl in
Lean source · full declaration
theorem
  _root_.AlgebraicGeometry.SmoothProperCurve.exists_sections_injective_of_tensorProduct_algEquiv_pi
    (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (R₀ : Type u) [CommRing R₀] [Algebra R R₀]
    (B : Type u) [CommRing B] [Algebra R₀ B]
    (ι : Spec (CommRingCat.of B) ⟶ pullback c (specMap R R₀)) [IsClosedImmersion ι]
    (hι : ι ≫ baseChange R c R₀ = specMap R₀ B)
    (R' : Type u) [CommRing R'] [Algebra R R'] [Algebra R₀ R'] [IsScalarTower R R₀ R']
    (d : ℕ) (φ : (R' ⊗[R₀] B) ≃ₐ[R'] (Fin d → R')) :
    ∃ σ : Fin d → SchemeHomOver (𝟙 (Spec (CommRingCat.of R'))) (baseChange R c R'),
      ∀ (k : Type u) [Field k] (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R')),
        Function.Injective fun i => s ≫ (σ i).1 :=
  ⟨fun m => sec c ι hι φ m, fun k _ s => sec_injective c ι hι φ k s⟩

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