Splitting.lean

lemma AlgHom.equalizerCompRightEquiv_symm_apply (R S : Type*) [CommRing R] [CommRing S]
    [Algebra R S] {E F : Type*} (σ τ : E → F) (x : Function.Coequalizer σ τ → S) (i : F) :
    ((equalizerCompRightEquiv R S σ τ).symm x).val i = x (.mk _ _ i)

lemma AlgHom.equalizerCompRightEquiv_apply (R S : Type*) [CommRing R] [CommRing S]
    [Algebra R S] {E F : Type*} (σ τ : E → F) (x : equalizer (compRight R S σ) (compRight R S τ))
    (i : F) :
    (AlgHom.equalizerCompRightEquiv R S σ τ) x (Function.Coequalizer.mk σ τ i) =
      x.val i

lemma OfLocalizationSpan.pi (hP : OfLocalizationSpan P)
    (hPi : RespectsIso P)
    {ι : Type u} [_root_.Finite ι]
    (R : ι → Type u) (S : ι → Type u) [∀ i, CommRing (R i)]
    [∀ i, CommRing (S i)] (f : ∀ i, R i →+* S i)
    (hf : ∀ i, P (f i)) :
    P (RingHom.pi <| fun i ↦ (f i).comp <| Pi.evalRingHom R i) := by
  classical
  have := Ideal.span_single_eq_top R
  apply hP.ofIsLocalization hPi _ _ this
  rintro ⟨r, i, rfl⟩
  let i₁ : Algebra (∀ i, R i) (R i) := (Pi.evalRingHom R i).toAlgebra
  let i₂ : Algebra (∀ i, S i) (S i) := (Pi.evalRingHom S i).toAlgebra
  refine ⟨R i, S i, inferInstance, inferInstance, i₁, i₂, ?_, ?_, f i, ?_, hf i⟩
  · refine IsLocalization.away_of_isIdempotentElem ?_ (RingHom.ker_evalRingHom _ _)
      ((Pi.evalRingHom R i).surjective)
    simp [IsIdempotentElem, ← Pi.single_mul_left]
  · have : (RingHom.pi fun i ↦ (f i).comp <| Pi.evalRingHom R i)
        (Pi.single i 1) = Pi.single i 1 := by
      ext j
      simp only [Pi.single, RingHom.pi_apply, coe_comp, Function.comp_apply, Pi.evalRingHom_apply,
        Function.update, Pi.zero_apply]
      by_cases h : j = i
      · subst h
        simp
      · simp [h]
    change IsLocalization.Away
      ((RingHom.pi fun i ↦ (f i).comp <| Pi.evalRingHom R i) (Pi.single i 1)) (S i)
    rw [this]
    refine IsLocalization.away_of_isIdempotentElem ?_ (RingHom.ker_evalRingHom _ _)
      ((Pi.evalRingHom S i).surjective)
    simp [IsIdempotentElem, ← Pi.single_mul_left]
  · ext j x
    simp [RingHom.algebraMap_toAlgebra]

lemma _root_.Pi.algebraMap_instAlgebraForall_apply {ι : Type*} (A : ι → Type*)
    [∀ i, Semiring (A i)] (S : ι → Type*) [∀ i, CommSemiring (S i)]
    [∀ i, Algebra (S i) (A i)] (x : ∀ i, S i) :
    algebraMap (∀ i, S i) (∀ i, A i) x = fun i ↦ algebraMap (S i) (A i) (x i) :=
  rfl

instance (R M N : Type*) [CommRing R] [AddCommGroup M] [AddCommGroup N]
    [Module R M] [Module R N] [Module.Flat R M] [Module.Flat R N] :
    Module.Flat R (M × N)

instance {ι : Type*} (R : Type*) [CommRing R] [_root_.Finite ι]
    (M : ι → Type*) [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)]
    [∀ i, Module.Flat R (M i)] :
    Module.Flat R (∀ i, M i)

