ArithmeticBoundaryEtale.lean

lemma mem_genericPoints_image_of_generalizingMap
    {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y]
    [T0Space X] [QuasiSober Y] {f : X → Y} (hf : GeneralizingMap f)
    (x : genericPoints X) : f x.1 ∈ genericPoints Y

lemma exists_irreducibleComponent_image_eq
    {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y]
    [T0Space X] [QuasiSober X] [QuasiSober Y]
    {f : X → Y} (hfc : Continuous f) (hfclosed : IsClosedMap f)
    (hfgeneral : GeneralizingMap f) (Z : Set X)
    (hZ : Z ∈ irreducibleComponents X) :
    ∃ W : Set Y, W ∈ irreducibleComponents Y ∧ f '' Z = W

lemma ker_inr_of_isPushout_of_surjective
    {R A B P : CommRingCat.{u}} {f : R ⟶ A} {g : R ⟶ B}
    {inl : A ⟶ P} {inr : B ⟶ P}
    (h : IsPushout f g inl inr) (hf : Function.Surjective f.hom) :
    RingHom.ker inr.hom = (RingHom.ker f.hom).map g.hom

lemma isRegularSystemOfParameters_map_of_flat_of_formallyUnramified_of_essFiniteType
    {R S : Type u} [CommRing R] [CommRing S]
    (f : R →+* S) [IsLocalRing R] [IsLocalRing S] [IsLocalHom f]
    (hflat : f.Flat) (hunramified : f.FormallyUnramified)
    (hfiniteType : f.EssFiniteType) {d : ℕ} (t : Fin d → R)
    (ht : AlgebraicGeometry.Scheme.IsRegularSystemOfParameters t) :
    AlgebraicGeometry.Scheme.IsRegularSystemOfParameters (fun i ↦ f (t i)) := by
  algebraize [f]
  let : Module.Flat R S := hflat
  let : Module.FaithfullyFlat R S :=
    Module.FaithfullyFlat.of_flat_of_isLocalHom
  let : Algebra.FormallyUnramified R S := hunramified
  let : Algebra.EssFiniteType R S := hfiniteType
  change AlgebraicGeometry.Scheme.IsRegularSystemOfParameters
    (fun i ↦ algebraMap R S (t i))
  have hlist : List.ofFn (fun i ↦ algebraMap R S (t i)) =
      (List.ofFn t).map (algebraMap R S) := by
    rw [List.map_ofFn]
    congr 1
  constructor
  · rw [hlist]
    exact ht.1.of_faithfullyFlat (S := S)
  · rw [hlist, ← Ideal.map_ofList, ht.2,
      Algebra.FormallyUnramified.map_maximalIdeal]

lemma Hom.ringChar_residueField_eq {X Y : Scheme.{u}} (f : Y ⟶ X) (y : Y) :
    ringChar (Y.residueField y) = ringChar (X.residueField (f y))

lemma stalkIdeal_eq_map_ideal (I : X.IdealSheafData) (x : X)
    (U : X.affineOpens) (hxU : x ∈ U.1) :
    I.stalkIdeal x =
      (I.ideal U).map (X.presheaf.germ U.1 x hxU).hom

lemma stalkIdeal_mul (I J : X.IdealSheafData) (x : X) :
    (I * J).stalkIdeal x = I.stalkIdeal x * J.stalkIdeal x

lemma stalkIdeal_finset_prod {ι : Type*} (s : Finset ι)
    (I : ι → X.IdealSheafData) (x : X) :
    (∏ i ∈ s, I i).stalkIdeal x = ∏ i ∈ s, (I i).stalkIdeal x

lemma ideal_comap_preimage_of_isAffineHom
    (I : X.IdealSheafData) (f : Y ⟶ X) [IsAffineHom f]
    (U : X.affineOpens) :
    (I.comap f).ideal ⟨f ⁻¹ᵁ U.1, U.2.preimage f⟩ =
      (I.ideal U).map (f.app U.1).hom

