LeanPool.BrauerGroupNew.Subfield.Defs #

Imported Lean Pool material for LeanPool.BrauerGroupNew.Subfield.Defs.

source

structure SubField (K : Type u_1) (A : Type u_2) [CommSemiring K] [Semiring A] [Algebra K A] extends Subalgebra K A :

Type u_2

A subalgebra whose carrier is commutative and contains inverses of all nonzero elements.

carrier : Set A
mul_mem' {a b : A} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
one_mem' : 1 ∈ self.carrier
add_mem' {a b : A} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
zero_mem' : 0 ∈ self.carrier
algebraMap_mem' (r : K) : (algebraMap K A) r ∈ self.carrier
mul_comm ⦃x : A⦄ (hx : x ∈ self.carrier) ⦃y : A⦄ (hy : y ∈ self.carrier) : x * y = y * x
exists_inverse ⦃x : A⦄ : x ∈ self.carrier → x ≠ 0 → ∃ y ∈ self.carrier, x * y = 1

Instances For

source

theorem SubField.toSubalgebra_injective {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :

Function.Injective toSubalgebra

source

@[simp]

theorem SubField.toSubalgebra_inj {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {L₁ L₂ : SubField R A} :

L₁.toSubalgebra = L₂.toSubalgebra ↔ L₁ = L₂

source

@[implicit_reducible]

instance SubField.instSetLike {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :

SetLike (SubField R A) A

Equations

SubField.instSetLike = { coe := fun (L : SubField R A) => ↑L.toSubalgebra, coe_injective := ⋯ }

source

@[implicit_reducible]

instance SubField.instPartialOrder {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :

PartialOrder (SubField R A)

Equations

SubField.instPartialOrder = PartialOrder.ofSetLike (SubField R A) A

source

theorem SubField.mem_carrier {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {L : SubField R A} {a : A} :

a ∈ L.carrier ↔ a ∈ L

source

@[simp]

theorem SubField.mem_toSubalgebra {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {L : SubField R A} {a : A} :

a ∈ L.toSubalgebra ↔ a ∈ L

source

@[simp]

theorem SubField.coe_toSubalgebra {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (L : SubField R A) :

↑L.toSubalgebra = ↑L

source

theorem SubField.ext {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {L₁ L₂ : SubField R A} (h : ∀ (x : A), x ∈ L₁ ↔ x ∈ L₂) :

L₁ = L₂

source

theorem SubField.ext_iff {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {L₁ L₂ : SubField R A} :

L₁ = L₂ ↔ ∀ (x : A), x ∈ L₁ ↔ x ∈ L₂

source

@[simp]

theorem SubField.toSubalgebra_le_toSubalgebra {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {L₁ L₂ : SubField R A} :

L₁.toSubalgebra ≤ L₂.toSubalgebra ↔ L₁ ≤ L₂

source

@[simp]

theorem SubField.toSubalgebra_lt_toSubalgebra {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {L₁ L₂ : SubField R A} :

L₁.toSubalgebra < L₂.toSubalgebra ↔ L₁ < L₂

source

instance SubField.instSubsemiringClass {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :

SubsemiringClass (SubField R A) A

source

@[implicit_reducible, instance 100]

instance SubField.algebra' {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {K' : Type u_4} [CommSemiring K'] [SMul K' R] [Algebra K' A] [IsScalarTower K' R A] (S : SubField R A) :

Algebra K' ↥S

Equations

S.algebra' = S.algebra'

source

@[implicit_reducible]

noncomputable instance SubField.carrier.instSemifield {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {L : SubField R A} [Nontrivial A] :

Semifield ↥L.toSubalgebra

Equations

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

source

def SubField.dSup {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set (SubField R A)) (hs : s.Nonempty) (hsdir : DirectedOn (fun (x1 x2 : SubField R A) => x1 ≤ x2) s) :

SubField R A

The directed supremum of a set of subfields.

Equations

SubField.dSup s hs hsdir = { toSubalgebra := ⨆ L ∈ s, L.toSubalgebra, mul_comm := ⋯, exists_inverse := ⋯ }

Instances For

source

@[simp]

theorem SubField.dSup_toSubalgebra {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set (SubField R A)) (hs : s.Nonempty) (hsdir : DirectedOn (fun (x1 x2 : SubField R A) => x1 ≤ x2) s) :

(dSup s hs hsdir).toSubalgebra = ⨆ L ∈ s, L.toSubalgebra

source

theorem SubField.isLUB_dSup {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set (SubField R A)) (hs : s.Nonempty) (hsdir : DirectedOn (fun (x1 x2 : SubField R A) => x1 ≤ x2) s) :

IsLUB s (dSup s hs hsdir)

source

instance SubField.instSubringClass {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] :

SubringClass (SubField R A) A

source

theorem SubField.mem_toSubring {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {L : SubField R A} {a : A} :

a ∈ L.toSubring ↔ a ∈ L

source

@[simp]

theorem SubField.coe_toSubring {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] (L : SubField R A) :

↑L.toSubring = ↑L

source

@[implicit_reducible]

noncomputable instance SubField.carrier.instField {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {L : SubField R A} [Nontrivial A] :

Field ↥L

Equations

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

source

@[implicit_reducible]

instance SubField.instBot {K : Type u_2} {A : Type u_3} [Semifield K] [Semiring A] [Algebra K A] :

Bot (SubField K A)

Equations

SubField.instBot = { bot := let __Subalgebra := ⊥; { toSubalgebra := __Subalgebra, mul_comm := ⋯, exists_inverse := ⋯ } }

source

instance SubField.instNonempty {K : Type u_2} {A : Type u_3} [Semifield K] [Semiring A] [Algebra K A] :

Nonempty (SubField K A)

source

theorem SubField.exists_isMax (K : Type u_2) (A : Type u_3) [Semifield K] [Semiring A] [Algebra K A] :

∃ (L : SubField K A), IsMax L