Documentation

Mathlib.RingTheory.RingHom.OpenImmersion

Standard Open Immersion #

We define the property RingHom.IsStandardOpenImmersion on ring homomorphisms: it means that the morphism is a localization map away from some element. We also define the equivalent Algebra.IsStandardOpenImmersion.

source
class Algebra.IsStandardOpenImmersion (R : Type u_4) (S : Type u_5) [CommSemiring R] [CommSemiring S] [Algebra R S] :
Prop

A standard open immersion is one that is a localization map away from some element.

Instances
    source
    theorem Algebra.isStandardOpenImmersion_iff (R : Type u_4) (S : Type u_5) [CommSemiring R] [CommSemiring S] [Algebra R S] :
    IsStandardOpenImmersion R S ↔ ∃ (r : R), IsLocalization.Away r S
    source
    instance Algebra.IsStandardOpenImmersion.instAway {R : Type u_1} [CommSemiring R] (r : R) :
    IsStandardOpenImmersion R (Localization.Away r)
    source
    theorem Algebra.IsStandardOpenImmersion.trans (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [CommSemiring S] [CommSemiring T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsStandardOpenImmersion R S] [IsStandardOpenImmersion S T] :
    IsStandardOpenImmersion R T
    source
    instance Algebra.IsStandardOpenImmersion.instTensorProduct {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommSemiring R] [CommSemiring S] [CommSemiring T] [Algebra R S] [Algebra R T] [IsStandardOpenImmersion R T] :
    IsStandardOpenImmersion S (TensorProduct R S T)
    source
    instance Algebra.IsStandardOpenImmersion.inst {R : Type u_1} [CommSemiring R] :
    IsStandardOpenImmersion R R
    source
    theorem Algebra.IsStandardOpenImmersion.of_bijective {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (h : Function.Bijective ⇑(algebraMap R S)) :
    IsStandardOpenImmersion R S
    source
    theorem Algebra.IsStandardOpenImmersion.of_algEquiv {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] {T : Type u_4} [CommSemiring T] [Algebra R T] (e : S ≃ₐ[R] T) [h : IsStandardOpenImmersion R S] :
    IsStandardOpenImmersion R T
    source
    theorem Algebra.IsStandardOpenImmersion.iff_of_algEquiv {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] {T : Type u_4} [CommSemiring T] [Algebra R T] (e : S ≃ₐ[R] T) :
    IsStandardOpenImmersion R S ↔ IsStandardOpenImmersion R T
    source
    theorem Algebra.IsStandardOpenImmersion.of_isPushout (R : Type u_1) (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (R' : Type u_4) (S' : Type u_5) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsPushout R S R' S'] [IsStandardOpenImmersion R S] :
    IsStandardOpenImmersion R' S'
    source
    def RingHom.IsStandardOpenImmersion {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) :
    Prop

    A standard open immersion is one that is a localization map away from some element.

    Equations
    Instances For
      source
      theorem RingHom.isStandardOpenImmersion_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] :
      (algebraMap R S).IsStandardOpenImmersion ↔ Algebra.IsStandardOpenImmersion R S
      source
      theorem RingHom.IsStandardOpenImmersion.algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] :
      (algebraMap R S).IsStandardOpenImmersion
      source
      theorem RingHom.IsStandardOpenImmersion.toAlgebra {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.IsStandardOpenImmersion) :
      Algebra.IsStandardOpenImmersion R S
      source
      theorem RingHom.IsStandardOpenImmersion.of_bijective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Bijective ⇑f) :
      f.IsStandardOpenImmersion

      A bijective ring map is a standard open immersion.

      source
      theorem RingHom.IsStandardOpenImmersion.id (R : Type u_1) [CommRing R] :
      (RingHom.id R).IsStandardOpenImmersion

      The identity map of a ring is a standard open immersion.

      source
      theorem RingHom.IsStandardOpenImmersion.comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] {f : R →+* S} {g : S →+* T} (hf : f.IsStandardOpenImmersion) (hg : g.IsStandardOpenImmersion) :
      (g.comp f).IsStandardOpenImmersion

      The composition of two standard open immersions is a standard open immersion.

      source
      theorem RingHom.IsStandardOpenImmersion.containsIdentities :
      ContainsIdentities fun {R S : Type u} [CommRing R] [CommRing S] => IsStandardOpenImmersion
      source
      theorem RingHom.IsStandardOpenImmersion.stableUnderComposition :
      StableUnderComposition fun {R S : Type u} [CommRing R] [CommRing S] => IsStandardOpenImmersion
      source
      theorem RingHom.IsStandardOpenImmersion.respectsIso :
      RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => IsStandardOpenImmersion
      source
      theorem RingHom.IsStandardOpenImmersion.isStableUnderBaseChange :
      IsStableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => IsStandardOpenImmersion
      source
      theorem RingHom.IsStandardOpenImmersion.holdsForLocalizationAway :
      HoldsForLocalizationAway fun {R S : Type u} [CommRing R] [CommRing S] => IsStandardOpenImmersion