Local subrings of fields

Main result

• LocalSubring : The class of local subrings of a commutative ring.
• LocalSubring.ofPrime: The localization of a subring as a LocalSubring.

instance instIsLocalRingSubtypeMemSubringMapOfNontrivial {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Nontrivial S] (f : R →+* S) (s : Subring R) [IsLocalRing ↥s] : IsLocalRing ↥(Subring.map f s)

Equations

• ⋯ = ⋯

instance isLocalRing_top {R : Type u_1} [CommRing R] [IsLocalRing R] : IsLocalRing ↥⊤

Equations

• ⋯ = ⋯

structure LocalSubring (R : Type u_1) [CommRing R] : Type u_1

The class of local subrings of a commutative ring.

• toSubring : Subring R

  The underlying subring of a local subring.

• isLocalRing : IsLocalRing ↥self.toSubring

theorem LocalSubring.ext {R : Type u_1} {inst✝ : CommRing R} {x y : LocalSubring R} (toSubring : x.toSubring = y.toSubring) : x = y

theorem LocalSubring.toSubring_injective {R : Type u_1} [CommRing R] : Function.Injective LocalSubring.toSubring

def LocalSubring.copy {R : Type u_1} [CommRing R] (S : LocalSubring R) (s : Set R) (hs : s = ↑S.toSubring) : LocalSubring R

Copy of a local subring with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations

• S.copy s hs = LocalSubring.mk (S.toSubring.copy s hs)

def LocalSubring.map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Nontrivial S] (f : R →+* S) (s : LocalSubring R) : LocalSubring S

The image of a LocalSubring as a LocalSubring.

Equations

• LocalSubring.map f s = LocalSubring.mk (Subring.map f s.toSubring)

@[simp]

theorem LocalSubring.map_toSubring {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Nontrivial S] (f : R →+* S) (s : LocalSubring R) : (LocalSubring.map f s).toSubring = Subring.map f s.toSubring

def LocalSubring.range {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [Nontrivial S] (f : R →+* S) : LocalSubring S

The range of a ringhom from a local ring as a LocalSubring.

Equations

• LocalSubring.range f = (LocalSubring.map f (LocalSubring.mk ⊤)).copy ↑f.range ⋯

@[simp]

theorem LocalSubring.range_toSubring {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [Nontrivial S] (f : R →+* S) : (LocalSubring.range f).toSubring = (Subring.map f ⊤).copy (Set.range ⇑f) ⋯

instance LocalSubring.instPartialOrder {R : Type u_1} [CommRing R] : PartialOrder (LocalSubring R)

The domination order on local subrings. A dominates B if and only if B ≤ A (as subrings) and m_A ∩ B = m_B.

Stacks Tag 00I9

Equations

• LocalSubring.instPartialOrder = PartialOrder.mk ⋯

theorem LocalSubring.le_def {R : Type u_1} [CommRing R] {A B : LocalSubring R} : A ≤ B ↔ ∃ (h : A.toSubring ≤ B.toSubring), IsLocalHom (Subring.inclusion h)

A dominates B if and only if B ≤ A (as subrings) and m_A ∩ B = m_B.

theorem LocalSubring.toSubring_mono {R : Type u_1} [CommRing R] : Monotone LocalSubring.toSubring

noncomputable def LocalSubring.ofPrime {K : Type u_3} [Field K] (A : Subring K) (P : Ideal ↥A) [P.IsPrime] : LocalSubring K

The localization of a subring at a prime, as a local subring. Also see Localization.subalgebra.ofField

Equations

• LocalSubring.ofPrime A P = LocalSubring.range (IsLocalization.lift ⋯)

theorem LocalSubring.le_ofPrime {K : Type u_3} [Field K] (A : Subring K) (P : Ideal ↥A) [P.IsPrime] : A ≤ (LocalSubring.ofPrime A P).toSubring

noncomputable instance LocalSubring.instAlgebraSubtypeMemSubringToSubringOfPrime {K : Type u_3} [Field K] (A : Subring K) (P : Ideal ↥A) [P.IsPrime] : Algebra ↥A ↥(LocalSubring.ofPrime A P).toSubring

Equations

• LocalSubring.instAlgebraSubtypeMemSubringToSubringOfPrime A P = (Subring.inclusion ⋯).toAlgebra

instance LocalSubring.instIsScalarTowerSubtypeMemSubringToSubringOfPrime {K : Type u_3} [Field K] (A : Subring K) (P : Ideal ↥A) [P.IsPrime] : IsScalarTower (↥A) (↥(LocalSubring.ofPrime A P).toSubring) K

Equations

• ⋯ = ⋯

noncomputable def LocalSubring.ofPrimeEquiv {K : Type u_3} [Field K] (A : Subring K) (P : Ideal ↥A) [P.IsPrime] : Localization.AtPrime P ≃ₐ[↥A] ↥(LocalSubring.ofPrime A P).toSubring

The localization of a subring at a prime is indeed isomorphic to its abstract localization.

Equations

• LocalSubring.ofPrimeEquiv A P = AlgEquiv.ofInjective (IsLocalization.liftAlgHom ⋯) ⋯

instance LocalSubring.instAtPrimeSubtypeMemSubringToSubringOfPrime {K : Type u_3} [Field K] (A : Subring K) (P : Ideal ↥A) [P.IsPrime] : IsLocalization.AtPrime (↥(LocalSubring.ofPrime A P).toSubring) P

Equations

• ⋯ = ⋯