NYLL
Module

exists_twoSidedPool_of_oneSided_of_iso.lean

Nyll.JacobianVarieties.Picard.exists_twoSidedPool_of_oneSided_of_iso
45 declarations indexed from sourceView source ↗

Module documentation

Two-sided chart-section pools from a curve automorphism

Imports8
Imported by1

Declarations

abbrev

wL

L53 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wL
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
abbrev wL : XL ⟶ XL
theorem

wL_fst

L55 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wL_fst
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
theorem wL_fst : wL hσ f ≫ pullback.fst _ _ = pullback.fst _ _ ≫ σ.hom
theorem

wL_snd

L58 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wL_snd
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
theorem wL_snd : wL hσ f ≫ bcL = bcL
theorem

hσinv

L61 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.hσinv
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
include hσ in
Lean source · statement
theorem hσinv : σ.inv ≫ c = c
abbrev

wLinv

L63 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wLinv
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
abbrev wLinv : XL ⟶ XL
theorem

wLinv_fst

L65 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wLinv_fst
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
theorem wLinv_fst : wLinv hσ f ≫ pullback.fst _ _ = pullback.fst _ _ ≫ σ.inv
theorem

wLinv_snd

L69 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wLinv_snd
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
theorem wLinv_snd : wLinv hσ f ≫ bcL = bcL
theorem

wL_wLinv

L71 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wL_wLinv
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
theorem wL_wLinv : wL hσ f ≫ wLinv hσ f = 𝟙 _
theorem

wLinv_wL

L76 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wLinv_wL
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
theorem wLinv_wL : wLinv hσ f ≫ wL hσ f = 𝟙 _
theorem

wLinv_base_wL_base

L81 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wLinv_base_wL_base
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
theorem wLinv_base_wL_base (x : ↥XL) : (wLinv hσ f).base ((wL hσ f).base x) = x
theorem

wL_base_wLinv_base

L84 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wL_base_wLinv_base
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
theorem wL_base_wLinv_base (x : ↥XL) : (wL hσ f).base ((wLinv hσ f).base x) = x
theorem

wL_base_injective

L87 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wL_base_injective
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
theorem wL_base_injective : Function.Injective (wL hσ f).base
theorem

εinf_wL

