The complexification A ⊗_ℝ ℂ = A[i] of a commutative ring

Hironaka: for a preanalytic ℝ-space X = (X, 𝒪_X), "(X, 𝒪_X ⊗_ℝ ℂ) is a ℂ-local-ringed space, which will be denoted by X(ℂ)" [Hir64, Ch. 0, §1, p. 120]. Since ℂ = ℝ ⊕ ℝ i is free of rank two over ℝ, the tensor product A ⊗_ℝ ℂ of a commutative ring A (with an ℝ-structure) is the ring A[i] = {a + b i : a, b ∈ A} of Gaussian pairs with i² = -1, and it is this ring — which needs no ℝ-structure on A to be formed — that the complexification uses sectionwise: Γ(U, 𝒪_X ⊗_ℝ ℂ) = Γ(U, 𝒪_X)[i]. The identification with Mathlib's tensor product is the ℝ-algebra isomorphism tensorEquiv : Complexified A ≃ₐ[ℝ] A ⊗[ℝ] ℂ, a + b i ↦ a ⊗ 1 + b ⊗ i.

Main definitions

In the namespace Hironaka.AnalyticSpace.Complexified:

• Complexified A: the pairs ⟨re, im⟩, a commutative ring with (a + bi)(c + di) = (ac - bd) + (ad + bc) i; ofReal : A →+* Complexified A (a ↦ a + 0 i), I (0 + 1 i), I_mul_I, re_add_im; the R-algebra structure induced from one on A;
• map (f : A →+* B) : Complexified A →+* Complexified B (componentwise; functorial), mapEquiv;
• algebraMapComplex (φ : ℝ →+* A) : ℂ →+* Complexified A, c ↦ φ(Re c) + φ(Im c) i: the ℂ-structure of X(ℂ) from the ℝ-structure of X;
• norm z = z.re² + z.im² and isUnit_iff_isUnit_norm; the local-ring theorem isLocalRing_of_exists_sub_mem: if A is a local ring whose residue field is ℝ (every element is congruent to a constant φ c modulo 𝔪_A), then Complexified A is a local ring — the stalks 𝒪_{X,x} ⊗_ℝ ℂ of X(ℂ) are local because the residue fields of a preanalytic ℝ-space are ℝ; isLocalHom_map: a local homomorphism complexifies to a local homomorphism;
• tensorEquiv: the identification with A ⊗[ℝ] ℂ (the standard ℂ = ℝ[i]);
• A[i] is a finite A-module, hence Noetherian when A is.

The complexification of a space is built on this in Hironaka/AnalyticSpace/Complexify.lean.

structure AnalyticSpace.Complexified (A : Type u) : Type u

