CommAlgPrincipal.lean

def commAlgPrincipalLocalization {A : Type u} [CommRing A]
    (R : CommAlgCat.{v} A) (d : R) : CommAlgCat.{v} A

def commAlgPrimeLocalization {A : Type u} [CommRing A]
    (S : CommAlgCat.{v} A) (p : Ideal S) [p.IsPrime] : CommAlgCat.{v} A

def commAlgContractionIdeal {A : Type u} [CommRing A]
    (R S : CommAlgCat.{v} A) (f : R →+* S) (p : Ideal S) : Ideal R

def commAlgPrincipalCoefficientMap {A : Type u} [CommRing A]
    (R : CommAlgCat.{v} A) (d : R) : R →+* commAlgPrincipalLocalization R d

def commAlgPrimeCoefficientMap {A : Type u} [CommRing A]
    (S : CommAlgCat.{v} A) (p : Ideal S) [p.IsPrime] :
    S →+* commAlgPrimeLocalization S p

def commAlgPrincipalToPrimeMap {A : Type u} [CommRing A]
    (R S : CommAlgCat.{v} A) (f : R →+* S) (d : R) (p : Ideal S) [p.IsPrime]
    (h : d ∉ commAlgContractionIdeal R S f p) :
    commAlgPrincipalLocalization R d →+* commAlgPrimeLocalization S p

theorem commAlgPrincipalToPrimeMap_comp_coefficient {A : Type u} [CommRing A]
    (R S : CommAlgCat.{v} A) (f : R →+* S) (d : R) (p : Ideal S) [p.IsPrime]
    (h : d ∉ commAlgContractionIdeal R S f p) :
    (commAlgPrincipalToPrimeMap R S f d p h).comp
        (commAlgPrincipalCoefficientMap R d) =
      (commAlgPrimeCoefficientMap S p).comp f

theorem commAlgPrincipalCoefficientMap_comp_base {A : Type u} [CommRing A]
    (R : CommAlgCat.{v} A) (d : R) :
    (commAlgPrincipalCoefficientMap R d).comp (commAlgCoefficientMap R) =
      commAlgCoefficientMap (commAlgPrincipalLocalization R d)

theorem nativePrimeCoefficientMap_injective
    (S : Type v) [CommRing S] [IsDomain S] (p : Ideal S) [p.IsPrime] :
    Function.Injective (primeLocalizationCoefficientMap S p).toFun

theorem principalLocalization_injective_of_coefficient_injective
    {R : Type v} [CommRing R] (d : R) {T : Type w} [CommSemiring T]
    (j : principalLocalizationCommRingCat R d →+* T)
    (hj : Function.Injective
      (j.comp (principalLocalizationCoefficientMap R d)).toFun) :
    Function.Injective j.toFun

theorem commAlgPrincipalToPrimeMap_injective {A : Type u} [CommRing A]
    (R S : CommAlgCat.{v} A) (f : R →+* S) (d : R) (p : Ideal S) [p.IsPrime]
    (h : d ∉ commAlgContractionIdeal R S f p) [IsDomain S]
    (hf : Function.Injective f.toFun) :
    Function.Injective (commAlgPrincipalToPrimeMap R S f d p h).toFun

theorem principalCoefficientMap_comp_isUnit_of_dvd
    {R S : Type v} [CommRing R] [CommRing S]
    (f : R →+* S) (r : R) (s : S) (h : f.toFun r ∣ s) :
    IsUnit (((principalLocalizationCoefficientMap S s).comp f).toFun r)

def commAlgPrincipalTransitionMap {A : Type u} [CommRing A]
    (R S : CommAlgCat.{v} A) (f : R →+* S)
    (r : R) (s : S) (h : f.toFun r ∣ s) :
    commAlgPrincipalLocalization R r →+* commAlgPrincipalLocalization S s

theorem commAlgPrincipalTransitionMap_comp_coefficient
    {A : Type u} [CommRing A]
    (R S : CommAlgCat.{v} A) (f : R →+* S)
    (r : R) (s : S) (h : f.toFun r ∣ s) :
    (commAlgPrincipalTransitionMap R S f r s h).comp
        (commAlgPrincipalCoefficientMap R r) =
      (commAlgPrincipalCoefficientMap S s).comp f

