NYLL
Module

preimage_range_subset_connectedComponentIn_fibre_baseChange.lean

Nyll.JacobianVarieties.Picard.preimage_range_subset_connectedComponentIn_fibre_baseChange
2 declarations indexed from sourceView source ↗

Module documentation

Connected components in fibres after base change

The fibre comparison homeomorphism carries the section point to the base-changed section. It transports the assumed containment in a connected component to the base-changed fibre.

Imports11
Imported by1

Declarations

theorem

exists_fibreIso_baseChange

L72 ↗
JacobianVarieties.Picard.Proofs.ComponentTransport.AlgebraicGeometry.RelPicard.TZETransport.exists_fibreIso_baseChange
Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ComponentTransport
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace TZETransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem exists_fibreIso_baseChange {k : Type u} [Field k]
    (x' : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of A)) :
    ∃ φ : pullback (baseChange R c A) x' ≅ pullback c (x' ≫ specMap R A),
      φ.hom ≫ pullback.snd c (x' ≫ specMap R A) = pullback.snd (baseChange R c A) x' ∧
      φ.hom ≫ pullback.fst c (x' ≫ specMap R A) =
        pullback.fst (baseChange R c A) x' ≫ pullback.fst c (specMap R A)
theorem

preimage_range_subset_connectedComponentIn_fibre_baseChange

L85 ↗
AlgebraicGeometry.RelPicard.preimage_range_subset_connectedComponentIn_fibre_baseChange
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ComponentTransport
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open AlgebraicGeometry.RelPicard.TZETransport in
with_weak_namespace _root_.AlgebraicGeometry.RelPicard
Lean source · statement
theorem preimage_range_subset_connectedComponentIn_fibre_baseChange
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (A : Type u) [CommRing A] [Algebra R A]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (U : C.Opens)
    {Z ZA : Scheme.{u}} (z : Z ⟶ C) (zA : ZA ⟶ pullback c (specMap R A))
    (hzA : Set.range (zA ≫ pullback.fst c (specMap R A)).base ⊆ Set.range z.base)
    (hzε : ∀ (k : Type u) [Field k] [IsAlgClosed k]
      (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R)),
      (pullback.fst c s).base ⁻¹' Set.range z.base ⊆
        connectedComponentIn ((pullback.fst c s ⁻¹ᵁ U : (pullback c s).Opens) : Set ↥(pullback c s))
          (((sectionFibrePoint ε s).1).base (IsLocalRing.closedPoint k))) :
    ∀ (k : Type u) [Field k] [IsAlgClosed k]
      (s' : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of A)),
      (pullback.fst (baseChange R c A) s').base ⁻¹' Set.range zA.base ⊆
        connectedComponentIn
          ((pullback.fst (baseChange R c A) s' ⁻¹ᵁ (pullback.fst c (specMap R A) ⁻¹ᵁ U) :
              (pullback (baseChange R c A) s').Opens) : Set ↥(pullback (baseChange R c A) s'))
          (((sectionFibrePoint (sectionBaseChange A ε) s').1).base
            (IsLocalRing.closedPoint k))

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