Local isomorphisms

A ring homomorphism is a local isomorphism if source locally (in the geometric sense) it is a standard open immersion.

Main declarations

• Algebra.IsLocalIso: The class of algebras that are locally standard open immersions.

We show that local isomorphisms are local, stable under composition and base change.

Implementation note

Most results in this file follow purely formally from the corresponding property of standard open immersion. We could use the RingHom.Locally API to obtain them, but it would yield results with less universe generality and we would have to replace CommSemiring by CommRing. In the future, we may consider refactoring the API for RingHom properties to allow for also treating properties of CommSemirings and then simplify the proofs in this file.

class Algebra.IsLocalIso (R : Type u_1) (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] : Prop

An R-algebra S is a local isomorphism if source locally (in the geometric sense), it is a standard open immersion.

• exists_notMem_isStandardOpenImmersion (q : Ideal S) [q.IsPrime] : ∃ g ∉ q, IsStandardOpenImmersion R (Localization.Away g)

theorem Algebra.isLocalIso_iff (R : Type u_1) (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] : IsLocalIso R S ↔ ∀ (q : Ideal S) [q.IsPrime], ∃ g ∉ q, IsStandardOpenImmersion R (Localization.Away g)

theorem Algebra.IsLocalIso.span_isStandardOpenImmersion_eq_top (R : Type u_1) (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] [IsLocalIso R S] : Ideal.span {g : S | IsStandardOpenImmersion R (Localization.Away g)} = ⊤

theorem Algebra.IsLocalIso.iff_span_isStandardOpenImmersion_eq_top {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] : IsLocalIso R S ↔ Ideal.span {g : S | IsStandardOpenImmersion R (Localization.Away g)} = ⊤

@[instance 100]

instance Algebra.IsLocalIso.instOfIsStandardOpenImmersion {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] [IsStandardOpenImmersion R S] : IsLocalIso R S

theorem Algebra.IsLocalIso.of_span_range_eq_top {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] {ι : Type u_3} (f : ι → S) (h : Ideal.span (Set.range f) = ⊤) (T : ι → Type u_4) [(i : ι) → CommSemiring (T i)] [(i : ι) → Algebra R (T i)] [(i : ι) → Algebra S (T i)] [∀ (i : ι), IsScalarTower R S (T i)] [∀ (i : ι), IsLocalization.Away (f i) (T i)] [∀ (i : ι), IsLocalIso R (T i)] : IsLocalIso R S

theorem Algebra.IsLocalIso.of_span_eq_top {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] {s : Set S} (h : Ideal.span s = ⊤) : (∀ x ∈ s, IsLocalIso R (Localization.Away x)) → IsLocalIso R S

theorem Algebra.IsLocalIso.pi_of_finite {ι : Type u_3} (R : Type u_4) (S : ι → Type u_5) [CommSemiring R] [(i : ι) → CommRing (S i)] [(i : ι) → Algebra R (S i)] [Finite ι] [∀ (i : ι), IsLocalIso R (S i)] : IsLocalIso R ((i : ι) → S i)

theorem Algebra.IsLocalIso.trans (R : Type u_1) (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (T : Type u_3) [CommSemiring T] [Algebra S T] [Algebra R T] [IsScalarTower R S T] [IsLocalIso R S] [IsLocalIso S T] : IsLocalIso R T

Local isomorphisms are stable under composition.

theorem Algebra.IsLocalIso.of_algEquiv {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] {T : Type u_3} [CommSemiring T] [Algebra R T] (e : S ≃ₐ[R] T) [IsLocalIso R S] : IsLocalIso R T

theorem Algebra.IsLocalIso.iff_of_algEquiv {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] {T : Type u_3} [CommSemiring T] [Algebra R T] (e : S ≃ₐ[R] T) : IsLocalIso R S ↔ IsLocalIso R T

instance Algebra.IsLocalIso.instTensorProduct {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (T : Type u_3) [CommSemiring T] [Algebra R T] [IsLocalIso R S] : IsLocalIso T (TensorProduct R T S)