L91 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.εinf_wL
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
include hσε in
Lean source · statement
theorem εinf_wL : (sectionBaseChange (Localization.Away f) ε).1 ≫ wL hσ f =
    (sectionBaseChange (Localization.Away f) ε').1
theorem

range_εzero_eq

L102 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.range_εzero_eq
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
include hσε in
Lean source · statement
theorem range_εzero_eq : Set.range (sectionBaseChange (Localization.Away f) ε').1.base =
    (wL hσ f).base '' Set.range (sectionBaseChange (Localization.Away f) ε).1.base
theorem

w_base_mem_smoothLocus

L107 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.w_base_mem_smoothLocus
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
include hσU in
Lean source · statement
theorem w_base_mem_smoothLocus {x : ↥C} (hx : x ∈ (U : Set ↥C)) :
    σ.hom.base x ∈ (U : Set ↥C)
theorem

wL_base_mem_preimage_smoothLocus

L113 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wL_base_mem_preimage_smoothLocus
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
include hσU in
Lean source · statement
theorem wL_base_mem_preimage_smoothLocus {x : ↥XL}
    (hx : x ∈ ((pullback.fst (c) (specMap R (Localization.Away f)) ⁻¹ᵁ U : (XL).Opens) : Set ↥XL)) :
    (wL hσ f).base x ∈ ((pullback.fst (c) (specMap R (Localization.Away f)) ⁻¹ᵁ U : (XL).Opens) :
      Set ↥XL)
theorem

isClosedImmersion_εzero

L121 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.isClosedImmersion_εzero
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
theorem isClosedImmersion_εzero [IsSeparated c] :
    IsClosedImmersion (sectionBaseChange (Localization.Away f) ε').1
theorem

range_εzero_subset

L128 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.range_εzero_subset
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
include hε'U in
Lean source · statement
theorem range_εzero_subset : Set.range (sectionBaseChange (Localization.Away f) ε').1.base ⊆
    ((pullback.fst (c) (specMap R (Localization.Away f)) ⁻¹ᵁ U : (XL).Opens) : Set ↥XL)
theorem

eq_sectionFibrePoint_of_mem

L136 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.eq_sectionFibrePoint_of_mem
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
theorem eq_sectionFibrePoint_of_mem {k : Type} [Field k]
    (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of (Localization.Away f)))
    (γ : SchemeHomOver (𝟙 (Spec (CommRingCat.of (Localization.Away f)))) (bcL)) (y : ↥(pullback
      (bcL) s))
    (hy : (pullback.fst (bcL) s).base y ∈ Set.range γ.1.base) :
    y = (sectionFibrePoint γ s).1.base (IsLocalRing.closedPoint k)
abbrev

wLs

L178 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wLs
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
abbrev wLs {k : Type} [Field k]
    (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of (Localization.Away f))) :
    pullback (bcL) s ⟶ pullback (bcL) s
theorem

wLs_fst

L185 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wLs_fst
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
theorem wLs_fst {k : Type} [Field k]
    (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of (Localization.Away f))) :
    wLs hσ f s ≫ pullback.fst _ _ = pullback.fst _ _ ≫ wL hσ f
abbrev

wLsInv

L189 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wLsInv
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
abbrev wLsInv {k : Type} [Field k]
    (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of (Localization.Away f))) :
    pullback (bcL) s ⟶ pullback (bcL) s
theorem

wLsInv_fst

L196 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wLsInv_fst
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
theorem wLsInv_fst {k : Type} [Field k]
    (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of (Localization.Away f))) :
    wLsInv hσ f s ≫ pullback.fst _ _ = pullback.fst _ _ ≫ wLinv hσ f
theorem

wLsInv_wLs

L200 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wLsInv_wLs
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
theorem wLsInv_wLs {k : Type} [Field k]
    (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of (Localization.Away f))) :
    wLsInv hσ f s ≫ wLs hσ f s = 𝟙 _
theorem

wLs_base_wLsInv_base

L211 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wLs_base_wLsInv_base
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
local notation "L" => Localization.Away f
local notation "XL" => pullback (c) (specMap R (Localization.Away f))
local notation "bcL" => baseChange R (c) (Localization.Away f)
Lean source · statement
theorem wLs_base_wLsInv_base {k : Type} [Field k]
    (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of (Localization.Away f)))
    (y : ↥(pullback (bcL) s)) : (wLs hσ f s).base ((wLsInv hσ f s).base y) = y
instance

isIso_wL

L225 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.isIso_wL
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
Lean source · statement
instance isIso_wL : IsIso (wL hσ f)
theorem

range_comp_wL

L227 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.range_comp_wL
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
Lean source · statement
theorem range_comp_wL {Y : Scheme.{0}}
    (g : Y ⟶ pullback (c) (specMap R (Localization.Away f))) :
    Set.range (g ≫ wL hσ f).base = (wL hσ f).base '' Set.range g.base
theorem

wLs_fst_base

L232 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wLs_fst_base
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
Lean source · statement
theorem wLs_fst_base {k : Type} [Field k]
    (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of (Localization.Away f)))
    (y : ↥(pullback (baseChange R (c) (Localization.Away f)) s)) :
    (pullback.fst (baseChange R (c) (Localization.Away f)) s).base ((wLs hσ f s).base y) =
      (wL hσ f).base ((pullback.fst (baseChange R (c) (Localization.Away f)) s).base y)
theorem

wLsInv_fst_base

