NYLL
Module

SmoothProperCurve_FiniteMapData_exists_baseChange.lean

Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_FiniteMapData_exists_baseChange
46 declarations indexed from sourceView source ↗

Module documentation

Base change of finite-map data on a smooth proper curve

A finite-map presentation pulls back along an algebra map with the same exponent, pulled-back charts and pulled-back coordinate functions. Finite local base extensions also preserve the generic etaleness of its level sets.

Imports5
Imported by13

Declarations

theorem

isPullback_sectionBaseChange

L52 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.SmoothProperCurve.isPullback_sectionBaseChange
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem isPullback_sectionBaseChange :
    IsPullback (sectionBaseChange R' ε).1 (specMap R R') (pullback.fst c (specMap R R')) ε.1
theorem

range_sectionBaseChange

L73 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.SmoothProperCurve.range_sectionBaseChange
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
section
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem range_sectionBaseChange :
    Set.range (sectionBaseChange R' ε).1.base =
      (pullback.fst c (specMap R R')).base ⁻¹' Set.range ε.1.base
theorem

isAffineOpen_preimage_U

L103 ↗
AlgebraicGeometry.SmoothProperCurve.FiniteMapData.isAffineOpen_preimage_U
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} (𝔉 : FiniteMapData c ε)
  (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.isAffineOpen_preimage_U :
    IsAffineOpen ((pullback.fst c (specMap R R')) ⁻¹ᵁ 𝔉.U)
theorem

isAffineOpen_preimage_V

L109 ↗
AlgebraicGeometry.SmoothProperCurve.FiniteMapData.isAffineOpen_preimage_V
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} (𝔉 : FiniteMapData c ε)
  (R' : Type u) [CommRing R'] [Algebra R R']
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
Lean source · statement
theorem _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.isAffineOpen_preimage_V :
    IsAffineOpen ((pullback.fst c (specMap R R')) ⁻¹ᵁ 𝔉.V)
theorem

preimage_U_sup_preimage_V

L115 ↗
AlgebraicGeometry.SmoothProperCurve.FiniteMapData.preimage_U_sup_preimage_V
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} (𝔉 : FiniteMapData c ε)
  (R' : Type u) [CommRing R'] [Algebra R R']
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
Lean source · statement
theorem _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.preimage_U_sup_preimage_V :
    (pullback.fst c (specMap R R')) ⁻¹ᵁ 𝔉.U ⊔ (pullback.fst c (specMap R R')) ⁻¹ᵁ 𝔉.V = ⊤
theorem

mem_preimage_U_iff

L121 ↗
AlgebraicGeometry.SmoothProperCurve.FiniteMapData.mem_preimage_U_iff
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} (𝔉 : FiniteMapData c ε)
  (R' : Type u) [CommRing R'] [Algebra R R']
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
Lean source · statement
theorem _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.mem_preimage_U_iff (x :
    ↑(pullback c (specMap R R'))) :
    x ∈ (pullback.fst c (specMap R R')) ⁻¹ᵁ 𝔉.U ↔ x ∉ Set.range (sectionBaseChange R' ε).1.base
theorem

preimage_U_inf_preimage_V_eq_basicOpen_f

L129 ↗
AlgebraicGeometry.SmoothProperCurve.FiniteMapData.preimage_U_inf_preimage_V_eq_basicOpen_f
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} (𝔉 : FiniteMapData c ε)
  (R' : Type u) [CommRing R'] [Algebra R R']
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
Lean source · statement
theorem
  _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.preimage_U_inf_preimage_V_eq_basicOpen_f
    :
    (pullback.fst c (specMap R R')) ⁻¹ᵁ 𝔉.U ⊓ (pullback.fst c (specMap R R')) ⁻¹ᵁ 𝔉.V =
      (pullback c (specMap R R')).basicOpen (((pullback.fst c (specMap R R')).app 𝔉.U).hom 𝔉.f)
theorem

preimage_U_inf_preimage_V_eq_basicOpen_g

L138 ↗
AlgebraicGeometry.SmoothProperCurve.FiniteMapData.preimage_U_inf_preimage_V_eq_basicOpen_g
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} (𝔉 : FiniteMapData c ε)
  (R' : Type u) [CommRing R'] [Algebra R R']
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
Lean source · statement
theorem
  _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.preimage_U_inf_preimage_V_eq_basicOpen_g
    :
    (pullback.fst c (specMap R R')) ⁻¹ᵁ 𝔉.U ⊓ (pullback.fst c (specMap R R')) ⁻¹ᵁ 𝔉.V =
      (pullback c (specMap R R')).basicOpen (((pullback.fst c (specMap R R')).app 𝔉.V).hom 𝔉.g)
theorem

res_app_f_mul_res_app_g

L148 ↗
AlgebraicGeometry.SmoothProperCurve.FiniteMapData.res_app_f_mul_res_app_g
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} (𝔉 : FiniteMapData c ε)
  (R' : Type u) [CommRing R'] [Algebra R R']
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
Lean source · statement
theorem _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.res_app_f_mul_res_app_g :
    ((pullback c (specMap R R')).presheaf.map (homOfLE (inf_le_left :
        (pullback.fst c (specMap R R')) ⁻¹ᵁ 𝔉.U ⊓ (pullback.fst c (specMap R R')) ⁻¹ᵁ 𝔉.V ≤
          (pullback.fst c (specMap R R')) ⁻¹ᵁ 𝔉.U)).op).hom
        (((pullback.fst c (specMap R R')).app 𝔉.U).hom 𝔉.f) *
      ((pullback c (specMap R R')).presheaf.map (homOfLE (inf_le_right :
        (pullback.fst c (specMap R R')) ⁻¹ᵁ 𝔉.U ⊓ (pullback.fst c (specMap R R')) ⁻¹ᵁ 𝔉.V ≤
          (pullback.fst c (specMap R R')) ⁻¹ᵁ 𝔉.V)).op).hom
        (((pullback.fst c (specMap R R')).app 𝔉.V).hom 𝔉.g) = 1
abbrev

sm

L190 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.sm
Documentation

The spectrum morphism induced by the extension of the base ring.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
Lean source · statement
abbrev sm : Spec (CommRingCat.of R') ⟶ Spec (CommRingCat.of R)
abbrev

p

L194 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.p
Documentation

The projection from the base changed curve to the original curve.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
Lean source · statement
abbrev p : pullback c (sm (R := R) R') ⟶ C
lemma

ofHom_algebraMap_eq

L196 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.ofHom_algebraMap_eq
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
include halg in
Lean source · statement
lemma ofHom_algebraMap_eq :
    CommRingCat.ofHom (algebraMap R Γ(C, U)) = (Scheme.ΓSpecIso (.of R)).inv ≫ c.appLE ⊤ U le_top
lemma

specMap_algebraMap_eq

L202 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.specMap_algebraMap_eq
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
include halg in
Lean source · statement
lemma specMap_algebraMap_eq :
    Spec.map (CommRingCat.ofHom (algebraMap R Γ(C, U))) = hU.isoSpec.inv ≫ U.ι ≫ c
def

Φ

L211 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.Φ
Documentation

The affine chart isomorphism identifying the base changed open with its tensor product spectrum.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
Lean source · statement
def Φ : (↑((p c R') ⁻¹ᵁ U) : Scheme.{u}) ≅ Spec (CommRingCat.of (Γ(C, U) ⊗[R] R'))
lemma

Φ_hom_comp_fst

L221 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.Φ_hom_comp_fst
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
Lean source · statement
lemma Φ_hom_comp_fst :
    (Φ c R' U hU halg).hom ≫ Spec.map (CommRingCat.ofHom
      (Algebra.TensorProduct.includeLeftRingHom : Γ(C, U) →+* Γ(C, U) ⊗[R] R')) =
      ((p c R') ∣_ U) ≫ hU.isoSpec.hom
lemma

Φ_hom_comp_snd

L230 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.Φ_hom_comp_snd
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
Lean source · statement
lemma Φ_hom_comp_snd :
    (Φ c R' U hU halg).hom ≫ Spec.map (CommRingCat.ofHom
      ((Algebra.TensorProduct.includeRight : R' →ₐ[R] Γ(C, U) ⊗[R] R') : R' →+* Γ(C, U) ⊗[R] R')) =
      ((p c R') ⁻¹ᵁ U).ι ≫ pullback.snd c (sm (R := R) R')
def

ΓIso

L240 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.ΓIso
Documentation

The section ring isomorphism from a base changed affine open to the tensor product ring.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
Lean source · statement
def ΓIso : Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) ≅ CommRingCat.of (Γ(C, U) ⊗[R] R')
lemma

ΓIso_hom_eq

L244 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.ΓIso_hom_eq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
Lean source · statement
lemma ΓIso_hom_eq : (ΓIso c R' U hU halg).hom =
    ((p c R') ⁻¹ᵁ U).topIso.inv ≫ (Φ c R' U hU halg).inv.appTop ≫
      (Scheme.ΓSpecIso (.of (Γ(C, U) ⊗[R] R'))).hom
lemma

Φ_hom_appTop_comp_inv_appTop

L250 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.Φ_hom_appTop_comp_inv_appTop
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
Lean source · statement
lemma Φ_hom_appTop_comp_inv_appTop :
    (Φ c R' U hU halg).hom.appTop ≫ (Φ c R' U hU halg).inv.appTop = 𝟙 _
lemma

presheaf_map_comp_eq

L254 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.presheaf_map_comp_eq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
Lean source · statement
lemma presheaf_map_comp_eq {X : Scheme.{u}} {A B D : X.Opens} (i : (Opposite.op A) ⟶ (Opposite.op
    B))
    (j : (Opposite.op B) ⟶ (Opposite.op D)) (k : (Opposite.op A) ⟶ (Opposite.op D)) :
    X.presheaf.map i ≫ X.presheaf.map j = X.presheaf.map k
lemma

presheaf_map_eq_of_parallel

L260 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.presheaf_map_eq_of_parallel
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
Lean source · statement
lemma presheaf_map_eq_of_parallel {X : Scheme.{u}} {V W : X.Opens} (i j : (Opposite.op V) ⟶
    (Opposite.op W)) :
    X.presheaf.map i = X.presheaf.map j
lemma

app_comp_ΓIso_hom

L265 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.app_comp_ΓIso_hom
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
Lean source · statement
lemma app_comp_ΓIso_hom :
    (p c R').app U ≫ (ΓIso c R' U hU halg).hom =
      CommRingCat.ofHom (Algebra.TensorProduct.includeLeftRingHom : Γ(C, U) →+* Γ(C, U) ⊗[R] R')
lemma

ΓIso_hom_app

L299 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.ΓIso_hom_app
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
Lean source · statement
lemma ΓIso_hom_app (a : Γ(C, U)) :
    (ΓIso c R' U hU halg).hom (((p c R').app U) a) = a ⊗ₜ[R] (1 : R')
lemma

algebraMap_comp_ΓIso_hom

L305 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.algebraMap_comp_ΓIso_hom
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
Lean source · statement
lemma algebraMap_comp_ΓIso_hom :
    (Scheme.ΓSpecIso (.of R')).inv ≫ (pullback.snd c (sm (R := R) R')).appLE ⊤ ((p c R') ⁻¹ᵁ U)
        le_top ≫
      (ΓIso c R' U hU halg).hom =
      CommRingCat.ofHom ((Algebra.TensorProduct.includeRight : R' →ₐ[R] Γ(C, U) ⊗[R] R') :
        R' →+* Γ(C, U) ⊗[R] R')
lemma

ΓIso_hom_algebraMap'

L331 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.ΓIso_hom_algebraMap'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
Lean source · statement
lemma ΓIso_hom_algebraMap' (r' : R') :
    (ΓIso c R' U hU halg).hom (((pullback.snd c (sm (R := R) R')).appLE ⊤ ((p c R') ⁻¹ᵁ U) le_top)
      ((Scheme.ΓSpecIso (.of R')).inv r')) = (1 : Γ(C, U)) ⊗ₜ[R] r'
def

bcEquiv

L349 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.bcEquiv
Documentation

The algebra equivalence identifying sections on the base changed affine open with the scalar extension.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
section algebra
variable [Algebra R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U)]
  (halg' : ∀ r' : R', algebraMap R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) r' =
    ((pullback.snd c (sm (R := R) R')).appLE ⊤ ((p c R') ⁻¹ᵁ U) le_top)
      ((Scheme.ΓSpecIso (.of R')).inv r'))
Lean source · statement
def bcEquiv : Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) ≃ₐ[R'] R' ⊗[R] Γ(C, U)
lemma

bcEquiv_app

L357 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.bcEquiv_app
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
section algebra
variable [Algebra R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U)]
  (halg' : ∀ r' : R', algebraMap R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) r' =
    ((pullback.snd c (sm (R := R) R')).appLE ⊤ ((p c R') ⁻¹ᵁ U) le_top)
      ((Scheme.ΓSpecIso (.of R')).inv r'))
Lean source · statement
lemma bcEquiv_app (a : Γ(C, U)) :
    bcEquiv c R' U hU halg halg' ((p c R').app U a) = (1 : R') ⊗ₜ[R] a
lemma

bcEquiv_symm_tmul

L362 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.bcEquiv_symm_tmul
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
section algebra
variable [Algebra R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U)]
  (halg' : ∀ r' : R', algebraMap R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) r' =
    ((pullback.snd c (sm (R := R) R')).appLE ⊤ ((p c R') ⁻¹ᵁ U) le_top)
      ((Scheme.ΓSpecIso (.of R')).inv r'))
Lean source · statement
lemma bcEquiv_symm_tmul (r' : R') (a : Γ(C, U)) :
    (bcEquiv c R' U hU halg halg').symm (r' ⊗ₜ[R] a) =
      algebraMap R' _ r' * (p c R').app U a
lemma

finite_aeval_tensor

L370 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.finite_aeval_tensor
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
section algebra
variable [Algebra R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U)]
  (halg' : ∀ r' : R', algebraMap R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) r' =
    ((pullback.snd c (sm (R := R) R')).appLE ⊤ ((p c R') ⁻¹ᵁ U) le_top)
      ((Scheme.ΓSpecIso (.of R')).inv r'))
omit hU halg in
Lean source · statement
lemma finite_aeval_tensor {Γ₀ : Type u} [CommRing Γ₀] [Algebra R Γ₀] (f : Γ₀)
    (hf : (Polynomial.aeval f : Polynomial R →ₐ[R] Γ₀).toRingHom.Finite) :
    (Polynomial.aeval ((1 : R') ⊗ₜ[R] f) : Polynomial R' →ₐ[R'] R' ⊗[R] Γ₀).toRingHom.Finite
lemma

finite_aeval_bc

L414 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.finite_aeval_bc
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
section algebra
variable [Algebra R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U)]
  (halg' : ∀ r' : R', algebraMap R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) r' =
    ((pullback.snd c (sm (R := R) R')).appLE ⊤ ((p c R') ⁻¹ᵁ U) le_top)
      ((Scheme.ΓSpecIso (.of R')).inv r'))
include hU halg halg' in
Lean source · statement
lemma finite_aeval_bc (f : Γ(C, U))
    (hf : (Polynomial.aeval f : Polynomial R →ₐ[R] Γ(C, U)).toRingHom.Finite) :
    (Polynomial.aeval ((p c R').app U f) :
      Polynomial R' →ₐ[R'] Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U)).toRingHom.Finite
def

θ

L434 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.θ
Documentation

The iterated scalar extension equivalence for sections on the base changed affine open.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
section algebra
variable [Algebra R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U)]
  (halg' : ∀ r' : R', algebraMap R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) r' =
    ((pullback.snd c (sm (R := R) R')).appLE ⊤ ((p c R') ⁻¹ᵁ U) le_top)
      ((Scheme.ΓSpecIso (.of R')).inv r'))
section levelset
variable (S : Type u) [CommRing S] [Algebra R' S] [Algebra R S] [IsScalarTower R R' S]
Lean source · statement
def θ : S ⊗[R'] Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) ≃ₐ[S] S ⊗[R] Γ(C, U)
lemma

θ_tmul

L438 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.θ_tmul
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
section algebra
variable [Algebra R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U)]
  (halg' : ∀ r' : R', algebraMap R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) r' =
    ((pullback.snd c (sm (R := R) R')).appLE ⊤ ((p c R') ⁻¹ᵁ U) le_top)
      ((Scheme.ΓSpecIso (.of R')).inv r'))
section levelset
variable (S : Type u) [CommRing S] [Algebra R' S] [Algebra R S] [IsScalarTower R R' S]
Lean source · statement
lemma θ_tmul (x : S) (y : Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U)) :
    θ c R' U hU halg halg' S (x ⊗ₜ[R'] y) =
      Algebra.TensorProduct.cancelBaseChange R R' S S Γ(C, U) (x ⊗ₜ[R'] bcEquiv c R' U hU halg
          halg' y)
lemma

θ_one_tmul_app

L444 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.θ_one_tmul_app
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
section algebra
variable [Algebra R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U)]
  (halg' : ∀ r' : R', algebraMap R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) r' =
    ((pullback.snd c (sm (R := R) R')).appLE ⊤ ((p c R') ⁻¹ᵁ U) le_top)
      ((Scheme.ΓSpecIso (.of R')).inv r'))
section levelset
variable (S : Type u) [CommRing S] [Algebra R' S] [Algebra R S] [IsScalarTower R R' S]
Lean source · statement
lemma θ_one_tmul_app (f : Γ(C, U)) :
    θ c R' U hU halg halg' S ((1 : S) ⊗ₜ[R'] (p c R').app U f) = (1 : S) ⊗ₜ[R] f
lemma

θ_tmul_one

L448 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.θ_tmul_one
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
section algebra
variable [Algebra R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U)]
  (halg' : ∀ r' : R', algebraMap R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) r' =
    ((pullback.snd c (sm (R := R) R')).appLE ⊤ ((p c R') ⁻¹ᵁ U) le_top)
      ((Scheme.ΓSpecIso (.of R')).inv r'))
section levelset
variable (S : Type u) [CommRing S] [Algebra R' S] [Algebra R S] [IsScalarTower R R' S]
Lean source · statement
lemma θ_tmul_one (s : S) :
    θ c R' U hU halg halg' S (s ⊗ₜ[R'] (1 : Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U))) =
      s ⊗ₜ[R] (1 : Γ(C, U))
lemma

ideal_map_θ

L454 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.ideal_map_θ
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
section algebra
variable [Algebra R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U)]
  (halg' : ∀ r' : R', algebraMap R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) r' =
    ((pullback.snd c (sm (R := R) R')).appLE ⊤ ((p c R') ⁻¹ᵁ U) le_top)
      ((Scheme.ΓSpecIso (.of R')).inv r'))
section levelset
variable (S : Type u) [CommRing S] [Algebra R' S] [Algebra R S] [IsScalarTower R R' S]
Lean source · statement
lemma ideal_map_θ (f : Γ(C, U)) (s : S) :
    Ideal.map (θ c R' U hU halg halg' S)
      (Ideal.span {(1 : S) ⊗ₜ[R'] (p c R').app U f - s ⊗ₜ[R'] 1}) =
      Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : Γ(C, U))}
def

levelSetEquiv

L464 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.levelSetEquiv
Documentation

The equivalence between the level set after base change and the corresponding scalar extended quotient.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
section algebra
variable [Algebra R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U)]
  (halg' : ∀ r' : R', algebraMap R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) r' =
    ((pullback.snd c (sm (R := R) R')).appLE ⊤ ((p c R') ⁻¹ᵁ U) le_top)
      ((Scheme.ΓSpecIso (.of R')).inv r'))
section levelset
variable (S : Type u) [CommRing S] [Algebra R' S] [Algebra R S] [IsScalarTower R R' S]
Lean source · statement
def levelSetEquiv (f : Γ(C, U)) (s : S) :
    (S ⊗[R'] Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) ⧸
      Ideal.span {(1 : S) ⊗ₜ[R'] (p c R').app U f - s ⊗ₜ[R'] 1}) ≃ₐ[S]
    (S ⊗[R] Γ(C, U) ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : Γ(C, U))})
lemma

levelSet_transport

L471 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.levelSet_transport
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
section algebra
variable [Algebra R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U)]
  (halg' : ∀ r' : R', algebraMap R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) r' =
    ((pullback.snd c (sm (R := R) R')).appLE ⊤ ((p c R') ⁻¹ᵁ U) le_top)
      ((Scheme.ΓSpecIso (.of R')).inv r'))
section levelset
variable (S : Type u) [CommRing S] [Algebra R' S] [Algebra R S] [IsScalarTower R R' S]
include hU halg halg' in
Lean source · statement
lemma levelSet_transport (f : Γ(C, U)) (s : S) (m : ℕ)
    (h : Module.Finite S (S ⊗[R] Γ(C, U) ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : Γ(C, U))}) ∧
      Module.Free S (S ⊗[R] Γ(C, U) ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : Γ(C, U))}) ∧
      Module.finrank S (S ⊗[R] Γ(C, U) ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : Γ(C, U))}) = m)
          :
    Module.Finite S (S ⊗[R'] Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) ⧸
        Ideal.span {(1 : S) ⊗ₜ[R'] (p c R').app U f - s ⊗ₜ[R'] 1}) ∧
      Module.Free S (S ⊗[R'] Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) ⧸
        Ideal.span {(1 : S) ⊗ₜ[R'] (p c R').app U f - s ⊗ₜ[R'] 1}) ∧
      Module.finrank S (S ⊗[R'] Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) ⧸
        Ideal.span {(1 : S) ⊗ₜ[R'] (p c R').app U f - s ⊗ₜ[R'] 1}) = m
lemma

etale_transport

L487 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.etale_transport
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
section algebra
variable [Algebra R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U)]
  (halg' : ∀ r' : R', algebraMap R' Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) r' =
    ((pullback.snd c (sm (R := R) R')).appLE ⊤ ((p c R') ⁻¹ᵁ U) le_top)
      ((Scheme.ΓSpecIso (.of R')).inv r'))
section levelset
variable (S : Type u) [CommRing S] [Algebra R' S] [Algebra R S] [IsScalarTower R R' S]
include hU halg halg' in
Lean source · statement
lemma etale_transport (f : Γ(C, U)) (s : S)
    (h : Algebra.Etale S (S ⊗[R] Γ(C, U) ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : Γ(C, U))})) :
    Algebra.Etale S (S ⊗[R'] Γ(pullback c (sm (R := R) R'), (p c R') ⁻¹ᵁ U) ⧸
        Ideal.span {(1 : S) ⊗ₜ[R'] (p c R').app U f - s ⊗ₜ[R'] 1})
lemma

isLocalHom_algebraMap_of_isIntegral

L502 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.AffineBaseChange.isLocalHom_algebraMap_of_isIntegral
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace AffineBaseChange
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R'] (U : C.Opens) (hU : IsAffineOpen U)
  [Algebra R Γ(C, U)]
  (halg : ∀ r : R, algebraMap R Γ(C, U) r = (c.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (.of R)).inv r))
omit hU in
Lean source · statement
lemma isLocalHom_algebraMap_of_isIntegral {S : Type u} [CommRing S] [IsLocalRing R] [Algebra R' S]
    [Algebra R S] [IsScalarTower R R' S] [Algebra.IsIntegral R R'] [Nontrivial S]
    [IsLocalHom (algebraMap R' S)] : IsLocalHom (algebraMap R S)
def

baseChangeData

L541 ↗
AlgebraicGeometry.SmoothProperCurve.FiniteMapData.baseChangeData
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open AlgebraicGeometry.AffineBaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} (𝔉 : FiniteMapData c ε)
  (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.baseChangeData :
    FiniteMapData (baseChange R c R') (sectionBaseChange R' ε)
lemma

baseChangeData_U

L572 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.baseChangeData_U
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open AlgebraicGeometry.AffineBaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} (𝔉 : FiniteMapData c ε)
  (R' : Type u) [CommRing R'] [Algebra R R']
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
Lean source · statement
lemma baseChangeData_U : (𝔉.baseChangeData R').U = (pullback.fst c (specMap R R'))
    ⁻¹ᵁ 𝔉.U
lemma

baseChangeData_V

L574 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.baseChangeData_V
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open AlgebraicGeometry.AffineBaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} (𝔉 : FiniteMapData c ε)
  (R' : Type u) [CommRing R'] [Algebra R R']
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
Lean source · statement
lemma baseChangeData_V : (𝔉.baseChangeData R').V = (pullback.fst c (specMap R R'))
    ⁻¹ᵁ 𝔉.V
lemma

baseChangeData_m

L576 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.baseChangeData_m
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open AlgebraicGeometry.AffineBaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} (𝔉 : FiniteMapData c ε)
  (R' : Type u) [CommRing R'] [Algebra R R']
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
Lean source · statement
lemma baseChangeData_m : (𝔉.baseChangeData R').m = 𝔉.m
lemma

baseChangeData_f

L577 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.baseChangeData_f
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open AlgebraicGeometry.AffineBaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} (𝔉 : FiniteMapData c ε)
  (R' : Type u) [CommRing R'] [Algebra R R']
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
Lean source · statement
lemma baseChangeData_f :
    (𝔉.baseChangeData R').f = ((pullback.fst c (specMap R R')).app 𝔉.U).hom 𝔉.f
theorem

levelSetsGenericallyEtale_baseChange

L580 ↗
AlgebraicGeometry.SmoothProperCurve.FiniteMapData.levelSetsGenericallyEtale_baseChange
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open AlgebraicGeometry.AffineBaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} (𝔉 : FiniteMapData c ε)
  (R' : Type u) [CommRing R'] [Algebra R R']
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
Lean source · statement
theorem
    _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.levelSetsGenericallyEtale_baseChange
    (hloc : IsLocalRing R) (hfin : Module.Finite R R')
    (h : 𝔉.LevelSetsGenericallyEtale) : (𝔉.baseChangeData R').LevelSetsGenericallyEtale
theorem

exists_baseChange

L605 ↗
AlgebraicGeometry.SmoothProperCurve.FiniteMapData.exists_baseChange
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.TensorProduct
with_weak_namespace _root_.AlgebraicCurves.Geometry.Curves.Proofs
open _root_.AlgebraicGeometry SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry
    _root_.AlgebraicGeometry.SmoothProperCurve
    SmoothProperCurve_FiniteMapData_exists_baseChange.AlgebraicGeometry.SmoothProperCurve in
with_weak_namespace SmoothProperCurve_FiniteMapData_exists_baseChange
Lean source · statement
theorem _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.exists_baseChange
    {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} (𝔉 : SmoothProperCurve.FiniteMapData c ε)
    (R' : Type u) [CommRing R'] [Algebra R R'] :
    ∃ 𝔉' : SmoothProperCurve.FiniteMapData (baseChange R c R') (sectionBaseChange R' ε),
      𝔉'.U = (pullback.fst c (specMap R R')) ⁻¹ᵁ 𝔉.U ∧ 𝔉'.V = (pullback.fst c (specMap R R')) ⁻¹ᵁ
          𝔉.V ∧
        𝔉'.m = 𝔉.m ∧
        (IsLocalRing R → Module.Finite R R' → 𝔉.LevelSetsGenericallyEtale →
            𝔉'.LevelSetsGenericallyEtale)

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