Theorems · Theorem · algebraic geometry

Algebra.IsLocalIso.of_span_range_eq_top

∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {ι : Type u_3}
  (f : ι → S),
  Ideal.span (Set.range f) = ⊤ →
    ∀ (T : ι → Type u_4) [inst_3 : (i : ι) → CommSemiring (T i)] [inst_4 : (i : ι) → Algebra R (T i)]
      [inst_5 : (i : ι) → Algebra S (T i)] [∀ (i : ι), IsScalarTower R S (T i)]
      [∀ (i : ι), IsLocalization.Away (f i) (T i)] [∀ (i : ι), Algebra.IsLocalIso R (T i)], Algebra.IsLocalIso R S

Defined in

Mathlib.RingTheory.LocalIso

Cited by

3 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraCommSemiringAlgebraAlgebraIsScalarTowerIsLocalization.AwayAlgebra.IsLocalIso