LeanPool.BrauerGroupNew.ToSecond

Imported Lean Pool material for LeanPool.BrauerGroupNew.ToSecond.

structure GoodRep {F : Type} (K : Type) [Field K] [Field F] [Algebra F K] (X : BrauerGroup F) extends CSA F : Type 1

A relative Brauer class representative with a splitting-field embedding.

• carrier : Type
• isRing : Ring ↑self.toAlgCat
• isAlgebra : Algebra F ↑self.toAlgCat
• isCentral : Algebra.IsCentral F ↑self.toAlgCat
• isSimple : IsSimpleRing ↑self.toAlgCat
• fin_dim : FiniteDimensional F ↑self.toAlgCat
• quot_eq : Quotient.mk'' self.toCSA = X

  The underlying central simple algebra represents the chosen Brauer class.

• ι : K →ₐ[F] ↑self.toAlgCat

  The chosen algebra embedding of the splitting field into the representative.

• dim_eq_sq : Module.finrank F ↑self.toAlgCat = Module.finrank F K ^ 2

  The representative has the expected square dimension over the base field.

@[implicit_reducible]

noncomputable instance GoodRep.instCoeSortType {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} : CoeSort (GoodRep K X) Type

Equations

• GoodRep.instCoeSortType = { coe := fun (A : GoodRep K X) => ↑A.toAlgCat }

noncomputable def GoodRep.ιRange {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} (A : GoodRep K X) : K ≃ₐ[F] ↥A.ι.range

The splitting-field embedding identifies K with its range.

Equations

• A.ιRange = AlgEquiv.ofInjective A.ι ⋯

@[implicit_reducible]

noncomputable instance GoodRep.instAlgebraCarrier {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} (A : GoodRep K X) : Algebra F ↑A.toAlgCat

Equations

• A.instAlgebraCarrier = AlgCat.instAlgebraObjForgetAlgHomCarrier F

instance GoodRep.instIsSimpleOrderTwoSidedIdealSubtypeCarrierMemSubalgebraRangeι {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} (A : GoodRep K X) : IsSimpleOrder (TwoSidedIdeal ↥A.ι.range)

theorem GoodRep.centralizerιRange {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} (A : GoodRep K X) : Subalgebra.centralizer F ↑A.ι.range = A.ι.range

@[implicit_reducible]

noncomputable instance GoodRep.instModuleCarrier {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} (A : GoodRep K X) : Module K ↑A.toAlgCat

Equations

