Module

preimage_range_subset_diff_connectedComponentIn_fibre_baseChange_of_not_smooth.lean

Nyll.JacobianVarieties.Picard.preimage_range_subset_diff_connectedComponentIn_fibre_baseChange_of_not_smooth

2 declarations indexed from sourceView source ↗

Module documentation

Complements of fibre components after base change

The fibre comparison preserves the section point and the inverse image of the chosen open. It transports containment outside the section's component on non-smooth fibres.

Imports11

Imported by1

Nyll.JacobianVarieties.Picard.All

theorem

exists_fibreIso_baseChange

JacobianVarieties.Picard.Proofs.ComponentComplement.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.ComponentComplement
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_diff_connectedComponentIn_fibre_baseChange_of_not_smooth

AlgebraicGeometry.RelPicard.preimage_range_subset_diff_connectedComponentIn_fibre_baseChange_of_not_smooth

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ComponentComplement
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_diff_connectedComponentIn_fibre_baseChange_of_not_smooth
    {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)),
      ¬ Smooth (pullback.snd c s) →
      (pullback.fst c s).base ⁻¹' Set.range z.base ⊆
        ((pullback.fst c s ⁻¹ᵁ U : (pullback c s).Opens) : Set ↥(pullback c s)) \
          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)),
      ¬ Smooth (pullback.snd (baseChange R c A) s') →
      (pullback.fst (baseChange R c A) s').base ⁻¹' Set.range zA.base ⊆
        ((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')) \
          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))