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.

exists_away : ∃ (r : R), IsLocalization.Away r S

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.instIsStandardOpenImmersionAway {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.instIsStandardOpenImmersionTensorProduct {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

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

f.IsStandardOpenImmersion = Algebra.IsStandardOpenImmersion R S

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

Documentation

Mathlib.RingTheory.RingHom.OpenImmersion

Standard Open Immersion #