• A.instModuleCarrier = { smul := fun (c : K) (a : ↑A.toAlgCat) => A.ι c * a, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[simp]

theorem GoodRep.smul_def {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} (A : GoodRep K X) (c : K) (a : ↑A.toAlgCat) : c • a = A.ι c * a

instance GoodRep.instFiniteDimensionalCarrier {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} (A : GoodRep K X) : FiniteDimensional F ↑A.toAlgCat

instance GoodRep.instIsScalarTowerCarrier {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} (A : GoodRep K X) : IsScalarTower F K ↑A.toAlgCat

instance GoodRep.instFiniteDimensionalCarrier_1 {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} (A : GoodRep K X) : FiniteDimensional K ↑A.toAlgCat

theorem GoodRep.dim_eq' {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} (A : GoodRep K X) [FiniteDimensional F K] : Module.finrank K ↑A.toAlgCat = Module.finrank F K

noncomputable def GoodRep.conjFactor {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} (A : GoodRep K X) (σ : Gal(K/F)) : Type

A unit implementing the Galois action by conjugation on the embedded splitting field.

Equations

• A.conjFactor σ = { a : (↑A.toAlgCat)ˣ // ∀ (x : K), A.ι (σ x) = ↑a * A.ι x * ↑a⁻¹ }

noncomputable def GoodRep.arbitraryConjFactor {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} (A : GoodRep K X) (σ : Gal(K/F)) : A.conjFactor σ

A chosen conjugating unit for each Galois automorphism, supplied by Skolem-Noether.

Equations

• A.arbitraryConjFactor σ = ⟨⋯.choose, ⋯⟩

@[simp]

theorem GoodRep.conjFactor_prop {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ : Gal(K/F)} (x : A.conjFactor σ) (c : K) : ↑↑x * A.ι c * ↑(↑x)⁻¹ = A.ι (σ c)

noncomputable def GoodRep.mul' {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ τ : Gal(K/F)} (x : A.conjFactor σ) (y : A.conjFactor τ) : A.conjFactor (σ * τ)

The product of two conjugating units as a conjugating unit for the product automorphism.

Equations

• GoodRep.mul' x y = ⟨↑x * ↑y, ⋯⟩

@[simp]

theorem GoodRep.mul'_coe {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ τ : Gal(K/F)} (x : A.conjFactor σ) (y : A.conjFactor τ) : ↑↑(mul' x y) = ↑↑x * ↑↑y

theorem GoodRep.conjFactor_rel_aux {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ : Gal(K/F)} (x y : A.conjFactor σ) : ∃ (c : K), ↑↑x = ↑↑y * A.ι c

theorem GoodRep.conjFactor_rel {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ : Gal(K/F)} (x y : A.conjFactor σ) : ∃! c : K, ↑↑x = ↑↑y * A.ι c

noncomputable def GoodRep.conjFactorTwistCoeff {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ : Gal(K/F)} (x y : A.conjFactor σ) : K

The scalar comparing two conjugating units for the same automorphism.

Equations

• GoodRep.conjFactorTwistCoeff x y = Exists.choose ⋯

theorem GoodRep.conjFactorTwistCoeff_spec {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ : Gal(K/F)} (x y : A.conjFactor σ) : ↑↑x = ↑↑y * A.ι (conjFactorTwistCoeff x y)

theorem GoodRep.conjFactorTwistCoeff_unique {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ : Gal(K/F)} (x y : A.conjFactor σ) (c : K) (h : ↑↑x = ↑↑y * A.ι c) : c = conjFactorTwistCoeff x y

@[simp]

theorem GoodRep.conjFactorTwistCoeff_self {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ : Gal(K/F)} (x : A.conjFactor σ) : conjFactorTwistCoeff x x = 1

noncomputable def GoodRep.conjFactorTwistCoeffAsUnit {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ : Gal(K/F)} (x y : A.conjFactor σ) : Kˣ

The twist coefficient packaged as a unit.

Equations

• GoodRep.conjFactorTwistCoeffAsUnit x y = { val := GoodRep.conjFactorTwistCoeff x y, inv := GoodRep.conjFactorTwistCoeff y x, val_inv := ⋯, inv_val := ⋯ }

theorem GoodRep.val_inv_conjFactorTwistCoeffAsUnit {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ : Gal(K/F)} (x y : A.conjFactor σ) : ↑(conjFactorTwistCoeffAsUnit x y)⁻¹ = conjFactorTwistCoeff y x

theorem GoodRep.val_conjFactorTwistCoeffAsUnit {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ : Gal(K/F)} (x y : A.conjFactor σ) : ↑(conjFactorTwistCoeffAsUnit x y) = conjFactorTwistCoeff x y

@[simp]

theorem GoodRep.conjFactorTwistCoeff_swap {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ : Gal(K/F)} (x y : A.conjFactor σ) : conjFactorTwistCoeff x y * conjFactorTwistCoeff y x = 1

theorem GoodRep.conjFactorTwistCoeff_inv {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ : Gal(K/F)} (x y : A.conjFactor σ) : conjFactorTwistCoeff x y = (conjFactorTwistCoeff y x)⁻¹

theorem GoodRep.conjFactorTwistCoeff_swap' {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ : Gal(K/F)} (x y : A.conjFactor σ) : conjFactorTwistCoeff y x * conjFactorTwistCoeff x y = 1

@[simp]

theorem GoodRep.conjFactorTwistCoeff_swap'' {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ : Gal(K/F)} (x y : A.conjFactor σ) : A.ι (conjFactorTwistCoeff x y) * A.ι (conjFactorTwistCoeff y x) = 1

theorem GoodRep.conjFactorTwistCoeff_swap''' {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ : Gal(K/F)} (x y : A.conjFactor σ) : A.ι (conjFactorTwistCoeff y x) * A.ι (conjFactorTwistCoeff x y) = 1

theorem GoodRep.conjFactorTwistCoeff_spec' {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ : Gal(K/F)} (x y : A.conjFactor σ) : ↑↑x = A.ι (σ (conjFactorTwistCoeff x y)) * ↑↑y

noncomputable def GoodRep.conjFactorCompCoeff {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ τ : Gal(K/F)} (x : A.conjFactor σ) (y : A.conjFactor τ) (z : A.conjFactor (σ * τ)) : K

The scalar measuring the defect of the chosen conjugating units from being multiplicative.

Equations

• GoodRep.conjFactorCompCoeff x y z = σ (τ (GoodRep.conjFactorTwistCoeff (GoodRep.mul' x y) z))

noncomputable def GoodRep.conjFactorCompCoeffAsUnit {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ τ : Gal(K/F)} (x : A.conjFactor σ) (y : A.conjFactor τ) (z : A.conjFactor (σ * τ)) : Kˣ

The composition coefficient packaged as a unit.

Equations

• GoodRep.conjFactorCompCoeffAsUnit x y z = { val := GoodRep.conjFactorCompCoeff x y z, inv := σ (τ (GoodRep.conjFactorTwistCoeff z (GoodRep.mul' x y))), val_inv := ⋯, inv_val := ⋯ }

theorem GoodRep.val_conjFactorCompCoeffAsUnit {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ τ : Gal(K/F)} (x : A.conjFactor σ) (y : A.conjFactor τ) (z : A.conjFactor (σ * τ)) : ↑(conjFactorCompCoeffAsUnit x y z) = conjFactorCompCoeff x y z

theorem GoodRep.val_inv_conjFactorCompCoeffAsUnit {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ τ : Gal(K/F)} (x : A.conjFactor σ) (y : A.conjFactor τ) (z : A.conjFactor (σ * τ)) : ↑(conjFactorCompCoeffAsUnit x y z)⁻¹ = σ (τ (conjFactorTwistCoeff z (mul' x y)))

theorem GoodRep.conjFactorCompCoeff_spec {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ τ : Gal(K/F)} (x : A.conjFactor σ) (y : A.conjFactor τ) (z : A.conjFactor (σ * τ)) : ↑↑x * ↑↑y = A.ι (conjFactorCompCoeff x y z) * ↑↑z

theorem GoodRep.conjFactorCompCoeff_spec'_ {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ τ : Gal(K/F)} (x : A.conjFactor σ) (y : A.conjFactor τ) (z : A.conjFactor (σ * τ)) : A.ι (↑(conjFactorCompCoeffAsUnit x y z))⁻¹ * (↑↑x * ↑↑y) = ↑↑z

theorem GoodRep.conjFactorCompCoeff_spec' {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ τ : Gal(K/F)} (x : A.conjFactor σ) (y : A.conjFactor τ) (z : A.conjFactor (σ * τ)) : A.ι (σ (τ (conjFactorTwistCoeff z (mul' x y)))) * (↑↑x * ↑↑y) = ↑↑z

theorem GoodRep.conjFactorCompCoeff_spec'' {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ τ : Gal(K/F)} (x : A.conjFactor σ) (y : A.conjFactor τ) (z : A.conjFactor (σ * τ)) : A.ι (conjFactorCompCoeff x y z) = ↑↑x * ↑↑y * ↑(↑z)⁻¹

theorem GoodRep.conjFactorCompCoeff_inv {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ τ : Gal(K/F)} (x : A.conjFactor σ) (y : A.conjFactor τ) (z : A.conjFactor (σ * τ)) : A.ι (conjFactorCompCoeff x y z)⁻¹ = ↑↑z * (↑(↑y)⁻¹ * ↑(↑x)⁻¹)

theorem GoodRep.conjFactorCompCoeff_comp_comp₁ {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {ρ σ τ : Gal(K/F)} (xρ : A.conjFactor ρ) (xσ : A.conjFactor σ) (xτ : A.conjFactor τ) (xρσ : A.conjFactor (ρ * σ)) (xρστ : A.conjFactor (ρ * σ * τ)) : ↑↑xρ * ↑↑xσ * ↑↑xτ = A.ι (conjFactorCompCoeff xρ xσ xρσ) * A.ι (conjFactorCompCoeff xρσ xτ xρστ) * ↑↑xρστ

theorem GoodRep.conjFactorCompCoeff_eq {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {σ τ : Gal(K/F)} (x : A.conjFactor σ) (y : A.conjFactor τ) (z : A.conjFactor (σ * τ)) : A.ι (conjFactorCompCoeff x y z) = ↑↑x * ↑↑y * ↑(↑z)⁻¹

theorem GoodRep.conjFactorCompCoeff_comp_comp₂ {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {ρ σ τ : Gal(K/F)} (xρ : A.conjFactor ρ) (xσ : A.conjFactor σ) (xτ : A.conjFactor τ) (xστ : A.conjFactor (σ * τ)) (xρστ : A.conjFactor (ρ * σ * τ)) : ↑↑xρ * (↑↑xσ * ↑↑xτ) = A.ι (ρ (conjFactorCompCoeff xσ xτ xστ)) * A.ι (conjFactorCompCoeff xρ xστ xρστ) * ↑↑xρστ

theorem GoodRep.conjFactorCompCoeff_comp_comp₃ {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {ρ σ τ : Gal(K/F)} (xρ : A.conjFactor ρ) (xσ : A.conjFactor σ) (xτ : A.conjFactor τ) (xρσ : A.conjFactor (ρ * σ)) (xστ : A.conjFactor (σ * τ)) (xρστ : A.conjFactor (ρ * σ * τ)) : A.ι (conjFactorCompCoeff xρ xσ xρσ) * A.ι (conjFactorCompCoeff xρσ xτ xρστ) * ↑↑xρστ = A.ι (ρ (conjFactorCompCoeff xσ xτ xστ)) * A.ι (conjFactorCompCoeff xρ xστ xρστ) * ↑↑xρστ

theorem GoodRep.conjFactorCompCoeff_comp_comp {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} {ρ σ τ : Gal(K/F)} (xρ : A.conjFactor ρ) (xσ : A.conjFactor σ) (xτ : A.conjFactor τ) (xρσ : A.conjFactor (ρ * σ)) (xστ : A.conjFactor (σ * τ)) (xρστ : A.conjFactor (ρ * σ * τ)) : conjFactorCompCoeff xρ xσ xρσ * conjFactorCompCoeff xρσ xτ xρστ = ρ (conjFactorCompCoeff xσ xτ xστ) * conjFactorCompCoeff xρ xστ xρστ

noncomputable def GoodRep.toCocycles₂ {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} (A : GoodRep K X) (x_ : (σ : Gal(K/F)) → A.conjFactor σ) : Gal(K/F) × Gal(K/F) → Kˣ

The two-cocycle associated to a system of conjugating units.

Equations

• A.toCocycles₂ x_ p = GoodRep.conjFactorCompCoeffAsUnit (x_ p.1) (x_ p.2) (x_ (p.1 * p.2))

theorem GoodRep.toCocycles₂_cond {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (ρ σ τ : Gal(K/F)) (x_ : (σ : Gal(K/F)) → A.conjFactor σ) : ρ ↑(A.toCocycles₂ x_ (σ, τ)) * ↑(A.toCocycles₂ x_ (ρ, σ * τ)) = ↑(A.toCocycles₂ x_ (ρ, σ)) * ↑(A.toCocycles₂ x_ (ρ * σ, τ))

theorem GoodRep.isMulCocycle₂ {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (x_ : (σ : Gal(K/F)) → A.conjFactor σ) : groupCohomology.IsMulCocycle₂ (A.toCocycles₂ x_)

theorem GoodRep.exists_iso {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) : Nonempty (↑A.toAlgCat ≃ₐ[F] ↑B.toAlgCat)

noncomputable def GoodRep.iso {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) : ↑A.toAlgCat ≃ₐ[F] ↑B.toAlgCat

A chosen algebra equivalence between two representatives of the same Brauer class.

Equations

• GoodRep.iso B = ⋯.some

noncomputable def GoodRep.isoConjCoeff {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) : (↑B.toAlgCat)ˣ

The unit conjugating the transported splitting-field embedding to the target embedding.

Equations

• GoodRep.isoConjCoeff B = ⋯.choose

theorem GoodRep.isoConjCoeff_spec {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) (r : K) : B.ι r = ↑(isoConjCoeff B) * (iso B) (A.ι r) * ↑(isoConjCoeff B)⁻¹

theorem GoodRep.isoConjCoeff_spec' {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) (r : K) : ↑(isoConjCoeff B)⁻¹ * B.ι r * ↑(isoConjCoeff B) = (iso B) (A.ι r)

theorem GoodRep.isoConjCoeff_spec'' {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) {σ : Gal(K/F)} (c : K) (x : A.conjFactor σ) : B.ι (σ c) = ↑(isoConjCoeff B) * (iso B) ↑↑x * ↑(isoConjCoeff B)⁻¹ * B.ι c * (↑(isoConjCoeff B) * (iso B) ↑(↑x)⁻¹ * ↑(isoConjCoeff B)⁻¹)

noncomputable def GoodRep.pushConjFactor {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) {σ : Gal(K/F)} (x : A.conjFactor σ) : B.conjFactor σ

Transport a conjugating unit across the chosen algebra equivalence.

Equations

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

@[simp]

theorem GoodRep.pushConjFactor_coe {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) {σ : Gal(K/F)} (x : A.conjFactor σ) : ↑↑(pushConjFactor B x) = ↑(isoConjCoeff B) * (iso B) ↑↑x * ↑(isoConjCoeff B)⁻¹

noncomputable def GoodRep.pushConjFactorCoeff {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) {σ : Gal(K/F)} (x : A.conjFactor σ) (y : B.conjFactor σ) : K

The scalar comparing a transported conjugating unit with a chosen target unit.

Equations

• GoodRep.pushConjFactorCoeff B x y = σ (GoodRep.conjFactorTwistCoeff y (GoodRep.pushConjFactor B x))

theorem GoodRep.pushConjFactorCoeff_spec {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) {σ : Gal(K/F)} (x : A.conjFactor σ) (y : B.conjFactor σ) : ↑↑y = B.ι (pushConjFactorCoeff B x y) * ↑↑(pushConjFactor B x)

theorem GoodRep.pushConjFactorCoeff_spec' {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) {σ : Gal(K/F)} (x : A.conjFactor σ) (y : B.conjFactor σ) : B.ι (pushConjFactorCoeff B x y) = ↑(isoConjCoeff B) * (iso B) (A.ι (pushConjFactorCoeff B x y)) * ↑(isoConjCoeff B)⁻¹

@[reducible, inline]

noncomputable abbrev GoodRep.pushConjFactorCoeffAsUnit {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) {σ : Gal(K/F)} (x : A.conjFactor σ) (y : B.conjFactor σ) : Kˣ

The transported-unit comparison scalar packaged as a unit.

Equations

• GoodRep.pushConjFactorCoeffAsUnit B x y = { val := GoodRep.pushConjFactorCoeff B x y, inv := σ (GoodRep.conjFactorTwistCoeff (GoodRep.pushConjFactor B x) y), val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem GoodRep.val_inv_pushConjFactorCoeffAsUnit {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) {σ : Gal(K/F)} (x : A.conjFactor σ) (y : B.conjFactor σ) : ↑(pushConjFactorCoeffAsUnit B x y)⁻¹ = σ (conjFactorTwistCoeff (pushConjFactor B x) y)

@[simp]

theorem GoodRep.val_pushConjFactorCoeffAsUnit {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) {σ : Gal(K/F)} (x : A.conjFactor σ) (y : B.conjFactor σ) : ↑(pushConjFactorCoeffAsUnit B x y) = pushConjFactorCoeff B x y

theorem GoodRep.compare_conjFactorCompCoeff {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) {σ τ : Gal(K/F)} (xσ : A.conjFactor σ) (yσ : B.conjFactor σ) (xτ : A.conjFactor τ) (yτ : B.conjFactor τ) (xστ : A.conjFactor (σ * τ)) (yστ : B.conjFactor (σ * τ)) : conjFactorCompCoeff yσ yτ yστ * pushConjFactorCoeff B xστ yστ = pushConjFactorCoeff B xσ yσ * σ (pushConjFactorCoeff B xτ yτ) * conjFactorCompCoeff xσ xτ xστ

noncomputable def GoodRep.trivialFactorSet {F K : Type} [Field K] [Field F] [Algebra F K] (c : Gal(K/F) → Kˣ) : Gal(K/F) × Gal(K/F) → Kˣ

The multiplicative two-coboundary associated to a one-cochain.

Equations

• GoodRep.trivialFactorSet c p = c p.1 * (Units.map ↑p.1.toRingEquiv.toRingHom) (c p.2) * (c (p.1 * p.2))⁻¹

theorem GoodRep.compare_toCocycles₂ {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) {σ τ : Gal(K/F)} (x_ : (σ : Gal(K/F)) → A.conjFactor σ) (y_ : (σ : Gal(K/F)) → B.conjFactor σ) : B.toCocycles₂ y_ (σ, τ) * pushConjFactorCoeffAsUnit B (x_ (σ * τ)) (y_ (σ * τ)) = pushConjFactorCoeffAsUnit B (x_ σ) (y_ σ) * (Units.map ↑σ) (pushConjFactorCoeffAsUnit B (x_ τ) (y_ τ)) * A.toCocycles₂ x_ (σ, τ)

theorem GoodRep.compare_toCocycles₂' {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} {A : GoodRep K X} (B : GoodRep K X) (x_ : (σ : Gal(K/F)) → A.conjFactor σ) (y_ : (σ : Gal(K/F)) → B.conjFactor σ) : groupCohomology.IsMulCoboundary₂ (B.toCocycles₂ y_ / A.toCocycles₂ x_)

noncomputable def Amelia.toAdditive (M G : Type) [Monoid M] [CommGroup G] [MulDistribMulAction M G] : ↑(Rep.ofMulDistribMulAction M G) ≃+ Additive G

The additive form of a multiplicative-distribution representation.

Equations

• Amelia.toAdditive M G = AddEquiv.refl ↑(Rep.ofMulDistribMulAction M G)

@[simp]

theorem Amelia.toAdditive_symm_apply (M G : Type) [Monoid M] [CommGroup G] [MulDistribMulAction M G] (a : ↑(Rep.ofMulDistribMulAction M G)) : (toAdditive M G).symm a = a

@[simp]

theorem Amelia.toAdditive_apply (M G : Type) [Monoid M] [CommGroup G] [MulDistribMulAction M G] (a : ↑(Rep.ofMulDistribMulAction M G)) : (toAdditive M G) a = a

noncomputable def galAct (F K : Type) [Field K] [Field F] [Algebra F K] : Rep ℤ Gal(K/F)

The Galois action of Gal(K/F) on Kˣ as a representation.

Equations

• galAct F K = Rep.ofMulDistribMulAction Gal(K/F) Kˣ

@[simp]

theorem galAct_ρ_apply {F K : Type} [Field K] [Field F] [Algebra F K] (σ : Gal(K/F)) (x : Kˣ) : ((galAct F K).ρ σ) (Additive.ofMul x) = Additive.ofMul ((Units.map ↑σ) x)

theorem mem_relativeBrGroup_iff_nonempty_goodRep {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] {X : BrauerGroup F} : X ∈ RelativeBrGroup K F ↔ Nonempty (GoodRep K X)

noncomputable def RelativeBrGroup.goodRep {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] (X : ↥(RelativeBrGroup K F)) : GoodRep K ↑X

Choose a good representative for an element of the relative Brauer group.

Equations

• RelativeBrGroup.goodRep X = ⋯.some

noncomputable def GoodRep.toH2 {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} (A : GoodRep K X) (x_ : (σ : Gal(K/F)) → A.conjFactor σ) : ↑(groupCohomology.H2 (galAct F K))

The cohomology class attached to a good representative and a system of conjugating units.

Equations

• A.toH2 x_ = (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π (galAct F K))) (groupCohomology.cocyclesOfIsMulCocycle₂ ⋯)

noncomputable def RelativeBrGroup.toSnd {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] : ↥(RelativeBrGroup K F) → ↑(groupCohomology.H2 (galAct F K))

Send a relative Brauer class to its degree-two Galois cohomology class.

Equations

• RelativeBrGroup.toSnd X = (RelativeBrGroup.goodRep X).toH2 (RelativeBrGroup.goodRep X).arbitraryConjFactor

theorem RelativeBrGroup.toSnd_wd {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] (X : ↥(RelativeBrGroup K F)) (A : GoodRep K ↑X) (x_ : (σ : Gal(K/F)) → A.conjFactor σ) : toSnd X = A.toH2 x_

theorem GoodRep.conjFactor_linearIndependent {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup F} (A : GoodRep K X) (x_ : (σ : Gal(K/F)) → A.conjFactor σ) : LinearIndependent K fun (i : Gal(K/F)) => ↑↑(x_ i)

noncomputable def GoodRep.conjFactorBasis {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] {X : BrauerGroup F} (A : GoodRep K X) [IsGalois F K] (x_ : (σ : Gal(K/F)) → A.conjFactor σ) : Module.Basis Gal(K/F) K ↑A.toAlgCat

The basis of a good representative obtained from conjugating units.

Equations

• A.conjFactorBasis x_ = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

noncomputable def RelativeBrGroup.fromCocycles₂ {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] (f : ↥(groupCohomology.cocycles₂ (galAct F K))) : ↥(RelativeBrGroup K F)

Build a relative Brauer class from a two-cocycle via the cross-product algebra.

Equations

• RelativeBrGroup.fromCocycles₂ f = ⟨Quotient.mk'' (CrossProductAlgebra.asCSA (⇑Additive.toMul ∘ ↑f)), ⋯⟩

noncomputable def RelativeBrGroup.fromSnd (F K : Type) [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] : ↑(groupCohomology.shortComplexH2 (galAct F K)).moduleCatLeftHomologyData.H → ↥(RelativeBrGroup K F)

Descend the cross-product construction to second cohomology.

Equations

• RelativeBrGroup.fromSnd F K = Quotient.lift RelativeBrGroup.fromCocycles₂ ⋯

theorem RelativeBrGroup.fromSnd_wd {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] (a : ↥(groupCohomology.cocycles₂ (galAct F K))) : fromSnd F K (Quotient.mk'' a) = ⟨Quotient.mk'' (CrossProductAlgebra.asCSA (⇑Additive.toMul ∘ ⇑a)), ⋯⟩

noncomputable def Amfix.coboundariesOfIsMulCoboundary₂ {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {f : G × G → M} (hf : groupCohomology.IsMulCoboundary₂ f) : ↥(groupCohomology.coboundaries₂ (Rep.ofMulDistribMulAction G M))

Convert a multiplicative two-coboundary witness into an additive cohomology coboundary.

Equations

• Amfix.coboundariesOfIsMulCoboundary₂ hf = ⟨⇑Additive.ofMul ∘ f, ⋯⟩

theorem RelativeBrGroup.toSnd_fromSnd {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] : toSnd ∘ fromSnd F K ∘ ⇑(CategoryTheory.ConcreteCategory.hom (groupCohomology.H2Iso (galAct F K)).hom) = id

theorem RelativeBrGroup.fromSnd_toSnd {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] : (fromSnd F K ∘ ⇑(CategoryTheory.ConcreteCategory.hom (groupCohomology.H2Iso (galAct F K)).hom)) ∘ toSnd = id

noncomputable def RelativeBrGroup.equivSnd {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] : ↥(RelativeBrGroup K F) ≃ ↑(groupCohomology.H2 (galAct F K))

The equivalence between the relative Brauer group and second Galois cohomology.

Equations

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