FiberLocalizationQuotient.lean

theorem one_tmul_eq_zero_of_mem_map
    (w : B) (hw : w ∈ p.map (algebraMap A B)) :
    (1 : p.ResidueField) ⊗ₜ[A] w = 0

theorem isUnit_algebraMap_fiber_of_notMem
    (r : A) (hr : r ∉ p) : IsUnit (algebraMap A (p.Fiber B) r)

theorem mem_iff_one_tmul_mem
    (q : Ideal B) (Q : Ideal (p.Fiber B))
    (hQq : Q.comap (Algebra.TensorProduct.includeRight
      (R := A) (A := p.ResidueField) (B := B)).toRingHom = q) (b : B) :
    b ∈ q ↔ (1 : p.ResidueField) ⊗ₜ[A] b ∈ Q

theorem quotientComposite_eq_zero
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) (Bq : Type w) [CommRing Bq] [Algebra B Bq]
    (a : A) (ha : a ∈ p) :
    ((Ideal.Quotient.mk ((p.map (algebraMap A B)).map (algebraMap B Bq))).comp
      ((algebraMap B Bq).comp (algebraMap A B))) a = 0

theorem isUnit_quotientMk_of_notMem
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) (q : Ideal B) [q.IsPrime]
    (Bq : Type w) [CommRing Bq] [Algebra B Bq] [IsLocalization.AtPrime Bq q]
    (b : B) (hb : b ∉ q) :
    IsUnit (Ideal.Quotient.mk ((p.map (algebraMap A B)).map (algebraMap B Bq))
      (algebraMap B Bq b))

def quotientMap
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) (Bq : Type w) [CommRing Bq] [Algebra B Bq] :
    A ⧸ p →+* Bq ⧸ (p.map (algebraMap A B)).map (algebraMap B Bq)

theorem quotientMap_mk
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) (Bq : Type w) [CommRing Bq] [Algebra B Bq] (a : A) :
    quotientMap p Bq (Ideal.Quotient.mk p a) =
      Ideal.Quotient.mk ((p.map (algebraMap A B)).map (algebraMap B Bq))
        (algebraMap B Bq (algebraMap A B a))

theorem quotientMap_isUnit
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p]
    (Bq : Type w) [CommRing Bq] [Algebra B Bq] [IsLocalization.AtPrime Bq q]
    (y : nonZeroDivisors (A ⧸ p)) : IsUnit (quotientMap (B := B) p Bq y)

def residueFieldMap
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p]
    (Bq : Type w) [CommRing Bq] [Algebra B Bq] [IsLocalization.AtPrime Bq q] :
    p.ResidueField →+* Bq ⧸ (p.map (algebraMap A B)).map (algebraMap B Bq)

theorem residueFieldMap_algebraMap
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p]
    (Bq : Type w) [CommRing Bq] [Algebra B Bq] [IsLocalization.AtPrime Bq q] (a : A) :
    residueFieldMap p q Bq (algebraMap A p.ResidueField a) =
      Ideal.Quotient.mk ((p.map (algebraMap A B)).map (algebraMap B Bq))
        (algebraMap B Bq (algebraMap A B a))

def localizationQuotientMap
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p]
    (Bq : Type w) [CommRing Bq] [Algebra B Bq] [IsLocalization.AtPrime Bq q] :
    p.Fiber B →+* Bq ⧸ (p.map (algebraMap A B)).map (algebraMap B Bq)

theorem localizationQuotientMap_tmul
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p]
    (Bq : Type w) [CommRing Bq] [Algebra B Bq] [IsLocalization.AtPrime Bq q]
    (x : p.ResidueField) (b : B) :
    localizationQuotientMap p q Bq (x ⊗ₜ[A] b) =
      residueFieldMap p q Bq x *
        Ideal.Quotient.mk ((p.map (algebraMap A B)).map (algebraMap B Bq))
          (algebraMap B Bq b)

theorem localizationQuotientMap_one_tmul
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p]
    (Bq : Type w) [CommRing Bq] [Algebra B Bq] [IsLocalization.AtPrime Bq q]
    (b : B) :
    localizationQuotientMap p q Bq ((1 : p.ResidueField) ⊗ₜ[A] b) =
      Ideal.Quotient.mk ((p.map (algebraMap A B)).map (algebraMap B Bq))
        (algebraMap B Bq b)

theorem localizationQuotientMap_algebraMap
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p]
    (Bq : Type w) [CommRing Bq] [Algebra B Bq] [IsLocalization.AtPrime Bq q]
    (a : A) :
    localizationQuotientMap p q Bq (algebraMap A (p.Fiber B) a) =
      Ideal.Quotient.mk ((p.map (algebraMap A B)).map (algebraMap B Bq))
        (algebraMap B Bq (algebraMap A B a))

theorem isLocalization_localizationQuotientMap
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p]
    (Q : Ideal (p.Fiber B)) [Q.IsPrime]
    (Bq : Type w) [CommRing Bq] [Algebra B Bq] [IsLocalization.AtPrime Bq q]
    (hQq : Q.comap (Algebra.TensorProduct.includeRight
      (R := A) (A := p.ResidueField) (B := B)).toRingHom = q) :
    @IsLocalization (p.Fiber B) _ Q.primeCompl
      (Bq ⧸ (p.map (algebraMap A B)).map (algebraMap B Bq)) _
      (localizationQuotientMap p q Bq).toAlgebra

theorem maximalIdeal_map_eq
    (Ap : Type w) [CommRing Ap] [Algebra A Ap] [IsLocalization.AtPrime Ap p]
    [IsLocalRing Ap] (g : Ap →+* Bq)
    (hg : g.comp (algebraMap A Ap) = (algebraMap B Bq).comp (algebraMap A B)) :
    (IsLocalRing.maximalIdeal Ap).map g =
      (p.map (algebraMap A B)).map (algebraMap B Bq)