L239 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.wLsInv_fst_base
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
Lean source · statement
theorem wLsInv_fst_base {k : Type} [Field k]
    (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of (Localization.Away f)))
    (y : ↥(pullback (baseChange R (c) (Localization.Away f)) s)) :
    (pullback.fst (baseChange R (c) (Localization.Away f)) s).base ((wLsInv hσ f s).base y) =
      (wLinv hσ f).base ((pullback.fst (baseChange R (c) (Localization.Away f)) s).base y)
def

farB

L250 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.farB
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
section Far
variable {M : ℕ} (B : Fin M → Type) [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)]
Lean source · statement
def farB : Fin (M + 1) → Type
instance

farCommRing

L252 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.farCommRing
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
section Far
variable {M : ℕ} (B : Fin M → Type) [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)]
Lean source · statement
instance farCommRing : ∀ i, CommRing (farB f B i)
instance

farAlgebra

L256 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.farAlgebra
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
section Far
variable {M : ℕ} (B : Fin M → Type) [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)]
Lean source · statement
instance farAlgebra : ∀ i, Algebra (Localization.Away f) (farB f B i)
theorem

farFinite

L260 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.farFinite
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
section Far
variable {M : ℕ} (B : Fin M → Type) [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)]
Lean source · statement
theorem farFinite [∀ i, Module.Finite (Localization.Away f) (B i)] :
    ∀ i, Module.Finite (Localization.Away f) (farB f B i)
theorem

farEtale

L265 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.farEtale
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
section Far
variable {M : ℕ} (B : Fin M → Type) [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)]
Lean source · statement
theorem farEtale [∀ i, Algebra.Etale (Localization.Away f) (B i)] :
    ∀ i, Algebra.Etale (Localization.Away f) (farB f B i)
def

farDeg

L270 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.farDeg
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
section Far
variable {M : ℕ} (B : Fin M → Type) [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)]
Lean source · statement
def farDeg (deg : Fin M → ℕ) : Fin (M + 1) → ℕ
def

farφ

L272 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.farφ
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
section Far
variable {M : ℕ} (B : Fin M → Type) [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)]
Lean source · statement
def farφ (R' : Type) [CommRing R'] [Algebra (Localization.Away f) R'] (deg : Fin M → ℕ)
    (φ : ∀ i, TensorProduct (Localization.Away f) R' (B i) ≃ₐ[R'] (Fin (deg i) → R')) :
    ∀ i, TensorProduct (Localization.Away f) R' (farB f B i) ≃ₐ[R'] (Fin (farDeg deg i) → R')
def

farZ

L279 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.farZ
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
section Far
variable {M : ℕ} (B : Fin M → Type) [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)]
Lean source · statement
def farZ (ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (z : ∀ i, Spec (CommRingCat.of (B i)) ⟶ pullback (c) (specMap R (Localization.Away f))) :
    ∀ i, Spec (CommRingCat.of (farB f B i)) ⟶ pullback (c) (specMap R (Localization.Away f))
theorem

farZ_isClosedImmersion

L285 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.farZ_isClosedImmersion
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
section Far
variable {M : ℕ} (B : Fin M → Type) [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)]
omit [∀ i, Algebra (Localization.Away f) (B i)] in
Lean source · statement
theorem farZ_isClosedImmersion [IsSeparated c]
    (z : ∀ i, Spec (CommRingCat.of (B i)) ⟶ pullback (c) (specMap R (Localization.Away f)))
    [∀ i, IsClosedImmersion (z i)] : ∀ i, IsClosedImmersion (farZ hσ f B ε' z i)
theorem

farB_zero

L292 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.farB_zero
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
section Far
variable {M : ℕ} (B : Fin M → Type) [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)]
omit [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)] in
Lean source · statement
theorem farB_zero : farB f B 0 = Localization.Away f
theorem

farB_succ

L294 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.farB_succ
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
section Far
variable {M : ℕ} (B : Fin M → Type) [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)]
omit [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)] in
Lean source · statement
theorem farB_succ (j : Fin M) : farB f B j.succ = B j
theorem

