structure SpringLike'.isSimple {X : Type u_1} [TopologicalSpace X] {i : X → Type u_2} [(x : X) → Field (i x)] {A : Subring ((x : X) → i x)} (hA : SpringLike' A) : Type (max (max u_1 u_2) (u_3 + 1))

Note that this is different from the definition of a simple spring in the paper. It is actually stronger!

• F : Type u_3
• field : Field self.F
• h (x : X) : i x →+* self.F
• forall_injective (x : X) : Function.Injective ⇑(self.h x)
• forall_finite (a : (x : X) → i x) : a ∈ A → {x : self.F | ∃ (x_1 : X), (self.h x_1) (a x_1) = x}.Finite

def SpringLike'.isIndex.indExtForVSuccIsSimpleOfIsSimple {X : Type u_1} [TopologicalSpace X] {i : X → Type u_2} [(x : X) → Field (i x)] {v : (p : σ(X)) → Valuation (i p.z.1) ℚ≥0} {A : Subring ((x : X) → i x)} {hA : SpringLike' A} {hAv : hA.isIndex v} {n : ℕ} (h : ⋯.isSimple) : ⋯.isSimple

Equations

• SpringLike'.isIndex.indExtForVSuccIsSimpleOfIsSimple h = { F := h.F, field := h.field, h := h.h, forall_injective := ⋯, forall_finite := ⋯ }

def SpringLike'.isIndex.indExtForVIsSimpleOfIsSimple {X : Type u_1} [TopologicalSpace X] {i : X → Type u_2} [(x : X) → Field (i x)] {v : (p : σ(X)) → Valuation (i p.z.1) ℚ≥0} {A : Subring ((x : X) → i x)} {hA : SpringLike' A} (h : hA.isSimple) (hAv : hA.isIndex v) (n : ℕ) : ⋯.isSimple

Equations

• SpringLike'.isIndex.indExtForVIsSimpleOfIsSimple h hAv n = Nat.recAuxOn n h fun (x : ℕ) (hn : ⋯.isSimple) => SpringLike'.isIndex.indExtForVSuccIsSimpleOfIsSimple hn

theorem SpringLike'.isIndex.indExtForVIsSimpleOfIsSimple_f {X : Type u_1} [TopologicalSpace X] {i : X → Type u_2} [(x : X) → Field (i x)] {v : (p : σ(X)) → Valuation (i p.z.1) ℚ≥0} {A : Subring ((x : X) → i x)} {hA : SpringLike' A} (h : hA.isSimple) (hAv : hA.isIndex v) (n : ℕ) : (indExtForVIsSimpleOfIsSimple h hAv n).F = h.F

theorem SpringLike'.isIndex.indExtForVIsSimpleOfIsSimple_h {X : Type u_1} [TopologicalSpace X] {i : X → Type u_2} [(x : X) → Field (i x)] {v : (p : σ(X)) → Valuation (i p.z.1) ℚ≥0} {A : Subring ((x : X) → i x)} {hA : SpringLike' A} (h : hA.isSimple) (hAv : hA.isIndex v) (n : ℕ) : (indExtForVIsSimpleOfIsSimple h hAv n).h ≍ h.h

theorem SpringLike'.isIndex.indExtForVIsSimpleOfIsSimple_h' {X : Type u_1} [TopologicalSpace X] {i : X → Type u_2} [(x : X) → Field (i x)] {v : (p : σ(X)) → Valuation (i p.z.1) ℚ≥0} {A : Subring ((x : X) → i x)} {hA : SpringLike' A} (h : hA.isSimple) (hAv : hA.isIndex v) (x : X) (n : ℕ) : (↑↑((indExtForVIsSimpleOfIsSimple h hAv n).h x)).toFun = ⋯.mp ∘ (↑↑(h.h x)).toFun

def SpringLike'.isIndex.iSupExtForVIsSimpleOfIsSimple {X : Type u_1} [TopologicalSpace X] {i : X → Type u_2} [(x : X) → Field (i x)] {v : (p : σ(X)) → Valuation (i p.z.1) ℚ≥0} {A : Subring ((x : X) → i x)} {hA : SpringLike' A} (h : hA.isSimple) (hAv : hA.isIndex v) : ⋯.isSimple

