Local subrings of fields

Main results

• 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)

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

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.ext_iff {R : Type u_1} {inst✝ : CommRing R} {x y : LocalSubring R} : x = y ↔ x.toSubring = y.toSubring

theorem LocalSubring.toSubring_injective {R : Type u_1} [CommRing R] : Function.Injective 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 = { toSubring := S.toSubring.copy s hs, isLocalRing := ⋯ }

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 = { toSubring := Subring.map f s.toSubring, isLocalRing := ⋯ }

@[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) : (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 ring homomorphism from a local ring as a LocalSubring.

Equations

• LocalSubring.range f = (LocalSubring.map f { toSubring := ⊤, isLocalRing := ⋯ }).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) : (range f).toSubring = (Subring.map f ⊤).copy (Set.range ⇑f) ⋯

@[instance_reducible]

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.

Equations

• One or more equations did not get rendered due to their size.

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 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 ≤ (ofPrime A P).toSubring

@[instance_reducible]

noncomputable instance LocalSubring.instAlgebraSubtypeMemSubringToSubringOfPrime {K : Type u_3} [Field K] (A : Subring K) (P : Ideal ↥A) [P.IsPrime] : Algebra ↥A ↥(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) (↥(ofPrime A P).toSubring) K

noncomputable def LocalSubring.ofPrimeEquiv {K : Type u_3} [Field K] (A : Subring K) (P : Ideal ↥A) [P.IsPrime] : Localization.AtPrime P ≃ₐ[↥A] ↥(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 (↥(ofPrime A P).toSubring) P