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.
class
Algebra.IsStandardOpenImmersion
(R : Type u_4)
(S : Type u_5)
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
:
A standard open immersion is one that is a localization map away from some element.
- exists_away : ∃ (r : R), IsLocalization.Away r S
Instances
theorem
Algebra.isStandardOpenImmersion_iff
(R : Type u_4)
(S : Type u_5)
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
:
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]
:
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)
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))
:
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]
:
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)
:
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'
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]
:
theorem
RingHom.IsStandardOpenImmersion.toAlgebra
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
{f : R →+* S}
(hf : f.IsStandardOpenImmersion)
:
theorem
RingHom.IsStandardOpenImmersion.of_bijective
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
{f : R →+* S}
(hf : Function.Bijective ⇑f)
:
A bijective ring map is a standard open immersion.
The identity map of a ring is a standard open immersion.
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.
theorem
RingHom.IsStandardOpenImmersion.containsIdentities :
ContainsIdentities fun {R S : Type u} [CommRing R] [CommRing S] => IsStandardOpenImmersion
theorem
RingHom.IsStandardOpenImmersion.stableUnderComposition :
StableUnderComposition fun {R S : Type u} [CommRing R] [CommRing S] => IsStandardOpenImmersion
theorem
RingHom.IsStandardOpenImmersion.respectsIso :
RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => IsStandardOpenImmersion
theorem
RingHom.IsStandardOpenImmersion.isStableUnderBaseChange :
IsStableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => IsStandardOpenImmersion
theorem
RingHom.IsStandardOpenImmersion.holdsForLocalizationAway :
HoldsForLocalizationAway fun {R S : Type u} [CommRing R] [CommRing S] => IsStandardOpenImmersion