Support.lean

theorem height_eq_height_under_of_faithfully_integral_over_integrallyClosed
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [IsDomain R] [IsIntegrallyClosed R] [IsDomain S]
    [Algebra R S] [Algebra.IsIntegral R S] [FaithfulSMul R S]
    (P : Ideal S) [P.IsPrime] :
    P.height = (P.under R).height

theorem contracted_height_eq_one
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [IsDomain R] [IsIntegrallyClosed R] [IsDomain S]
    [Algebra R S] [Algebra.IsIntegral R S] [FaithfulSMul R S]
    (P : Ideal S) [P.IsPrime] (hP : P.height = 1) :
    (P.under R).height = 1

theorem kaehlerDifferential_support_subset_height_ne_one_of_unramifiedAt_heightOne
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [IsDomain R] [IsIntegrallyClosed R] [IsDomain S]
    [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S]
    (hunramified :
      ∀ (p : Ideal R) [p.IsPrime], p.height = 1 →
        ∀ (P : Ideal S) [P.IsPrime] [P.LiesOver p],
          Algebra.IsUnramifiedAt R P) :
    Module.support S Ω[S⁄R] ⊆ {P | P.asIdeal.height ≠ 1}

theorem nonEtaleCotangentSupport_subset_height_ne_one_of_isEtaleAt_heightOne
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [IsDomain R] [IsIntegrallyClosed R] [IsDomain S]
    [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S]
    (hetale :
      ∀ (p : Ideal R) [p.IsPrime], p.height = 1 →
        ∀ (P : Ideal S) [P.IsPrime] [P.LiesOver p],
          Algebra.IsEtaleAt R P) :
    Module.support S Ω[S⁄R] ∪ Module.support S (Algebra.H1Cotangent R S) ⊆
      {P | P.asIdeal.height ≠ 1}