farDeg_zero

L295 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.farDeg_zero
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
section Far
variable {M : ℕ} (B : Fin M → Type) [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)]
Lean source · statement
theorem farDeg_zero (deg : Fin M → ℕ) : farDeg deg 0 = 1
theorem

farDeg_succ

L296 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.farDeg_succ
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
section Far
variable {M : ℕ} (B : Fin M → Type) [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)]
Lean source · statement
theorem farDeg_succ (deg : Fin M → ℕ) (j : Fin M) :
    farDeg deg j.succ = deg j
theorem

farZ_zero

L299 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.farZ_zero
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
section Far
variable {M : ℕ} (B : Fin M → Type) [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)]
omit [∀ i, Algebra (Localization.Away f) (B i)] in
Lean source · statement
theorem farZ_zero
    (z : ∀ i, Spec (CommRingCat.of (B i)) ⟶ pullback (c) (specMap R (Localization.Away f))) :
    farZ hσ f B ε' z 0 = (sectionBaseChange (Localization.Away f) ε').1
theorem

farZ_succ

L303 ↗
JacobianVarieties.Picard.Proofs.TwoSidedPool.E9PMerge.farZ_succ
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
namespace E9PMerge
variable {R : Type} [CommRing R] {C : Scheme.{0}} {c : C ⟶ Spec (CommRingCat.of R)} {U : C.Opens}
  {ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {σ : C ≅ C} (hσ : σ.hom ≫ c = c)
  (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
  (hε'U : Set.range ε'.1.base ⊆ (U : Set C)) (f : R)
section Far
variable {M : ℕ} (B : Fin M → Type) [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)]
omit [∀ i, Algebra (Localization.Away f) (B i)] in
Lean source · statement
theorem farZ_succ
    (z : ∀ i, Spec (CommRingCat.of (B i)) ⟶ pullback (c) (specMap R (Localization.Away f)))
    (j : Fin M) : farZ hσ f B ε' z j.succ = z j ≫ wL hσ f
theorem

exists_twoSidedPool_of_oneSided_of_iso

L324 ↗
AlgebraicGeometry.RelPicard.exists_twoSidedPool_of_oneSided_of_iso
Documentation

Extend a one-sided pool by its image under the curve automorphism and the second section.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.TwoSidedPool
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve TensorProduct
noncomputable section
attribute [local instance] E9PMerge.isIso_wL
attribute [local instance] E9PMerge.farCommRing
attribute [local instance] E9PMerge.farAlgebra
attribute [local simp] E9PMerge.farB_zero
attribute [local simp] E9PMerge.farB_succ
attribute [local simp] E9PMerge.farDeg_zero
attribute [local simp] E9PMerge.farDeg_succ
attribute [local simp] E9PMerge.farZ_zero
attribute [local simp] E9PMerge.farZ_succ
open E9PMerge in
Lean source · full declaration
theorem _root_.AlgebraicGeometry.RelPicard.exists_twoSidedPool_of_oneSided_of_iso
    (R : Type) [CommRing R] {C : Scheme.{0}} (c : C ⟶ Spec (CommRingCat.of R)) (U : C.Opens)
    (ε ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (σ : C ≅ C) (hσ : σ.hom ≫ c = c)
    (hσε : ε.1 ≫ σ.hom = ε'.1) (hσU : σ.hom ⁻¹ᵁ U = U)
    [IsSeparated c] (hε'U : Set.range ε'.1.base ⊆ (U : Set C))
    (A₀ B₀ n₀ : ℕ) (f : R)
    (hfar : ∀ (k : Type) [Field k] [IsAlgClosed k] (s : Spec (CommRingCat.of k) ⟶ Spec
      (CommRingCat.of (Localization.Away f))),
      ¬ Smooth (pullback.snd (baseChange R c (Localization.Away f)) s) →
      (∀ y : ↥(pullback (baseChange R c (Localization.Away f)) s),
        y ∈ connectedComponentIn
            (((pullback.fst (baseChange R c (Localization.Away f)) s ≫ pullback.fst c (specMap R
              (Localization.Away f))) ⁻¹ᵁ U :
                (pullback (baseChange R c (Localization.Away f)) s).Opens) : Set ↥(pullback
                  (baseChange R c (Localization.Away f)) s))
            (((sectionFibrePoint (sectionBaseChange (Localization.Away f) ε) s).1).base
              (IsLocalRing.closedPoint k)) →
        (pullback.map (baseChange R c (Localization.Away f)) s (baseChange R c (Localization.Away
          f)) s
            (curveChange σ.hom hσ (specMap R (Localization.Away f))) (𝟙 _) (𝟙 _)
            ((Category.comp_id _).trans (curveChange_snd _ _ _).symm)
            ((Category.comp_id _).trans (Category.id_comp _).symm)).base y ∈
          (((pullback.fst (baseChange R c (Localization.Away f)) s ≫ pullback.fst c (specMap R
            (Localization.Away f))) ⁻¹ᵁ U :
                (pullback (baseChange R c (Localization.Away f)) s).Opens) : Set ↥(pullback
                  (baseChange R c (Localization.Away f)) s)) \
          connectedComponentIn
            (((pullback.fst (baseChange R c (Localization.Away f)) s ≫ pullback.fst c (specMap R
              (Localization.Away f))) ⁻¹ᵁ U :
                (pullback (baseChange R c (Localization.Away f)) s).Opens) : Set ↥(pullback
                  (baseChange R c (Localization.Away f)) s))
            (((sectionFibrePoint (sectionBaseChange (Localization.Away f) ε) s).1).base
              (IsLocalRing.closedPoint k))) ∧
      ((sectionFibrePoint (sectionBaseChange (Localization.Away f) ε') s).1).base
        (IsLocalRing.closedPoint k) ∈
          (((pullback.fst (baseChange R c (Localization.Away f)) s ≫ pullback.fst c (specMap R
            (Localization.Away f))) ⁻¹ᵁ U :
                (pullback (baseChange R c (Localization.Away f)) s).Opens) : Set ↥(pullback
                  (baseChange R c (Localization.Away f)) s)) \
          connectedComponentIn
            (((pullback.fst (baseChange R c (Localization.Away f)) s ≫ pullback.fst c (specMap R
              (Localization.Away f))) ⁻¹ᵁ U :
                (pullback (baseChange R c (Localization.Away f)) s).Opens) : Set ↥(pullback
                  (baseChange R c (Localization.Away f)) s))
            (((sectionFibrePoint (sectionBaseChange (Localization.Away f) ε) s).1).base
              (IsLocalRing.closedPoint k)))
    (b M : ℕ) (hM : A₀ * b ^ n₀ + B₀ < M)
    (R' : Type) [CommRing R'] [Algebra R R'] [Algebra (Localization.Away f) R'] [IsScalarTower R
      (Localization.Away f) R']
    [Module.Finite (Localization.Away f) R'] [Algebra.Etale (Localization.Away f) R']
      [Module.FaithfullyFlat (Localization.Away f) R']
    (B : Fin M → Type) [∀ i, CommRing (B i)] [∀ i, Algebra (Localization.Away f) (B i)]
    [∀ i, Module.Finite (Localization.Away f) (B i)] [∀ i, Algebra.Etale (Localization.Away f) (B
      i)]
    (deg : Fin M → ℕ) (hdeg : ∀ i, 1 ≤ deg i) (hdegb : ∀ i, deg i ≤ b)
    (φ : ∀ i, TensorProduct (Localization.Away f) R' (B i) ≃ₐ[R'] (Fin (deg i) → R'))
    (z : ∀ i, Spec (CommRingCat.of (B i)) ⟶ pullback c (specMap R (Localization.Away f)))
    [∀ i, IsClosedImmersion (z i)]
    (hz₁ : ∀ i, z i ≫ baseChange R c (Localization.Away f) = specMap (Localization.Away f) (B i))
    (hz₂ : ∀ i, Set.range (z i).base ⊆
      ((pullback.fst c (specMap R (Localization.Away f)) ⁻¹ᵁ U : (pullback c (specMap R
        (Localization.Away f))).Opens) :
        Set ↥(pullback c (specMap R (Localization.Away f)))))
    (hz₃ : Pairwise fun i j => Disjoint (Set.range (z i).base) (Set.range (z j).base))
    (hz₄ : ∀ (k : Type) [Field k] [IsAlgClosed k] (s : Spec (CommRingCat.of k) ⟶ Spec
      (CommRingCat.of (Localization.Away f)))
      (i : Fin M),
      (pullback.fst (baseChange R c (Localization.Away f)) s).base ⁻¹' Set.range (z i).base ⊆
        connectedComponentIn
          (((pullback.fst (baseChange R c (Localization.Away f)) s ≫ pullback.fst c (specMap R
            (Localization.Away f))) ⁻¹ᵁ U :
              (pullback (baseChange R c (Localization.Away f)) s).Opens) : Set ↥(pullback
                (baseChange R c (Localization.Away f)) s))
          (((sectionFibrePoint (sectionBaseChange (Localization.Away f) ε) s).1).base
            (IsLocalRing.closedPoint k)))
    (hzinf : ∀ i, Disjoint (Set.range (z i).base) (Set.range (sectionBaseChange (Localization.Away
      f) ε).1.base))
    (hzzero : ∀ i, Disjoint (Set.range (z i).base) (Set.range (sectionBaseChange (Localization.Away
      f) ε').1.base))
    (hzw : ∀ i j, Disjoint (Set.range (z i).base)
      (Set.range (z j ≫ curveChange σ.hom hσ (specMap R (Localization.Away f))).base)) :
    ∃ (b M M' : ℕ)
      (_ : A₀ * b ^ n₀ + B₀ < M) (_ : A₀ * b ^ n₀ + B₀ < M')
      (R' : Type) (_ : CommRing R') (_ : Algebra R R')
      (_ : Algebra (Localization.Away f) R') (_ : IsScalarTower R (Localization.Away f) R')
      (_ : Module.Finite (Localization.Away f) R') (_ : Algebra.Etale (Localization.Away f) R')
      (_ : Module.FaithfullyFlat (Localization.Away f) R')
      (B : Fin M → Type) (_ : ∀ i, CommRing (B i)) (_ : ∀ i, Algebra (Localization.Away f) (B i))
      (_ : ∀ i, Module.Finite (Localization.Away f) (B i)) (_ : ∀ i, Algebra.Etale
        (Localization.Away f) (B i))
      (deg : Fin M → ℕ) (_ : ∀ i, 1 ≤ deg i) (_ : ∀ i, deg i ≤ b)
      (_ : ∀ i, TensorProduct (Localization.Away f) R' (B i) ≃ₐ[R'] (Fin (deg i) → R'))
      (z : ∀ i, Spec (CommRingCat.of (B i)) ⟶ pullback c (specMap R (Localization.Away f)))
      (_ : ∀ i, IsClosedImmersion (z i))
      (B' : Fin M' → Type) (_ : ∀ i, CommRing (B' i)) (_ : ∀ i, Algebra (Localization.Away f) (B'
        i))
      (_ : ∀ i, Module.Finite (Localization.Away f) (B' i)) (_ : ∀ i, Algebra.Etale
        (Localization.Away f) (B' i))
      (deg' : Fin M' → ℕ) (_ : ∀ i, 1 ≤ deg' i) (_ : ∀ i, deg' i ≤ b)
      (_ : ∀ i, TensorProduct (Localization.Away f) R' (B' i) ≃ₐ[R'] (Fin (deg' i) → R'))
      (z' : ∀ i, Spec (CommRingCat.of (B' i)) ⟶ pullback c (specMap R (Localization.Away f)))
      (_ : ∀ i, IsClosedImmersion (z' i)),
      (∀ i, z i ≫ baseChange R c (Localization.Away f) = specMap (Localization.Away f) (B i)) ∧
      (∀ i, Set.range (z i).base ⊆
        ((pullback.fst c (specMap R (Localization.Away f)) ⁻¹ᵁ U : (pullback c (specMap R
          (Localization.Away f))).Opens) :
          Set ↥(pullback c (specMap R (Localization.Away f))))) ∧
      (Pairwise fun i j => Disjoint (Set.range (z i).base) (Set.range (z j).base)) ∧
      (∀ (k : Type) [Field k] [IsAlgClosed k] (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of
        (Localization.Away f)))
        (i : Fin M),
        (pullback.fst (baseChange R c (Localization.Away f)) s).base ⁻¹' Set.range (z i).base ⊆
          connectedComponentIn
            (((pullback.fst (baseChange R c (Localization.Away f)) s ≫ pullback.fst c (specMap R
              (Localization.Away f))) ⁻¹ᵁ U :
                (pullback (baseChange R c (Localization.Away f)) s).Opens) : Set ↥(pullback
                  (baseChange R c (Localization.Away f)) s))
            (((sectionFibrePoint (sectionBaseChange (Localization.Away f) ε) s).1).base
              (IsLocalRing.closedPoint k))) ∧
      (∃ j, deg' j ≤ 1) ∧
      (∀ i, z' i ≫ baseChange R c (Localization.Away f) = specMap (Localization.Away f) (B' i)) ∧
      (∀ i, Set.range (z' i).base ⊆
        ((pullback.fst c (specMap R (Localization.Away f)) ⁻¹ᵁ U : (pullback c (specMap R
          (Localization.Away f))).Opens) :
          Set ↥(pullback c (specMap R (Localization.Away f))))) ∧
      (Pairwise fun i j => Disjoint (Set.range (z' i).base) (Set.range (z' j).base)) ∧
      (∀ i j, Disjoint (Set.range (z i).base) (Set.range (z' j).base)) ∧
      (∀ (k : Type) [Field k] [IsAlgClosed k] (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of
        (Localization.Away f)))
        (i : Fin M'), ¬ Smooth (pullback.snd (baseChange R c (Localization.Away f)) s) →
        (pullback.fst (baseChange R c (Localization.Away f)) s).base ⁻¹' Set.range (z' i).base ⊆
          (((pullback.fst (baseChange R c (Localization.Away f)) s ≫ pullback.fst c (specMap R
            (Localization.Away f))) ⁻¹ᵁ U :
                (pullback (baseChange R c (Localization.Away f)) s).Opens) : Set ↥(pullback
                  (baseChange R c (Localization.Away f)) s)) \
          connectedComponentIn
            (((pullback.fst (baseChange R c (Localization.Away f)) s ≫ pullback.fst c (specMap R
              (Localization.Away f))) ⁻¹ᵁ U :
                (pullback (baseChange R c (Localization.Away f)) s).Opens) : Set ↥(pullback
                  (baseChange R c (Localization.Away f)) s))
            (((sectionFibrePoint (sectionBaseChange (Localization.Away f) ε) s).1).base
              (IsLocalRing.closedPoint k))) := by
  have hM0 : 0 < M := lt_of_le_of_lt (Nat.zero_le _) hM
  have h1b : 1 ≤ b := (hdeg ⟨0, hM0⟩).trans (hdegb ⟨0, hM0⟩)
  refine ⟨b, M, M + 1, hM, Nat.lt_succ_of_lt hM, R', inferInstance, inferInstance, inferInstance,
    inferInstance,
    inferInstance, inferInstance, inferInstance, B, inferInstance, inferInstance, inferInstance,
      inferInstance,
    deg, hdeg, hdegb, φ, z, inferInstance, farB f B, inferInstance, inferInstance, farFinite f B,
      farEtale f B, farDeg deg,
    Fin.cases le_rfl hdeg, Fin.cases h1b hdegb, farφ f B R' deg φ, farZ hσ f B ε' z,
      farZ_isClosedImmersion hσ f B z,
    hz₁, hz₂, hz₃, hz₄, ⟨0, le_rfl⟩, ?_, ?_, ?_, ?_, ?_⟩
  · refine Fin.cases ?_ (fun j => ?_)
    · change (sectionBaseChange (Localization.Away f) ε').1 ≫ _ = Spec.map (CommRingCat.ofHom
        (RingHom.id _))
      rw [(sectionBaseChange (Localization.Away f) ε').2, CommRingCat.ofHom_id, Spec.map_id]
    · change (z j ≫ wL hσ f) ≫ _ = _
      rw [Category.assoc, wL_snd]
      exact hz₁ j
  · refine Fin.cases (range_εzero_subset hε'U f) (fun j => ?_)
    change Set.range (z j ≫ wL hσ f).base ⊆ _
    rw [range_comp_wL]
    rintro _ ⟨x, hx, rfl⟩
    exact wL_base_mem_preimage_smoothLocus hσ hσU f (hz₂ j hx)
  · intro i j hij
    induction i using Fin.cases with
    | zero =>
      induction j using Fin.cases with
      | zero => exact (hij rfl).elim
      | succ j =>
        change Disjoint (Set.range (sectionBaseChange (Localization.Away f) ε').1.base) (Set.range
          (z j ≫ wL hσ f).base)
        rw [range_εzero_eq hσ hσε f, range_comp_wL]
        exact (Set.disjoint_image_iff (wL_base_injective hσ f)).2 (hzinf j).symm
    | succ i =>
      induction j using Fin.cases with
      | zero =>
        change Disjoint (Set.range (z i ≫ wL hσ f).base) (Set.range (sectionBaseChange
          (Localization.Away f) ε').1.base)
        rw [range_εzero_eq hσ hσε f, range_comp_wL]
        exact (Set.disjoint_image_iff (wL_base_injective hσ f)).2 (hzinf i)
      | succ j =>
        change Disjoint (Set.range (z i ≫ wL hσ f).base) (Set.range (z j ≫ wL hσ f).base)
        rw [range_comp_wL, range_comp_wL]
        exact (Set.disjoint_image_iff (wL_base_injective hσ f)).2 (hz₃ fun h => hij (congrArg
          Fin.succ h))
  · intro i j
    induction j using Fin.cases with
    | zero => exact hzzero i
    | succ j => exact hzw i j
  · intro k _ _ s i hns
    induction i using Fin.cases with
    | zero =>
      intro y hy
      rw [eq_sectionFibrePoint_of_mem f s (sectionBaseChange (Localization.Away f) ε') y hy]
      exact (hfar k s hns).2
    | succ j =>
      intro y hy
      change (pullback.fst (baseChange R (c) (Localization.Away f)) s).base y ∈
        Set.range (z j ≫ wL hσ f).base at hy
      rw [range_comp_wL] at hy
      obtain ⟨x, hx, hxy⟩ := hy
      have hy₀ : (pullback.fst (baseChange R (c) (Localization.Away f)) s).base ((wLsInv hσ f
        s).base y) ∈
          Set.range (z j).base := by
        rw [wLsInv_fst_base, ← hxy, wLinv_base_wL_base]
        exact hx
      have key := (hfar k s hns).1 ((wLsInv hσ f s).base y) (hz₄ k s j hy₀)
      rwa [wLs_base_wLsInv_base] at key

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