lemma CodescendsAlong.of_forall_flat {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    (hPi : RespectsIso P) (hPl : OfLocalizationSpan P) (hP : CodescendsAlong P FaithfullyFlat)
    {ι : Type u} (T : ι → Type u) [∀ i, CommRing (T i)]
    [∀ i, Algebra R (T i)] [∀ i, Module.Flat R (T i)]
    (ho : ∀ i, IsOpen <| Set.range <| PrimeSpectrum.comap (algebraMap R (T i)))
    (hunion : ⋃ i, Set.range (PrimeSpectrum.comap (algebraMap R (T i))) = Set.univ)
    (H : ∀ i, P (algebraMap (T i) (T i ⊗[R] S))) :
    P (algebraMap R S)

lemma CodescendsAlong.of_forall_exists_flat {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    (hPi : RespectsIso P) (hPl : OfLocalizationSpan P)
    (hP : CodescendsAlong P FaithfullyFlat)
    (H : ∀ (p : PrimeSpectrum R), ∃ (T : Type u) (_ : CommRing T) (_ : Algebra R T),
      p ∈ Set.range (PrimeSpectrum.comap (algebraMap R T)) ∧ Module.Flat R T ∧
      IsOpen (Set.range <| PrimeSpectrum.comap (algebraMap R T)) ∧
      P (algebraMap T (T ⊗[R] S))) :
    P (algebraMap R S)

lemma PrimeSpectrum.range_comap_tensorProduct (R S T : Type u) [CommRing R]
    [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] :
    Set.range (PrimeSpectrum.comap <| algebraMap S (S ⊗[R] T)) =
      (PrimeSpectrum.comap (algebraMap R S)) ⁻¹'
        (Set.range <| PrimeSpectrum.comap (algebraMap R T))

lemma CodescendsAlong.algHom_of_forall_exists_flat {R A B : Type u} [CommRing R]
    [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    (hPi : RespectsIso P) (hPl : OfLocalizationSpan P)
    (hP : CodescendsAlong P FaithfullyFlat)
    (f : A →ₐ[R] B)
    (H : ∀ (p : PrimeSpectrum R), ∃ (T : Type u) (_ : CommRing T) (_ : Algebra R T),
      p ∈ Set.range (PrimeSpectrum.comap (algebraMap R T)) ∧ Module.Flat R T ∧
      IsOpen (Set.range <| PrimeSpectrum.comap (algebraMap R T)) ∧
      P (Algebra.TensorProduct.map (.id T T) f).toRingHom) :
    P f.toRingHom

def AlgHom.IsSplit (f : A →ₐ[R] B) : Prop

lemma AlgHom.IsSplit.mk (f : A →ₐ[R] B) {E F : Type*} [_root_.Finite E] [_root_.Finite F]
    (eA : A ≃ₐ[R] (E → R)) (eB : B ≃ₐ[R] (F → R)) (σ : F → E)
    (h : eB.toAlgHom.comp f = (AlgHom.compRight R R σ).comp eA.toAlgHom) :
    f.IsSplit

lemma AlgHom.compRight_apply' {E F : Type*} (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    (σ : E → F) (x : F → S) :
    AlgHom.compRight R S σ x = fun i ↦ x (σ i) :=
  rfl

lemma AlgHom.IsSplit.tensorProductMap {f : A →ₐ[R] B} (hf : f.IsSplit) :
    (Algebra.TensorProduct.map (.id S S) f).IsSplit

lemma AlgHom.IsSplit.iff_of_isScalarTower
    (T : Type u) [CommRing T] [Algebra R T] [Algebra S T]
    [IsScalarTower R S T] (f : A →ₐ[R] B) :
    (Algebra.TensorProduct.map (.id T T) f).IsSplit ↔
      (Algebra.TensorProduct.map (.id T T)
        (Algebra.TensorProduct.map (.id S S) f)).IsSplit

lemma exists_isFiniteSplit [Module.Finite R A] [Algebra.Etale R A]
    (p : PrimeSpectrum R) :
    ∃ (S : Type u) (_ : CommRing S) (_ : Algebra R S),
      Module.Flat R S ∧
      IsOpenMap (PrimeSpectrum.comap (algebraMap R S)) ∧
      p ∈ Set.range (PrimeSpectrum.comap (algebraMap R S)) ∧
      Algebra.IsFiniteSplit S (S ⊗[R] A)

lemma exists_isSplit [Module.Finite R A] [Algebra.Etale R A]
    [Module.Finite R B] [Algebra.Etale R B] (f : A →ₐ[R] B)
    (p : PrimeSpectrum R) :
    ∃ (S : Type u) (_ : CommRing S) (_ : Algebra R S),
      Module.Flat R S ∧
      IsOpenMap (PrimeSpectrum.comap (algebraMap R S)) ∧
      p ∈ Set.range (PrimeSpectrum.comap (algebraMap R S)) ∧
      (TensorProduct.map (AlgHom.id S S) f).IsSplit

lemma tensorEqualizer_compRight_bijective {E F : Type*} [Finite E] [Finite F]
    (σ τ : E → F) :
    Function.Bijective ((AlgHom.compRight R R σ).tensorEqualizer S S (.compRight R R τ))

lemma TensorProduct.map_bijective_of_bijective {R S A B C D : Type*} [CommSemiring R]
    [CommSemiring S] [Algebra R S]
    [Semiring A] [Algebra R A] [Algebra S A]
    [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Algebra S C]
    [IsScalarTower R S C] [Semiring D] [Algebra R D] {f : A →ₐ[S] C} {g : B →ₐ[R] D}
    (hf : Function.Bijective f) (hg : Function.Bijective g) :
    Function.Bijective (TensorProduct.map f g)

lemma tensorEqualizer_comp_comp {R : Type*} (S : Type*) [CommRing R] [CommRing S]
    [Algebra R S] (T : Type*) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
    {A A' : Type*} {B B' : Type*} [CommRing A] [CommRing A']
    [CommRing B] [CommRing B'] [Algebra R A] [Algebra R A']
    [Algebra R B] [Algebra R B'] (f g : A' →ₐ[R] B')
    (eA : A ≃ₐ[R] A') (eB : B ≃ₐ[R] B') :
    AlgHom.tensorEqualizer S T
      (eB.symm.toAlgHom.comp (f.comp eA.toAlgHom))
      (eB.symm.toAlgHom.comp (g.comp eA.toAlgHom)) =
        AlgHom.comp
          (AlgHom.equalizerCongr
            (TensorProduct.congr .refl eA.symm)
            (TensorProduct.congr .refl eB.symm)
            (by ext <;> simp) (by ext <;> simp)).toAlgHom
          (AlgHom.comp (AlgHom.tensorEqualizer S T f g)
          (TensorProduct.congr .refl
            (AlgHom.equalizerCongr eA eB (by ext; simp) (by ext; simp))).toAlgHom) := by
  ext t
  · simp [AlgHom.tensorEqualizer_tmul_one', AlgHom.equalizerCongr_apply]
  · simp [AlgHom.tensorEqualizer_one_tmul, AlgHom.equalizerCongr_apply]

theorem tensorEqualizer_bijective_of_finite_of_etale (f g : A →ₐ[R] B)
    [Module.Finite R A] [Algebra.Etale R A] [Module.Finite R B] [Algebra.Etale R B] :
    Function.Bijective (f.tensorEqualizer R S g)