This corresponds to the first statement in Theorem 4 of the paper.

Equations

• SpringLike'.isIndex.iSupExtForVIsSimpleOfIsSimple h hAv = { F := h.F, field := h.field, h := h.h, forall_injective := ⋯, forall_finite := ⋯ }

theorem Subring.map_apply_eq_zero_of_pi_of_eq_of_eq_of_mem_span_of_eq {X : Type u_1} {x : X} {i : X → Type u_2} [(x : X) → CommRing (i x)] {A : Subring ((x : X) → i x)} {a b c : ↥A} {R : Type u_3} [Ring R] {h : (x : X) → i x →+* R} (hahx : (h x) (↑a x) = 0) (hbhx : (h x) (↑b x) = 0) {m : FreeCommRing (Fin 2)} (hm : m ∈ Ideal.span {FreeCommRing.of 0, FreeCommRing.of 1}) (habcm : (FreeCommRing.lift fun (i_1 : Fin 2) => if i_1 = 0 then a else b) m = c) : (h x) (↑c x) = 0

theorem Subring.map_apply_eq_map_apply_of_pi_of_eq_of_eq {X : Type u_1} {x y : X} {i : X → Type u_2} [(x : X) → CommRing (i x)] {A : Subring ((x : X) → i x)} {a b c : ↥A} {R : Type u_3} [Ring R] {h : (x : X) → i x →+* R} (hahxy : (h x) (↑a x) = (h y) (↑a y)) (hbhxy : (h x) (↑b x) = (h y) (↑b y)) {m : FreeCommRing (Fin 2)} (habcm : (FreeCommRing.lift fun (i_1 : Fin 2) => if i_1 = 0 then a else b) m = c) : (h x) (↑c x) = (h y) (↑c y)

def NonVanishingConstSetsFromInter {X : Type u_1} {i : X → Type u_2} [(x : X) → Ring (i x)] {A : Subring ((x : X) → i x)} (a b : ↥A) {R : Type u_3} [Ring R] (h : (x : X) → i x →+* R) : Set (Set X)

Equations

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

theorem NonVanishingConstSetsFromInter.sUnion_eq {X : Type u_1} {i : X → Type u_2} [(x : X) → Ring (i x)] {A : Subring ((x : X) → i x)} (a b : ↥A) {R : Type u_3} [Ring R] (h : (x : X) → i x →+* R) : ⋃₀ NonVanishingConstSetsFromInter a b h = {x : X | (h x) (↑a x) ≠ 0 ∨ (h x) (↑b x) ≠ 0}

theorem NonVanishingConstSetsFromInter.map_apply_eq_map_apply_of_mem_of_mem_of_apply_eq {X : Type u_1} {x y : X} {i : X → Type u_2} [(x : X) → CommRing (i x)] {A : Subring ((x : X) → i x)} {a b c : ↥A} {R : Type u_3} [Ring R] {h : (x : X) → i x →+* R} {s : Set X} (habhs : s ∈ NonVanishingConstSetsFromInter a b h) (hsx : x ∈ s) (hsy : y ∈ s) {m : FreeCommRing (Fin 2)} (habcm : (FreeCommRing.lift fun (i_1 : Fin 2) => if i_1 = 0 then a else b) m = c) : (h x) (↑c x) = (h y) (↑c y)

theorem NonVanishingConstSetsFromInter.map_apply_ne_zero_of_forall_mem_of_forall_ne_zero_of_apply_eq {X : Type u_1} {x : X} {i : X → Type u_2} [(x : X) → CommRing (i x)] {A : Subring ((x : X) → i x)} {a b c : ↥A} {R : Type u_3} [Ring R] {h : (x : X) → i x →+* R} (habhx : (h x) (↑a x) ≠ 0 ∨ (h x) (↑b x) ≠ 0) {f : (s : Set X) → s ∈ NonVanishingConstSetsFromInter a b h → X} (habfh : ∀ (s : Set X) (hs : s ∈ NonVanishingConstSetsFromInter a b h), f s hs ∈ s) (habcfh : ∀ (s : Set X) (hs : s ∈ NonVanishingConstSetsFromInter a b h), (h (f s hs)) (↑c (f s hs)) ≠ 0) {m : FreeCommRing (Fin 2)} (habcm : (FreeCommRing.lift fun (i_1 : Fin 2) => if i_1 = 0 then a else b) m = c) : (h x) (↑c x) ≠ 0

