CoefficientDescent.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Descent through countable coefficient rings.

theorem OAI.TorsionFreeBass.countable_field_embeds_complex line 12
Source documentation
A countable characteristic-zero field admits an embedding in the complex numbers.
```
theorem countable_field_embeds_complex (F : Type*) [Field F] [CharZero F] [Countable F] :
    Nonempty (F →+* ℂ) := by
…
```
theorem OAI.TorsionFreeBass.countable_domain_embeds_complex line 39
Source documentation
The countable coefficient ring itself embeds, without an embedding of the ambient domain.
```
theorem countable_domain_embeds_complex (R : Type*) [CommRing R] [IsDomain R]
    [CharZero R] [Countable R] : ∃ f : R →+* ℂ, Function.Injective f := by
…
```

theorem OAI.TorsionFreeBass.descend_idempotents line 49

Source documentation

Descent of the scalar idempotent assertion from complex coefficients to a characteristic-zero domain, using only the finitely many coefficients.

theorem descend_idempotents {G : Type*} [Group G]
    (hC : ∀ e : MonoidAlgebra ℂ G, e * e = e → e = 0 ∨ e = 1)
    (R : Type*) [CommRing R] [IsDomain R] [CharZero R]
    (e : MonoidAlgebra R G) (he : e * e = e) : e = 0 ∨ e = 1 := by
…