The complexification A ⊗_ℝ ℂ = A[i] of a commutative ring A, realised as Gaussian pairs a + b i (Hironaka's 𝒪_X ⊗_ℝ ℂ [Hir64, Ch. 0, §1, p. 120], sectionwise).

• re : A

  The real part.

• im : A

  The imaginary part.

theorem AnalyticSpace.Complexified.ext {A : Type u} {x y : Complexified A} (re : x.re = y.re) (im : x.im = y.im) : x = y

theorem AnalyticSpace.Complexified.ext_iff {A : Type u} {x y : Complexified A} : x = y ↔ x.re = y.re ∧ x.im = y.im

@[instance_reducible]

instance AnalyticSpace.Complexified.instZero {A : Type u} [CommRing A] : Zero (Complexified A)

Equations

• AnalyticSpace.Complexified.instZero = { zero := { re := 0, im := 0 } }

@[instance_reducible]

instance AnalyticSpace.Complexified.instOne {A : Type u} [CommRing A] : One (Complexified A)

Equations

• AnalyticSpace.Complexified.instOne = { one := { re := 1, im := 0 } }

@[instance_reducible]

instance AnalyticSpace.Complexified.instAdd {A : Type u} [CommRing A] : Add (Complexified A)

Equations

• AnalyticSpace.Complexified.instAdd = { add := fun (z w : AnalyticSpace.Complexified A) => { re := z.re + w.re, im := z.im + w.im } }

@[instance_reducible]

instance AnalyticSpace.Complexified.instNeg {A : Type u} [CommRing A] : Neg (Complexified A)

Equations

• AnalyticSpace.Complexified.instNeg = { neg := fun (z : AnalyticSpace.Complexified A) => { re := -z.re, im := -z.im } }

@[instance_reducible]

instance AnalyticSpace.Complexified.instSub {A : Type u} [CommRing A] : Sub (Complexified A)

Equations

• AnalyticSpace.Complexified.instSub = { sub := fun (z w : AnalyticSpace.Complexified A) => { re := z.re - w.re, im := z.im - w.im } }

@[instance_reducible]

instance AnalyticSpace.Complexified.instMul {A : Type u} [CommRing A] : Mul (Complexified A)

Equations

• AnalyticSpace.Complexified.instMul = { mul := fun (z w : AnalyticSpace.Complexified A) => { re := z.re * w.re - z.im * w.im, im := z.re * w.im + z.im * w.re } }

@[instance_reducible]

instance AnalyticSpace.Complexified.instSMulNat {A : Type u} [CommRing A] : SMul ℕ (Complexified A)

Equations

• AnalyticSpace.Complexified.instSMulNat = { smul := fun (n : ℕ) (z : AnalyticSpace.Complexified A) => { re := n • z.re, im := n • z.im } }

@[instance_reducible]

instance AnalyticSpace.Complexified.instSMulInt {A : Type u} [CommRing A] : SMul ℤ (Complexified A)

Equations

• AnalyticSpace.Complexified.instSMulInt = { smul := fun (n : ℤ) (z : AnalyticSpace.Complexified A) => { re := n • z.re, im := n • z.im } }

@[instance_reducible]

instance AnalyticSpace.Complexified.instNatCast {A : Type u} [CommRing A] : NatCast (Complexified A)

Equations

• AnalyticSpace.Complexified.instNatCast = { natCast := fun (n : ℕ) => { re := ↑n, im := 0 } }

@[instance_reducible]

instance AnalyticSpace.Complexified.instIntCast {A : Type u} [CommRing A] : IntCast (Complexified A)

Equations

• AnalyticSpace.Complexified.instIntCast = { intCast := fun (n : ℤ) => { re := ↑n, im := 0 } }

@[simp]

theorem AnalyticSpace.Complexified.zero_re {A : Type u} [CommRing A] : re 0 = 0

@[simp]

theorem AnalyticSpace.Complexified.zero_im {A : Type u} [CommRing A] : im 0 = 0

@[simp]

theorem AnalyticSpace.Complexified.one_re {A : Type u} [CommRing A] : re 1 = 1

@[simp]

theorem AnalyticSpace.Complexified.one_im {A : Type u} [CommRing A] : im 1 = 0

@[simp]

theorem AnalyticSpace.Complexified.add_re {A : Type u} [CommRing A] (z w : Complexified A) : (z + w).re = z.re + w.re

@[simp]

theorem AnalyticSpace.Complexified.add_im {A : Type u} [CommRing A] (z w : Complexified A) : (z + w).im = z.im + w.im

@[simp]

theorem AnalyticSpace.Complexified.neg_re {A : Type u} [CommRing A] (z : Complexified A) : (-z).re = -z.re

@[simp]

theorem AnalyticSpace.Complexified.neg_im {A : Type u} [CommRing A] (z : Complexified A) : (-z).im = -z.im

@[simp]

theorem AnalyticSpace.Complexified.sub_re {A : Type u} [CommRing A] (z w : Complexified A) : (z - w).re = z.re - w.re

@[simp]

theorem AnalyticSpace.Complexified.sub_im {A : Type u} [CommRing A] (z w : Complexified A) : (z - w).im = z.im - w.im

@[simp]

theorem AnalyticSpace.Complexified.mul_re {A : Type u} [CommRing A] (z w : Complexified A) : (z * w).re = z.re * w.re - z.im * w.im

@[simp]

theorem AnalyticSpace.Complexified.mul_im {A : Type u} [CommRing A] (z w : Complexified A) : (z * w).im = z.re * w.im + z.im * w.re

@[simp]

theorem AnalyticSpace.Complexified.nsmul_re {A : Type u} [CommRing A] (n : ℕ) (z : Complexified A) : (n • z).re = n • z.re

@[simp]

theorem AnalyticSpace.Complexified.nsmul_im {A : Type u} [CommRing A] (n : ℕ) (z : Complexified A) : (n • z).im = n • z.im

@[simp]

theorem AnalyticSpace.Complexified.zsmul_re {A : Type u} [CommRing A] (n : ℤ) (z : Complexified A) : (n • z).re = n • z.re

@[simp]

theorem AnalyticSpace.Complexified.zsmul_im {A : Type u} [CommRing A] (n : ℤ) (z : Complexified A) : (n • z).im = n • z.im

@[simp]

theorem AnalyticSpace.Complexified.natCast_re {A : Type u} [CommRing A] (n : ℕ) : (↑n).re = ↑n

@[simp]

theorem AnalyticSpace.Complexified.natCast_im {A : Type u} [CommRing A] (n : ℕ) : (↑n).im = 0

@[simp]

theorem AnalyticSpace.Complexified.intCast_re {A : Type u} [CommRing A] (n : ℤ) : (↑n).re = ↑n

@[simp]

theorem AnalyticSpace.Complexified.intCast_im {A : Type u} [CommRing A] (n : ℤ) : (↑n).im = 0

@[instance_reducible]

instance AnalyticSpace.Complexified.instCommRing {A : Type u} [CommRing A] : CommRing (Complexified A)

Equations

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

instance AnalyticSpace.Complexified.instNontrivial {A : Type u} [CommRing A] [Nontrivial A] : Nontrivial (Complexified A)

def AnalyticSpace.Complexified.ofReal {A : Type u} [CommRing A] : A →+* Complexified A

The canonical inclusion A → A ⊗_ℝ ℂ, a ↦ a ⊗ 1 = a + 0 i.

Equations

• AnalyticSpace.Complexified.ofReal = { toFun := fun (a : A) => { re := a, im := 0 }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AnalyticSpace.Complexified.ofReal_re {A : Type u} [CommRing A] (a : A) : (ofReal a).re = a

@[simp]

theorem AnalyticSpace.Complexified.ofReal_im {A : Type u} [CommRing A] (a : A) : (ofReal a).im = 0

theorem AnalyticSpace.Complexified.ofReal_injective {A : Type u} [CommRing A] : Function.Injective ⇑ofReal

def AnalyticSpace.Complexified.I {A : Type u} [CommRing A] : Complexified A

The imaginary unit i = 1 ⊗ i of A ⊗_ℝ ℂ.

Equations

• AnalyticSpace.Complexified.I = { re := 0, im := 1 }

@[simp]

theorem AnalyticSpace.Complexified.I_re {A : Type u} [CommRing A] : I.re = 0

@[simp]

theorem AnalyticSpace.Complexified.I_im {A : Type u} [CommRing A] : I.im = 1

theorem AnalyticSpace.Complexified.I_mul_I {A : Type u} [CommRing A] : I * I = -1

theorem AnalyticSpace.Complexified.re_add_im {A : Type u} [CommRing A] (z : Complexified A) : ofReal z.re + ofReal z.im * I = z

theorem AnalyticSpace.Complexified.mk_eq {A : Type u} [CommRing A] (a b : A) : { re := a, im := b } = ofReal a + ofReal b * I

def AnalyticSpace.Complexified.map {A : Type u} {B : Type v} [CommRing A] [CommRing B] (f : A →+* B) : Complexified A →+* Complexified B

The complexification of a ring homomorphism, componentwise.

Equations

• AnalyticSpace.Complexified.map f = { toFun := fun (z : AnalyticSpace.Complexified A) => { re := f z.re, im := f z.im }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AnalyticSpace.Complexified.map_re {A : Type u} {B : Type v} [CommRing A] [CommRing B] (f : A →+* B) (z : Complexified A) : ((map f) z).re = f z.re

@[simp]

theorem AnalyticSpace.Complexified.map_im {A : Type u} {B : Type v} [CommRing A] [CommRing B] (f : A →+* B) (z : Complexified A) : ((map f) z).im = f z.im

@[simp]

theorem AnalyticSpace.Complexified.map_id {A : Type u} [CommRing A] : map (RingHom.id A) = RingHom.id (Complexified A)

theorem AnalyticSpace.Complexified.map_comp {A : Type u} {B : Type v} [CommRing A] [CommRing B] {C : Type u_1} [CommRing C] (g : B →+* C) (f : A →+* B) : map (g.comp f) = (map g).comp (map f)

theorem AnalyticSpace.Complexified.map_comp_apply {A : Type u} {B : Type v} [CommRing A] [CommRing B] {C : Type u_1} [CommRing C] (g : B →+* C) (f : A →+* B) (z : Complexified A) : (map g) ((map f) z) = (map (g.comp f)) z

@[simp]

theorem AnalyticSpace.Complexified.map_ofReal {A : Type u} {B : Type v} [CommRing A] [CommRing B] (f : A →+* B) (a : A) : (map f) (ofReal a) = ofReal (f a)

@[simp]

theorem AnalyticSpace.Complexified.map_I {A : Type u} {B : Type v} [CommRing A] [CommRing B] (f : A →+* B) : (map f) I = I

theorem AnalyticSpace.Complexified.map_injective {A : Type u} {B : Type v} [CommRing A] [CommRing B] {f : A →+* B} (hf : Function.Injective ⇑f) : Function.Injective ⇑(map f)

theorem AnalyticSpace.Complexified.map_surjective {A : Type u} {B : Type v} [CommRing A] [CommRing B] {f : A →+* B} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(map f)

theorem AnalyticSpace.Complexified.map_bijective {A : Type u} {B : Type v} [CommRing A] [CommRing B] {f : A →+* B} (hf : Function.Bijective ⇑f) : Function.Bijective ⇑(map f)

noncomputable def AnalyticSpace.Complexified.mapEquiv {A : Type u} {B : Type v} [CommRing A] [CommRing B] (e : A ≃+* B) : Complexified A ≃+* Complexified B

The complexification of a ring isomorphism.

Equations

• AnalyticSpace.Complexified.mapEquiv e = RingEquiv.ofBijective (AnalyticSpace.Complexified.map e.toRingHom) ⋯

@[simp]

theorem AnalyticSpace.Complexified.mapEquiv_apply {A : Type u} {B : Type v} [CommRing A] [CommRing B] (e : A ≃+* B) (z : Complexified A) : (mapEquiv e) z = (map e.toRingHom) z

def AnalyticSpace.Complexified.algebraMapComplex {A : Type u} [CommRing A] (φ : ℝ →+* A) : ℂ →+* Complexified A

The ℂ-structure of A ⊗_ℝ ℂ induced by an ℝ-structure φ : ℝ →+* A of A: c ↦ φ(Re c) + φ(Im c) i.

Equations

• AnalyticSpace.Complexified.algebraMapComplex φ = { toFun := fun (c : ℂ) => { re := φ c.re, im := φ c.im }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AnalyticSpace.Complexified.algebraMapComplex_re {A : Type u} [CommRing A] (φ : ℝ →+* A) (c : ℂ) : ((algebraMapComplex φ) c).re = φ c.re

@[simp]

theorem AnalyticSpace.Complexified.algebraMapComplex_im {A : Type u} [CommRing A] (φ : ℝ →+* A) (c : ℂ) : ((algebraMapComplex φ) c).im = φ c.im

theorem AnalyticSpace.Complexified.algebraMapComplex_ofReal {A : Type u} [CommRing A] (φ : ℝ →+* A) (r : ℝ) : (algebraMapComplex φ) ↑r = ofReal (φ r)

theorem AnalyticSpace.Complexified.algebraMapComplex_I {A : Type u} [CommRing A] (φ : ℝ →+* A) : (algebraMapComplex φ) Complex.I = I

theorem AnalyticSpace.Complexified.map_comp_algebraMapComplex {A : Type u} {B : Type v} [CommRing A] [CommRing B] (f : A →+* B) (φ : ℝ →+* A) : (map f).comp (algebraMapComplex φ) = algebraMapComplex (f.comp φ)

@[instance_reducible]

instance AnalyticSpace.Complexified.instSMul {A : Type u} [CommRing A] {R : Type u_1} [CommSemiring R] [Algebra R A] : SMul R (Complexified A)

Equations

• AnalyticSpace.Complexified.instSMul = { smul := fun (r : R) (z : AnalyticSpace.Complexified A) => { re := r • z.re, im := r • z.im } }

@[simp]

theorem AnalyticSpace.Complexified.smul_re {A : Type u} [CommRing A] {R : Type u_1} [CommSemiring R] [Algebra R A] (r : R) (z : Complexified A) : (r • z).re = r • z.re

@[simp]

theorem AnalyticSpace.Complexified.smul_im {A : Type u} [CommRing A] {R : Type u_1} [CommSemiring R] [Algebra R A] (r : R) (z : Complexified A) : (r • z).im = r • z.im

@[instance_reducible]

instance AnalyticSpace.Complexified.instAlgebra {A : Type u} [CommRing A] {R : Type u_1} [CommSemiring R] [Algebra R A] : Algebra R (Complexified A)

The R-algebra structure of A ⊗_ℝ ℂ from one of A (through ofReal).

Equations

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

@[simp]

theorem AnalyticSpace.Complexified.algebraMap_apply {A : Type u} [CommRing A] {R : Type u_1} [CommSemiring R] [Algebra R A] (r : R) : (algebraMap R (Complexified A)) r = ofReal ((algebraMap R A) r)

def AnalyticSpace.Complexified.ofRealAlgHom {A : Type u} [CommRing A] {R : Type u_1} [CommSemiring R] [Algebra R A] : A →ₐ[R] Complexified A

ofReal as an R-algebra homomorphism.

Equations

• AnalyticSpace.Complexified.ofRealAlgHom = { toRingHom := AnalyticSpace.Complexified.ofReal, commutes' := ⋯ }

@[simp]

theorem AnalyticSpace.Complexified.ofRealAlgHom_apply {A : Type u} [CommRing A] {R : Type u_1} [CommSemiring R] [Algebra R A] (a : A) : ofRealAlgHom a = ofReal a

The norm a² + b², units and the local-ring theorem

def AnalyticSpace.Complexified.norm {A : Type u} [CommRing A] (z : Complexified A) : A

The norm N(a + bi) = a² + b², multiplicative.

Equations

• z.norm = z.re * z.re + z.im * z.im

theorem AnalyticSpace.Complexified.norm_mul {A : Type u} [CommRing A] (z w : Complexified A) : (z * w).norm = z.norm * w.norm

theorem AnalyticSpace.Complexified.norm_one {A : Type u} [CommRing A] : norm 1 = 1

def AnalyticSpace.Complexified.conj {A : Type u} [CommRing A] (z : Complexified A) : Complexified A

The conjugate a - bi.

Equations

• z.conj = { re := z.re, im := -z.im }

theorem AnalyticSpace.Complexified.mul_conj {A : Type u} [CommRing A] (z : Complexified A) : z * z.conj = ofReal z.norm

theorem AnalyticSpace.Complexified.isUnit_iff_isUnit_norm {A : Type u} [CommRing A] (z : Complexified A) : IsUnit z ↔ IsUnit z.norm

theorem AnalyticSpace.Complexified.isUnit_ofReal_iff {A : Type u} [CommRing A] (a : A) : IsUnit (ofReal a) ↔ IsUnit a

theorem AnalyticSpace.Complexified.isLocalRing_of_exists_sub_mem {A : Type u} [CommRing A] [IsLocalRing A] (φ : ℝ →+* A) (h : ∀ (a : A), ∃ (c : ℝ), a - φ c ∈ IsLocalRing.maximalIdeal A) : IsLocalRing (Complexified A)

The local-ring theorem behind Hironaka's "(X, 𝒪_X ⊗_ℝ ℂ) is a ℂ-local-ringed space" [Hir64, Ch. 0, §1, p. 120]: if A is a local ring with residue field ℝ — every element is congruent modulo 𝔪_A to a constant φ c, φ : ℝ →+* A — then A ⊗_ℝ ℂ = A[i] is a local ring. Proof: for z = a + bi with a ≡ φ α, b ≡ φ β, the norm a² + b² ≡ φ(α² + β²); if (α, β) ≠ 0 this is a unit of A (a constant outside 𝔪_A), so z is a unit; otherwise a, b ∈ 𝔪_A and 1 - z has norm ≡ 1, a unit.

theorem AnalyticSpace.Complexified.isLocalHom_map {A : Type u} {B : Type v} [CommRing A] [CommRing B] (f : A →+* B) [IsLocalHom f] : IsLocalHom (map f)

A local homomorphism complexifies to a local homomorphism.

The identification with Mathlib's tensor product A ⊗[ℝ] ℂ

noncomputable def AnalyticSpace.Complexified.algebraMapComplexAlgHom {A : Type u} [CommRing A] [Algebra ℝ A] : ℂ →ₐ[ℝ] Complexified A

The ℂ-structure of A ⊗_ℝ ℂ as an ℝ-algebra homomorphism ℂ →ₐ[ℝ] A[i].

Equations

• AnalyticSpace.Complexified.algebraMapComplexAlgHom = { toRingHom := AnalyticSpace.Complexified.algebraMapComplex (algebraMap ℝ A), commutes' := ⋯ }

@[simp]

theorem AnalyticSpace.Complexified.algebraMapComplexAlgHom_apply {A : Type u} [CommRing A] [Algebra ℝ A] (c : ℂ) : algebraMapComplexAlgHom c = { re := (algebraMap ℝ A) c.re, im := (algebraMap ℝ A) c.im }

noncomputable def AnalyticSpace.Complexified.ofTensor {A : Type u} [CommRing A] [Algebra ℝ A] : TensorProduct ℝ A ℂ →ₐ[ℝ] Complexified A

A ⊗[ℝ] ℂ → A[i]: a ⊗ c ↦ a · (Re c + Im c · i).

Equations

• AnalyticSpace.Complexified.ofTensor = Algebra.TensorProduct.productMap AnalyticSpace.Complexified.ofRealAlgHom AnalyticSpace.Complexified.algebraMapComplexAlgHom

@[simp]

theorem AnalyticSpace.Complexified.ofTensor_tmul {A : Type u} [CommRing A] [Algebra ℝ A] (a : A) (c : ℂ) : ofTensor (a ⊗ₜ[ℝ] c) = ofReal a * { re := (algebraMap ℝ A) c.re, im := (algebraMap ℝ A) c.im }

noncomputable def AnalyticSpace.Complexified.toTensor {A : Type u} [CommRing A] [Algebra ℝ A] : Complexified A →ₐ[ℝ] TensorProduct ℝ A ℂ

A[i] → A ⊗[ℝ] ℂ: a + b i ↦ a ⊗ 1 + b ⊗ i.

Equations

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

@[simp]

theorem AnalyticSpace.Complexified.toTensor_apply {A : Type u} [CommRing A] [Algebra ℝ A] (z : Complexified A) : toTensor z = z.re ⊗ₜ[ℝ] 1 + z.im ⊗ₜ[ℝ] Complex.I

theorem AnalyticSpace.Complexified.toTensor_ofTensor {A : Type u} [CommRing A] [Algebra ℝ A] (t : TensorProduct ℝ A ℂ) : toTensor (ofTensor t) = t

theorem AnalyticSpace.Complexified.ofTensor_toTensor {A : Type u} [CommRing A] [Algebra ℝ A] (z : Complexified A) : ofTensor (toTensor z) = z

noncomputable def AnalyticSpace.Complexified.tensorEquiv {A : Type u} [CommRing A] [Algebra ℝ A] : Complexified A ≃ₐ[ℝ] TensorProduct ℝ A ℂ

The identification A[i] ≅ A ⊗[ℝ] ℂ (Hironaka's 𝒪_X ⊗_ℝ ℂ read sectionwise as 𝒪_X[i]): a + b i ↦ a ⊗ 1 + b ⊗ i.

Equations

• AnalyticSpace.Complexified.tensorEquiv = AlgEquiv.ofAlgHom AnalyticSpace.Complexified.toTensor AnalyticSpace.Complexified.ofTensor ⋯ ⋯

@[simp]

theorem AnalyticSpace.Complexified.tensorEquiv_apply {A : Type u} [CommRing A] [Algebra ℝ A] (z : Complexified A) : tensorEquiv z = z.re ⊗ₜ[ℝ] 1 + z.im ⊗ₜ[ℝ] Complex.I

theorem AnalyticSpace.Complexified.tensorEquiv_ofReal {A : Type u} [CommRing A] [Algebra ℝ A] (a : A) : tensorEquiv (ofReal a) = a ⊗ₜ[ℝ] 1

theorem AnalyticSpace.Complexified.tensorEquiv_I {A : Type u} [CommRing A] [Algebra ℝ A] : tensorEquiv I = 1 ⊗ₜ[ℝ] Complex.I

Noetherianity: A[i] is Noetherian when A is

theorem AnalyticSpace.Complexified.surjective_ofRealPair {A : Type u} [CommRing A] : Function.Surjective fun (p : A × A) => ofReal p.1 + ofReal p.2 * I

A[i] is generated by 1 and i as an A-module: the image of A × A.

def AnalyticSpace.Complexified.ofRealPairLinear {A : Type u} [CommRing A] : A × A →ₗ[A] Complexified A

The A-linear map A × A → A[i], (a, b) ↦ a + b i.

Equations

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

theorem AnalyticSpace.Complexified.surjective_ofRealPairLinear {A : Type u} [CommRing A] : Function.Surjective ⇑ofRealPairLinear

instance AnalyticSpace.Complexified.instModuleFinite {A : Type u} [CommRing A] : Module.Finite A (Complexified A)

instance AnalyticSpace.Complexified.instIsNoetherianRing {A : Type u} [CommRing A] [IsNoetherianRing A] : IsNoetherianRing (Complexified A)

A[i] = A ⊗_ℝ ℂ is Noetherian when A is (a finite A-module).