theorem SpringLike'.finite_nonVanishingConstSetsFromInter_of_isSimple {X : Type u_1} [TopologicalSpace X] {i : X → Type u_2} [(x : X) → Field (i x)] {A : Subring ((x : X) → i x)} (a b : ↥A) {hA : SpringLike' A} (h : hA.isSimple) : (NonVanishingConstSetsFromInter a b h.h).Finite

theorem SpringLike'.exists_mem_span_and_forall_map_apply_eq_zero_iff_and_of_isSimple {X : Type u_1} [TopologicalSpace X] {i : X → Type u_2} [(x : X) → Field (i x)] {A : Subring ((x : X) → i x)} (a b : ↥A) {hA : SpringLike' A} (h : hA.isSimple) : ∃ c ∈ Ideal.span {a, b}, ∀ (x : X), (h.h x) (↑c x) = 0 ↔ (h.h x) (↑a x) = 0 ∧ (h.h x) (↑b x) = 0

theorem SpringLike'.exists_mem_span_and_forall_apply_eq_zero_iff_and_of_isSimple {X : Type u_1} [TopologicalSpace X] {i : X → Type u_2} [(x : X) → Field (i x)] {A : Subring ((x : X) → i x)} (a b : ↥A) {hA : SpringLike' A} (h : hA.isSimple) : ∃ c ∈ Ideal.span {a, b}, ∀ (x : X), ↑c x = 0 ↔ ↑a x = 0 ∧ ↑b x = 0

theorem SpringLike'.exists_mem_span_and_forall_apply_eq_zero_iff_forall_of_isSimple {X : Type u_1} [TopologicalSpace X] {i : X → Type u_2} [(x : X) → Field (i x)] {A : Subring ((x : X) → i x)} {B : Set ↥A} (hB : B.Finite) {hA : SpringLike' A} (h : hA.isSimple) : ∃ c ∈ Ideal.span B, ∀ (x : X), ↑c x = 0 ↔ ∀ b ∈ B, ↑b x = 0

theorem SpringLike'.exists_mem_span_and_eq_biInter_of_isSimple {X : Type u_1} [TopologicalSpace X] {i : X → Type u_2} [(x : X) → Field (i x)] {A : Subring ((x : X) → i x)} {B : Set ↥A} (hB : B.Finite) {hA : SpringLike' A} (h : hA.isSimple) : ∃ c ∈ Ideal.span B, {x : X | ↑c x = 0} = ⋂ b ∈ B, {x : X | ↑b x = 0}

theorem SpringLike'.springLike_spring_isAffine_of_isSimple_of_forall_imp {X : Type u_1} [TopologicalSpace X] {i : X → Type u_2} [(x : X) → Field (i x)] {A : Subring ((x : X) → i x)} {hA : SpringLike' A} (h1 : hA.isSimple) (h2 : ∀ (a b : ↥A), (∀ (x : X), ↑b x = 0 → ↑a x = 0) → a ∈ (Ideal.span {b}).radical) : hA.springLike.spring.isAffine

This corresponds to the second statement in Theorem 4 of the paper.

theorem SpringLike'.isIndex.iSupExtForV_springLike_spring_isAffine_of_isSimple {X : Type u_1} [TopologicalSpace X] {i : X → Type u_2} [(x : X) → Field (i x)] {v : (p : σ(X)) → Valuation (i p.z.1) ℚ≥0} {A : Subring ((x : X) → i x)} {hA : SpringLike' A} (h : hA.isSimple) (hAv : hA.isIndex v) : ⋯.springLike.spring.isAffine

This corresponds to the third statement in Theorem 4 of the paper.