theorem commAlgPrincipalRingHom_ext
    {A : Type u} [CommRing A] (R : CommAlgCat.{v} A) (r : R)
    {T : Type v} [CommSemiring T]
    {f g : commAlgPrincipalLocalization R r →+* T}
    (h : f.comp (commAlgPrincipalCoefficientMap R r) =
      g.comp (commAlgPrincipalCoefficientMap R r)) : f = g

theorem commAlgPrincipalToPrimeMap_naturality
    {A : Type u} [CommRing A] (R S T : CommAlgCat.{v} A)
    (f : R →+* S) (g : S →+* T) (k : R →+* T)
    (hcoeff : g.comp f = k) (r : R) (s : S) (hdiv : f.toFun r ∣ s)
    (p : Ideal T) [p.IsPrime]
    (hr : r ∉ commAlgContractionIdeal R T k p)
    (hs : s ∉ commAlgContractionIdeal S T g p) :
    (commAlgPrincipalToPrimeMap S T g s p hs).comp
        (commAlgPrincipalTransitionMap R S f r s hdiv) =
      commAlgPrincipalToPrimeMap R T k r p hr

def commAlgPrimeComapLocalization {A : Type u} [CommRing A]
    (R S : CommAlgCat.{v} A) (f : R →+* S) (p : Ideal S) [p.IsPrime] :
    CommAlgCat.{v} A

def commAlgPrimeComapCoefficientMap {A : Type u} [CommRing A]
    (R S : CommAlgCat.{v} A) (f : R →+* S) (p : Ideal S) [p.IsPrime] :
    R →+* commAlgPrimeComapLocalization R S f p

def commAlgPrimeComapMap {A : Type u} [CommRing A]
    (R S : CommAlgCat.{v} A) (f : R →+* S) (p : Ideal S) [p.IsPrime] :
    commAlgPrimeComapLocalization R S f p →+* commAlgPrimeLocalization S p

theorem commAlgPrimeComapMap_comp_coefficient {A : Type u} [CommRing A]
    (R S : CommAlgCat.{v} A) (f : R →+* S) (p : Ideal S) [p.IsPrime] :
    (commAlgPrimeComapMap R S f p).comp (commAlgPrimeComapCoefficientMap R S f p) =
      (commAlgPrimeCoefficientMap S p).comp f

theorem commAlgPrimeCoefficientMap_injective {A : Type u} [CommRing A]
    (S : CommAlgCat.{v} A) [IsDomain S] (p : Ideal S) [p.IsPrime] :
    Function.Injective (commAlgPrimeCoefficientMap S p).toFun

theorem commAlgPrimeCoefficientMap_comp_isUnit {A : Type u} [CommRing A]
    (R S : CommAlgCat.{v} A) (f : R →+* S) (d : R) (p : Ideal S) [p.IsPrime]
    (h : d ∉ commAlgContractionIdeal R S f p) :
    IsUnit (((commAlgPrimeCoefficientMap S p).comp f).toFun d)

def commAlgPrincipalLift {A : Type u} [CommRing A]
    (R T : CommAlgCat.{v} A) (f : R →+* T) (d : R)
    (h : IsUnit (f.toFun d)) : commAlgPrincipalLocalization R d →+* T

theorem commAlgPrincipalLift_comp_coefficient {A : Type u} [CommRing A]
    (R T : CommAlgCat.{v} A) (f : R →+* T) (d : R) (h : IsUnit (f.toFun d)) :
    (commAlgPrincipalLift R T f d h).comp (commAlgPrincipalCoefficientMap R d) = f

theorem commAlgPrincipalLift_injective {A : Type u} [CommRing A]
    (R T : CommAlgCat.{v} A) (f : R →+* T) (d : R) (h : IsUnit (f.toFun d))
    (hf : Function.Injective f.toFun) :
    Function.Injective (commAlgPrincipalLift R T f d h).toFun

theorem commAlgPrincipalLift_eq_toPrime {A : Type u} [CommRing A]
    (R S : CommAlgCat.{v} A) (f : R →+* S) (d : R) (p : Ideal S) [p.IsPrime]
    (h : d ∉ commAlgContractionIdeal R S f p) :
    commAlgPrincipalLift R (commAlgPrimeLocalization S p)
        ((commAlgPrimeCoefficientMap S p).comp f) d
        (commAlgPrimeCoefficientMap_comp_isUnit R S f d p h) =
      commAlgPrincipalToPrimeMap R S f d p h