Algebra.FormallyUnramified.localization_base
theorem Algebra.FormallyUnramified.localization_base :
∀ {R Rₘ Sₘ : Type u} [inst : CommRing R] [inst_1 : CommRing Rₘ] [inst_2 : CommRing Sₘ],
Submonoid R →
∀ [inst_3 : Algebra R Sₘ] [inst_4 : Algebra R Rₘ] [inst_5 : Algebra Rₘ Sₘ] [inst_6 : IsScalarTower R Rₘ Sₘ]
[inst : Algebra.FormallyUnramified R Sₘ], Algebra.FormallyUnramified Rₘ Sₘ
This theorem, `Algebra.FormallyUnramified.localization_base`, states that for any three types `R`, `Rₘ`, and `Sₘ` which have Commutative Ring structures, given a submonoid of `R` and proper algebra structures on `R`, `Rₘ`, and `Sₘ` forming a scalar tower (`R` to `Rₘ` to `Sₘ`), if `R` to `Sₘ` is formally unramified, then `Rₘ` to `Sₘ` must also be formally unramified. The intended use is for copying proofs between `Formally{Unramified, Smooth, Etale}` without the need to change anything, including removing redundant arguments.
More concisely: If `R` is formally unramified over `Sₘ` and `R` has a commutative ring structure with a submonoid and proper algebra structures on `R`, `Rₘ`, and `Sₘ` forming a scalar tower, then `Rₘ` is formally unramified over `Sₘ`.
|
Algebra.FormallyUnramified.of_isLocalization
theorem Algebra.FormallyUnramified.of_isLocalization :
∀ {R Rₘ : Type u} [inst : CommRing R] [inst_1 : CommRing Rₘ] (M : Submonoid R) [inst_2 : Algebra R Rₘ]
[inst_3 : IsLocalization M Rₘ], Algebra.FormallyUnramified R Rₘ
This theorem states that for any two types `R` and `Rₘ`, which are both commutative rings, and a submonoid `M` of `R`, if `Rₘ` is a localization of `R` at `M`, then the algebra `R` to `Rₘ` is formally unramified. In the context of algebraic geometry, an algebra is said to be formally unramified if it does not introduce new 'ramification', a concept related to the branching of solutions in algebraic geometry. This theorem is asserting that this property holds for any localization, a process in algebra that simplifies the structure of the ring.
More concisely: If `R` is a commutative ring, `M` is a submonoid of `R`, and `Rₘ` is a localization of `R` at `M`, then the algebra homomorphism from `R` to `Rₘ` is formally unramified.
|