Scheme_Hom_smoothLocus_le_preimage_of_isPullback.lean

def locTensorBaseChangeEquiv (M : Type*) [AddCommGroup M] [Module S M]
    (q' : PrimeSpectrum S')
    [Algebra (Localization.AtPrime (q'.comap (algebraMap S S')).asIdeal) (Localization.AtPrime
      q'.asIdeal)]
    [IsScalarTower S (Localization.AtPrime (q'.comap (algebraMap S S')).asIdeal)
      (Localization.AtPrime q'.asIdeal)] :
    (Localization.AtPrime q'.asIdeal) ⊗[S'] (S' ⊗[S] M) ≃ₗ[Localization.AtPrime q'.asIdeal]
      (Localization.AtPrime q'.asIdeal) ⊗[Localization.AtPrime (q'.comap (algebraMap S S')).asIdeal]
        ((Localization.AtPrime (q'.comap (algebraMap S S')).asIdeal) ⊗[S] M)

theorem comap_notMem_support_of_notMem_support_baseChange [Module.Flat S S']
    (M : Type*) [AddCommGroup M] [Module S M]
    (q' : PrimeSpectrum S') (hq' : q' ∉ Module.support S' (S' ⊗[S] M)) :
    q'.comap (algebraMap S S') ∉ Module.support S M

theorem comap_mem_freeLocus_of_mem_freeLocus_baseChange [Module.Flat S S']
    (N : Type*) [AddCommGroup N] [Module S N] [Module.FinitePresentation S N]
    (q' : PrimeSpectrum S') (hq' : q' ∈ Module.freeLocus S' (S' ⊗[S] N)) :
    q'.comap (algebraMap S S') ∈ Module.freeLocus S N

theorem flat_right_baseChange {A B A' : Type u} [CommRing A] [CommRing B] [CommRing A'] [Algebra A
  B] [Algebra A A']
    [Module.Flat A A'] :
    letI : Algebra B (A' ⊗[A] B) := Algebra.TensorProduct.rightAlgebra
    Module.Flat B (A' ⊗[A] B) := by
  let : Algebra B (A' ⊗[A] B) := Algebra.TensorProduct.rightAlgebra
  let e₀ := (Algebra.TensorProduct.comm A A' B).toLinearEquiv.toAddEquiv
  have hsmul : ∀ (b : B) (z : A' ⊗[A] B), e₀ (b • z) = b • e₀ z := by
    intro b z
    induction z using TensorProduct.inductionOn with
    | add x y hx hy => rw [smul_add, map_add, hx, hy, map_add, smul_add]
    | tmul t b₀ =>
      change (Algebra.TensorProduct.comm A A' B) (((1 : A') ⊗ₜ[A] b) * (t ⊗ₜ[A] b₀)) =
        b • (Algebra.TensorProduct.comm A A' B) (t ⊗ₜ[A] b₀)
      rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul, Algebra.TensorProduct.comm_tmul,
        Algebra.TensorProduct.comm_tmul, TensorProduct.smul_tmul', smul_eq_mul]
  let e : (A' ⊗[A] B) ≃ₗ[B] (B ⊗[A] A') := { e₀ with map_smul' := hsmul }
  exact Module.Flat.of_linearEquiv e

theorem isSmoothAt_comap_of_isSmoothAt_baseChange
    {A B A' : Type u} [CommRing A] [CommRing B] [CommRing A'] [Algebra A B] [Algebra A A']
    [Algebra.FinitePresentation A B] [Module.Flat A A']
    (q' : Ideal (A' ⊗[A] B)) [q'.IsPrime] (h : Algebra.IsSmoothAt A' q') :
    Algebra.IsSmoothAt A (q'.comap (Algebra.TensorProduct.includeRight : B →ₐ[A] A' ⊗[A]
      B).toRingHom)

theorem formallySmooth_localRingHom_iff {A B : Type u} [CommRing A] [CommRing B] (φ : A →+* B)
    (q : Ideal B) [q.IsPrime] :
    (Localization.localRingHom (q.comap φ) q φ rfl).FormallySmooth ↔
      let := φ.toAlgebra; Algebra.FormallySmooth A (Localization.AtPrime q) := by
  let := φ.toAlgebra
  let alg1 : Algebra (Localization.AtPrime (q.comap φ)) (Localization.AtPrime q) :=
    (Localization.localRingHom (q.comap φ) q φ rfl).toAlgebra
  have : IsScalarTower A (Localization.AtPrime (q.comap φ)) (Localization.AtPrime q) := by
    apply IsScalarTower.of_algebraMap_eq
    intro a
    rw [RingHom.algebraMap_toAlgebra, IsScalarTower.algebraMap_apply A B (Localization.AtPrime q),
      Localization.localRingHom_to_map]
    rfl
  change Algebra.FormallySmooth (Localization.AtPrime (q.comap φ)) (Localization.AtPrime q) ↔
    Algebra.FormallySmooth A (Localization.AtPrime q)
  constructor
  · intro h
    have : Algebra.FormallySmooth A (Localization.AtPrime (q.comap φ)) :=
      Algebra.FormallySmooth.of_isLocalization (q.comap φ).primeCompl
    exact Algebra.FormallySmooth.comp A (Localization.AtPrime (q.comap φ)) (Localization.AtPrime q)
  · intro h
    exact Algebra.FormallySmooth.localization_base (q.comap φ).primeCompl

theorem mem_smoothLocus_SpecMap_iff {A B : CommRingCat.{u}} (φ : A ⟶ B)
    [LocallyOfFinitePresentation (Spec.map φ)] (q : PrimeSpectrum B) :
    (q : ↥(Spec B)) ∈ (Spec.map φ).smoothLocus ↔ letI := φ.hom.toAlgebra; Algebra.IsSmoothAt A
      q.asIdeal := by
  have : (RingHom.toMorphismProperty (fun f => RingHom.FormallySmooth f)).RespectsIso :=
    RingHom.toMorphismProperty_respectsIso_iff.mp RingHom.FormallySmooth.respectsIso
  refine Scheme.Hom.mem_smoothLocus.trans ?_
  refine ((RingHom.toMorphismProperty (fun f => RingHom.FormallySmooth f)).arrow_mk_iso_iff
    (Scheme.arrowStalkMapSpecIso φ q)).trans ?_
  exact formallySmooth_localRingHom_iff φ.hom q.asIdeal

theorem isSmoothAt_congr {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] {p q : Ideal A}
    [p.IsPrime] [q.IsPrime] (h : p = q) : Algebra.IsSmoothAt R p ↔ Algebra.IsSmoothAt R q

theorem isSmoothAt_comap_algEquiv {R A B : Type*} [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (Q : Ideal B) [Q.IsPrime]
    (h : Algebra.IsSmoothAt R Q) : Algebra.IsSmoothAt R (Q.comap e.toRingHom)

theorem isSmoothAt_comap_of_isSmoothAt_of_isPushout
    {A B A' C : Type u} [CommRing A] [CommRing B] [CommRing A'] [CommRing C]
    [Algebra A B] [Algebra A A'] [Algebra A' C] [Algebra B C] [Algebra A C]
    [IsScalarTower A A' C] [IsScalarTower A B C] [Algebra.IsPushout A A' B C]
    [Algebra.FinitePresentation A B] [Module.Flat A A']
    (Q : Ideal C) [Q.IsPrime] (h : Algebra.IsSmoothAt A' Q) :
    Algebra.IsSmoothAt A (Q.comap (algebraMap B C))

theorem smoothLocus_congr {X Y : Scheme.{u}} {f g : X ⟶ Y} (e : f = g)
    [LocallyOfFinitePresentation f] [LocallyOfFinitePresentation g] : f.smoothLocus = g.smoothLocus

theorem smoothLocus_comp_of_isOpenImmersion {X Y Z : Scheme.{u}} (f : X ⟶ Y) (k : Y ⟶ Z)
    [LocallyOfFinitePresentation f] [IsOpenImmersion k] :
    (f ≫ k).smoothLocus = f.smoothLocus

theorem smoothLocus_le_preimage_of_isPullback_of_isAffine
    {X Y X' Y' : Scheme.{u}} [IsAffine X] [IsAffine Y] [IsAffine Y']
    {f : X ⟶ Y} {f' : X' ⟶ Y'} {g : Y' ⟶ Y} {g' : X' ⟶ X}
    (h : IsPullback g' f' f g) [LocallyOfFinitePresentation f] [LocallyOfFinitePresentation f']
      [Flat g] :
    f'.smoothLocus ≤ g' ⁻¹ᵁ f.smoothLocus

theorem _root_.AlgebraicGeometry.Scheme.Hom.smoothLocus_le_preimage_of_isPullback
    {X Y X' Y' : Scheme.{u}} {f : X ⟶ Y} {f' : X' ⟶ Y'} {g : Y' ⟶ Y} {g' : X' ⟶ X}
    (h : IsPullback g' f' f g) [LocallyOfFinitePresentation f] [LocallyOfFinitePresentation f']
      [Flat g] :
    f'.smoothLocus ≤ g' ⁻¹ᵁ f.smoothLocus