lemma stalkIdeal_comap_of_isAffineHom
    (I : X.IdealSheafData) (f : Y ⟶ X) [IsAffineHom f] (y : Y) :
    (I.comap f).stalkIdeal y =
      (I.stalkIdeal (f y)).map (f.stalkMap y).hom

lemma _root_.AlgebraicGeometry.Scheme.initialParameterProduct_map
    {R S : Type u} [CommRing R] [CommRing S] (φ : R →+* S)
    {d : ℕ} (t : Fin d → R) (r : ℕ) (hr : r ≤ d) :
    φ (Scheme.initialParameterProduct t r hr) =
      Scheme.initialParameterProduct (fun j ↦ φ (t j)) r hr := by
  simp [Scheme.initialParameterProduct]

lemma IsStrictNormalCrossingsAt.comap_of_finiteEtale
    (I : X.IdealSheafData) (f : Y ⟶ X) [IsFiniteEtale f] (y : Y)
    (hI : I.IsStrictNormalCrossingsAt (f y)) :
    (I.comap f).IsStrictNormalCrossingsAt y

lemma IsNormalCrossingsAt.comap_of_finiteEtale
    (I : X.IdealSheafData) (f : Y ⟶ X) [IsFiniteEtale f] (y : Y)
    (hI : I.IsNormalCrossingsAt (f y)) :
    (I.comap f).IsNormalCrossingsAt y

def comapSubschemeTo (I : X.IdealSheafData) (f : Y ⟶ X) :
    (I.comap f).subscheme ⟶ I.subscheme

instance (I : X.IdealSheafData) (f : Y ⟶ X) [IsFiniteEtale f] :
    IsFiniteEtale (I.comapSubschemeTo f)

lemma comapSubschemeTo_subschemeι (I : X.IdealSheafData) (f : Y ⟶ X) :
    I.comapSubschemeTo f ≫ I.subschemeι = (I.comap f).subschemeι ≫ f

lemma exists_irreducibleComponent_image_comapSubschemeTo_eq
    (I : X.IdealSheafData) (f : Y ⟶ X) [IsFiniteEtale f]
    (Z : Set (I.comap f).subscheme)
    (hZ : Z ∈ irreducibleComponents (I.comap f).subscheme) :
    ∃ W : Set I.subscheme,
      W ∈ irreducibleComponents I.subscheme ∧ I.comapSubschemeTo f '' Z = W

lemma exists_residueCharacteristicPoint_on_comapComponent
    (D : EffectiveCartierDivisor X) (f : Y ⟶ X) [IsFiniteEtale f]
    (q : ℕ) (hD : D.HasNormalCrossingPointOfResidueCharacteristicOnEachComponent q)
    (Z : Set (D.1.comap f).subscheme)
    (hZ : Z ∈ irreducibleComponents (D.1.comap f).subscheme) :
    ∃ y : (D.1.comap f).subscheme,
      y ∈ Z ∧
        ringChar (Y.residueField ((D.1.comap f).subschemeι y)) = q ∧
          D.IsNormalCrossingsAt (f ((D.1.comap f).subschemeι y))

lemma exists_normalCrossingPointOfResidueCharacteristic_on_comapComponent
    (D : EffectiveCartierDivisor X) (f : Y ⟶ X) [IsFiniteEtale f]
    (q : ℕ) (hD : D.HasNormalCrossingPointOfResidueCharacteristicOnEachComponent q)
    (Z : Set (D.1.comap f).subscheme)
    (hZ : Z ∈ irreducibleComponents (D.1.comap f).subscheme) :
    ∃ y : (D.1.comap f).subscheme,
      y ∈ Z ∧
        ringChar (Y.residueField ((D.1.comap f).subschemeι y)) = q ∧
          (D.1.comap f).IsNormalCrossingsAt ((D.1.comap f).subschemeι y)