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

• carrier : CSA F
• quot_eq : Quotient.mk'' self.carrier = X
• ι : K →ₐ[F] self.carrier.carrier
• dim_eq_square : Module.finrank F self.carrier.carrier = Module.finrank F K ^ 2

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

Equations

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

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

Equations

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

noncomputable instance GoodRep.instAlgebraCarrierCarrier {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} (A : GoodRep K X) : Algebra F A.carrier.carrier

Equations

• A.instAlgebraCarrierCarrier = inferInstanceAs (Algebra F A.carrier.carrier)

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

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

noncomputable instance GoodRep.instModuleCarrierCarrier {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} (A : GoodRep K X) : Module K A.carrier.carrier

Equations

• A.instModuleCarrierCarrier = Module.mk ⋯ ⋯

@[simp]

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

instance GoodRep.instFiniteDimensionalCarrierCarrier {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} (A : GoodRep K X) : FiniteDimensional F A.carrier.carrier

instance GoodRep.instIsScalarTowerCarrierCarrier {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} (A : GoodRep K X) : IsScalarTower F K A.carrier.carrier

instance GoodRep.instFiniteDimensionalCarrierCarrier_1 {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} (A : GoodRep K X) : FiniteDimensional K A.carrier.carrier

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

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

Equations

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

noncomputable def GoodRep.aribitaryConjFactor {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} (A : GoodRep K X) (σ : K ≃ₐ[F] K) : A.conjFactor σ

Equations

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

@[simp]

theorem GoodRep.conjFactor_prop {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} {A : GoodRep K X} {σ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {σ τ : K ≃ₐ[F] K} (x : A.conjFactor σ) (y : A.conjFactor τ) : A.conjFactor (σ * τ)

Equations

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

@[simp]

theorem GoodRep.mul'_coe {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} {A : GoodRep K X} {σ τ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {σ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {σ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {σ : K ≃ₐ[F] K} (x y : A.conjFactor σ) : K

Equations

• GoodRep.conjFactorTwistCoeff x y = Exists.choose ⋯

theorem GoodRep.conjFactorTwistCoeff_spec {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} {A : GoodRep K X} {σ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {σ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {σ : K ≃ₐ[F] K} (x : A.conjFactor σ) : conjFactorTwistCoeff x x = 1

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem GoodRep.conjFactorTwistCoeff_swap {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} {A : GoodRep K X} {σ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {σ : K ≃ₐ[F] K} (x y : A.conjFactor σ) : conjFactorTwistCoeff x y = (conjFactorTwistCoeff y x)⁻¹

@[simp]

theorem GoodRep.conjFactorTwistCoeff_swap' {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} {A : GoodRep K X} {σ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {σ : K ≃ₐ[F] K} (x y : A.conjFactor σ) : A.ι (conjFactorTwistCoeff x y) * A.ι (conjFactorTwistCoeff y x) = 1

@[simp]

theorem GoodRep.conjFactorTwistCoeff_swap''' {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} {A : GoodRep K X} {σ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {σ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {σ τ : K ≃ₐ[F] K} (x : A.conjFactor σ) (y : A.conjFactor τ) (z : A.conjFactor (σ * τ)) : K

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.BrGroup} {A : GoodRep K X} {σ τ : K ≃ₐ[F] K} (x : A.conjFactor σ) (y : A.conjFactor τ) (z : A.conjFactor (σ * τ)) : Kˣ

Equations

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

@[simp]

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

@[simp]

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

theorem GoodRep.conjFactorCompCoeff_spec {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} {A : GoodRep K X} {σ τ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {σ τ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {σ τ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {σ τ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {σ τ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {ρ σ τ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {σ τ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {ρ σ τ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {ρ σ τ : K ≃ₐ[F] K} (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.BrGroup} {A : GoodRep K X} {ρ σ τ : K ≃ₐ[F] K} (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.toTwoCocycles {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} (A : GoodRep K X) (x_ : (σ : K ≃ₐ[F] K) → A.conjFactor σ) : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ

Equations

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

theorem GoodRep.toTwoCocycles_cond {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} {A : GoodRep K X} (ρ σ τ : K ≃ₐ[F] K) (x_ : (σ : K ≃ₐ[F] K) → A.conjFactor σ) : ρ ↑(A.toTwoCocycles x_ (σ, τ)) * ↑(A.toTwoCocycles x_ (ρ, σ * τ)) = ↑(A.toTwoCocycles x_ (ρ, σ)) * ↑(A.toTwoCocycles x_ (ρ * σ, τ))

theorem GoodRep.isTwoCocyles {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} {A : GoodRep K X} (x_ : (σ : K ≃ₐ[F] K) → A.conjFactor σ) : groupCohomology.IsMulTwoCocycle (A.toTwoCocycles x_)

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

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

Equations

• A.iso B = ⋯.some

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

Equations

• A.isoConjCoeff B = ⋯.choose

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

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

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

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

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.BrGroup} (A B : GoodRep K X) {σ : K ≃ₐ[F] K} (x : A.conjFactor σ) : ↑↑(A.pushConjFactor B x) = ↑(A.isoConjCoeff B) * (A.iso B) ↑↑x * ↑(A.isoConjCoeff B)⁻¹

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

Equations

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

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

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

@[reducible, inline]

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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_toTwoCocycles {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} (A B : GoodRep K X) {σ τ : K ≃ₐ[F] K} (x_ : (σ : K ≃ₐ[F] K) → A.conjFactor σ) (y_ : (σ : K ≃ₐ[F] K) → B.conjFactor σ) : B.toTwoCocycles y_ (σ, τ) * A.pushConjFactorCoeffAsUnit B (x_ (σ * τ)) (y_ (σ * τ)) = A.pushConjFactorCoeffAsUnit B (x_ σ) (y_ σ) * (Units.map ↑σ) (A.pushConjFactorCoeffAsUnit B (x_ τ) (y_ τ)) * A.toTwoCocycles x_ (σ, τ)

theorem GoodRep.compare_toTwoCocycles' {F K : Type} [Field K] [Field F] [Algebra F K] {X : BrauerGroup.BrGroup} (A B : GoodRep K X) (x_ : (σ : K ≃ₐ[F] K) → A.conjFactor σ) (y_ : (σ : K ≃ₐ[F] K) → B.conjFactor σ) : groupCohomology.IsMulTwoCoboundary (B.toTwoCocycles y_ / A.toTwoCocycles x_)

noncomputable def galAct (F K : Type) [Field K] [Field F] [Algebra F K] : Rep ℤ (K ≃ₐ[F] K)

Equations

• galAct F K = Rep.ofMulDistribMulAction (K ≃ₐ[F] K) Kˣ

@[simp]

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

theorem mem_relativeBrGroup_iff_exists_goodRep {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] (X : BrauerGroup.BrGroup) : 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

Equations

• RelativeBrGroup.goodRep X = ⋯.some

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

Equations

• A.toH2 x_ = Quotient.mk'' (groupCohomology.twoCocyclesOfIsMulTwoCocycle ⋯)

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)

Equations

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

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_ : (σ : K ≃ₐ[F] K) → A.conjFactor σ) : toSnd X = A.toH2 x_

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

noncomputable def GoodRep.conjFactorBasis {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] {X : BrauerGroup.BrGroup} (A : GoodRep K X) [IsGalois F K] (x_ : (σ : K ≃ₐ[F] K) → A.conjFactor σ) : Basis (K ≃ₐ[F] K) K A.carrier.carrier

Equations

• A.conjFactorBasis x_ = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

noncomputable def GoodRep.crossProductMul {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] (a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ) : ((K ≃ₐ[F] K) → K) →ₗ[F] ((K ≃ₐ[F] K) → K) →ₗ[F] (K ≃ₐ[F] K) → K

Equations

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

@[simp]

theorem GoodRep.crossProductMul_single_single {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (σ τ : K ≃ₐ[F] K) (c d : K) : ((crossProductMul a) (Pi.single σ c)) (Pi.single τ d) = Pi.single (σ * τ) (c * σ d * ↑(a (σ, τ)))

noncomputable def GoodRep.crossProductSMul {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : F →ₗ[F] ((K ≃ₐ[F] K) → K) →ₗ[F] (K ≃ₐ[F] K) → K

Equations

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

@[simp]

theorem GoodRep.crossProductSMul_single {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] (σ : K ≃ₐ[F] K) (r : F) (c : K) : (crossProductSMul r) (Pi.single σ c) = Pi.single σ (r • c)

structure GoodRep.CrossProduct {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : Type

• val : (K ≃ₐ[F] K) → K

noncomputable instance GoodRep.CrossProduct.instAdd {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : Add (CrossProduct ha)

Equations

• GoodRep.CrossProduct.instAdd ha = { add := fun (x y : GoodRep.CrossProduct ha) => { val := x.val + y.val } }

@[simp]

theorem GoodRep.CrossProduct.add_val {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (x y : CrossProduct ha) : (x + y).val = x.val + y.val

noncomputable instance GoodRep.CrossProduct.instZero {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : Zero (CrossProduct ha)

Equations

• GoodRep.CrossProduct.instZero ha = { zero := { val := 0 } }

@[simp]

theorem GoodRep.CrossProduct.zero_val {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : val 0 = 0

noncomputable instance GoodRep.CrossProduct.instSMulNat {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : SMul ℕ (CrossProduct ha)

Equations

• GoodRep.CrossProduct.instSMulNat ha = { smul := fun (n : ℕ) (x : GoodRep.CrossProduct ha) => { val := n • x.val } }

@[simp]

theorem GoodRep.CrossProduct.nsmul_val {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (n : ℕ) (x : CrossProduct ha) : (n • x).val = n • x.val

noncomputable instance GoodRep.CrossProduct.instNeg {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : Neg (CrossProduct ha)

Equations

• GoodRep.CrossProduct.instNeg ha = { neg := fun (x : GoodRep.CrossProduct ha) => { val := -x.val } }

@[simp]

theorem GoodRep.CrossProduct.neg_val {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (x : CrossProduct ha) : (-x).val = -x.val

noncomputable instance GoodRep.CrossProduct.instSub {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : Sub (CrossProduct ha)

Equations

• GoodRep.CrossProduct.instSub ha = { sub := fun (x y : GoodRep.CrossProduct ha) => { val := x.val - y.val } }

@[simp]

theorem GoodRep.CrossProduct.sub_val {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (x y : CrossProduct ha) : (x - y).val = x.val - y.val

noncomputable instance GoodRep.CrossProduct.instSMulInt {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : SMul ℤ (CrossProduct ha)

Equations

• GoodRep.CrossProduct.instSMulInt ha = { smul := fun (n : ℤ) (x : GoodRep.CrossProduct ha) => { val := n • x.val } }

@[simp]

theorem GoodRep.CrossProduct.zsmul_val {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (n : ℤ) (x : CrossProduct ha) : (n • x).val = n • x.val

theorem GoodRep.CrossProduct.val_injective {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : Function.Injective val

theorem GoodRep.CrossProduct.ext {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (x y : CrossProduct ha) : x.val = y.val → x = y

noncomputable instance GoodRep.CrossProduct.addCommGroup {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : AddCommGroup (CrossProduct ha)

Equations

• GoodRep.CrossProduct.addCommGroup ha = Function.Injective.addCommGroup GoodRep.CrossProduct.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable def GoodRep.CrossProduct.valAddMonoidHom {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : CrossProduct ha →+ (K ≃ₐ[F] K) → K

Equations

• GoodRep.CrossProduct.valAddMonoidHom ha = { toFun := fun (x : GoodRep.CrossProduct ha) => x.val, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem GoodRep.CrossProduct.valAddMonoidHom_apply {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (x : CrossProduct ha) (a✝ : K ≃ₐ[F] K) : (valAddMonoidHom ha) x a✝ = x.val a✝

theorem GoodRep.CrossProduct.single_induction {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (x : CrossProduct ha) {motive : CrossProduct ha → Prop} (single : ∀ (σ : K ≃ₐ[F] K) (c : K), motive { val := Pi.single σ c }) (add : ∀ (x y : CrossProduct ha), motive x → motive y → motive { val := x.val + y.val }) (zero : motive { val := 0 }) : motive x

noncomputable instance GoodRep.CrossProduct.instMul {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : Mul (CrossProduct ha)

Equations

• GoodRep.CrossProduct.instMul ha = { mul := fun (x y : GoodRep.CrossProduct ha) => { val := ((GoodRep.crossProductMul a) x.val) y.val } }

theorem GoodRep.CrossProduct.mul_def {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (x y : CrossProduct ha) : x * y = { val := ((crossProductMul a) x.val) y.val }

@[simp]

theorem GoodRep.CrossProduct.mul_val {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (x y : CrossProduct ha) : (x * y).val = ((crossProductMul a) x.val) y.val

noncomputable instance GoodRep.CrossProduct.instOne {F K : Type} [Field K] [Field F] [Algebra F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : One (CrossProduct ha)

Equations

• GoodRep.CrossProduct.instOne ha = { one := { val := Pi.single 1 (↑(a (1, 1)))⁻¹ } }

@[simp]

theorem GoodRep.CrossProduct.one_val {F K : Type} [Field K] [Field F] [Algebra F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : val 1 = Pi.single 1 (↑(a (1, 1)))⁻¹

noncomputable instance GoodRep.CrossProduct.monoid {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : Monoid (CrossProduct ha)

Equations

• GoodRep.CrossProduct.monoid ha = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯

noncomputable instance GoodRep.CrossProduct.instRing {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : Ring (CrossProduct ha)

Equations

• GoodRep.CrossProduct.instRing ha = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable instance GoodRep.CrossProduct.instSMul {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : SMul F (CrossProduct ha)

Equations

• GoodRep.CrossProduct.instSMul ha = { smul := fun (r : F) (x : GoodRep.CrossProduct ha) => { val := (GoodRep.crossProductSMul r) x.val } }

@[simp]

theorem GoodRep.CrossProduct.smul_val {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (r : F) (x : CrossProduct ha) : (r • x).val = (crossProductSMul r) x.val

noncomputable instance GoodRep.CrossProduct.algebra {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : Algebra F (CrossProduct ha)

Equations

• GoodRep.CrossProduct.algebra ha = Algebra.mk { toFun := fun (r : F) => r • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

@[simp]

theorem GoodRep.CrossProduct.algebraMap_val {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (r : F) : (algebraMap F (CrossProduct ha)) r = r • 1

noncomputable def GoodRep.CrossProduct.ι {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : K →ₐ[F] CrossProduct ha

Equations

• GoodRep.CrossProduct.ι ha = { toFun := fun (b : K) => { val := Pi.single 1 (b * ↑(a (1, 1))⁻¹) }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem GoodRep.CrossProduct.ι_apply_val {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (b : K) : ((ι ha) b).val = Pi.single 1 (b * ↑(a (1, 1))⁻¹)

@[simp]

theorem GoodRep.CrossProduct.a_one_left {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ : K ≃ₐ[F] K) : a (1, σ) = a 1

theorem GoodRep.CrossProduct.a_one_right {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ : K ≃ₐ[F] K) : a (σ, 1) = (Units.map ↑σ) (a 1)

theorem GoodRep.CrossProduct.a_one_right' {F K : Type} [Field K] [Field F] [Algebra F K] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ : K ≃ₐ[F] K) : ↑(a (σ, 1)) = σ ↑(a 1)

theorem GoodRep.CrossProduct.identity_double_cross {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ : K ≃ₐ[F] K) (b : K) : (ι ha) b * { val := Pi.single σ 1 } = { val := Pi.single σ b }

theorem GoodRep.CrossProduct.identity_double_cross' {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ : K ≃ₐ[F] K) (b c : K) : (ι ha) b * { val := Pi.single σ c } = { val := Pi.single σ (b * c) }

noncomputable def GoodRep.CrossProduct.Units.ofLeftRightInverse (G : Type u_1) [Monoid G] (a b c : G) (h : a * b = 1) (h' : c * a = 1) : Gˣ

Equations

• GoodRep.CrossProduct.Units.ofLeftRightInverse G a b c h h' = { val := a, inv := b, val_inv := h, inv_val := ⋯ }

@[simp]

theorem GoodRep.CrossProduct.Units.val_ofLeftRightInverse (G : Type u_1) [Monoid G] (a b c : G) (h : a * b = 1) (h' : c * a = 1) : ↑(ofLeftRightInverse G a b c h h') = a

@[simp]

theorem GoodRep.CrossProduct.Units.val_inv_ofLeftRightInverse (G : Type u_1) [Monoid G] (a b c : G) (h : a * b = 1) (h' : c * a = 1) : ↑(ofLeftRightInverse G a b c h h')⁻¹ = b

theorem GoodRep.CrossProduct.Units.ofLeftRightInverse_inv_eq1 (G : Type u_1) [Monoid G] (a b c : G) (h : a * b = 1) (h' : c * a = 1) : (ofLeftRightInverse G a b c h h').inv = b

theorem GoodRep.CrossProduct.Units.ofLeftRightInverse_inv_eq2 (G : Type u_1) [Monoid G] (a b c : G) (h : a * b = 1) (h' : c * a = 1) : (ofLeftRightInverse G a b c h h').inv = c

noncomputable def GoodRep.CrossProduct.x_ {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ : K ≃ₐ[F] K) : (CrossProduct ha)ˣ

Equations

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

@[simp]

theorem GoodRep.CrossProduct.x__val {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ : K ≃ₐ[F] K) : (↑(x_ ha σ)).val = Pi.single σ 1

theorem GoodRep.CrossProduct.x__inv {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ : K ≃ₐ[F] K) : (x_ ha σ).inv.val = Pi.single σ⁻¹ (σ⁻¹ (↑(a (σ, σ⁻¹))⁻¹ * ↑(a 1)⁻¹))

theorem GoodRep.CrossProduct.x__inv' {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ : K ≃ₐ[F] K) : (x_ ha σ).inv.val = Pi.single σ⁻¹ ↑((a (σ⁻¹, σ))⁻¹ * (a 1)⁻¹)

theorem GoodRep.CrossProduct.x__mul {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ τ : K ≃ₐ[F] K) : ↑(x_ ha σ) * ↑(x_ ha τ) = (ι ha) ↑(a (σ, τ)) * ↑(x_ ha (σ * τ))

theorem GoodRep.CrossProduct.x__conj {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ : K ≃ₐ[F] K) (c : K) : ↑(x_ ha σ) * (ι ha) c * ↑(x_ ha σ)⁻¹ = (ι ha) (σ c)

theorem GoodRep.CrossProduct.x__conj' {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ : K ≃ₐ[F] K) (c : K) : ↑(x_ ha σ) * (ι ha) c = (ι ha) (σ c) * ↑(x_ ha σ)

noncomputable instance GoodRep.CrossProduct.module {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : Module K (CrossProduct ha)

Equations

• GoodRep.CrossProduct.module ha = Module.mk ⋯ ⋯

theorem GoodRep.CrossProduct.smul_def {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (c : K) (x : CrossProduct ha) : c • x = (ι ha) c * x

theorem GoodRep.CrossProduct.smul_single {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (c d : K) (σ : K ≃ₐ[F] K) : c • { val := Pi.single σ d } = { val := Pi.single σ (c * d) }

noncomputable def GoodRep.CrossProduct.x_AsBasis {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : Basis (K ≃ₐ[F] K) K (CrossProduct ha)

Equations

• GoodRep.CrossProduct.x_AsBasis ha = Basis.mk ⋯ ⋯

instance GoodRep.CrossProduct.instIsScalarTower {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : IsScalarTower F K (CrossProduct ha)

@[simp]

theorem GoodRep.CrossProduct.x_AsBasis_apply {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ : K ≃ₐ[F] K) : (x_AsBasis ha) σ = { val := Pi.single σ 1 }

theorem GoodRep.CrossProduct.one_in_x_AsBasis {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : 1 = (a (1, 1))⁻¹ • (x_AsBasis ha) 1

theorem GoodRep.CrossProduct.single_in_xAsBasis {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (c : K) (σ : K ≃ₐ[F] K) : { val := Pi.single σ c } = c • (x_AsBasis ha) σ

theorem GoodRep.CrossProduct.mul_single_in_xAsBasis {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (c d : K) (σ τ : K ≃ₐ[F] K) : { val := Pi.single σ c } * { val := Pi.single τ d } = (c * σ d * ↑(a (σ, τ))) • (x_AsBasis ha) (σ * τ)

theorem GoodRep.CrossProduct.x_AsBasis_conj' {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ : K ≃ₐ[F] K) (c : K) : (x_AsBasis ha) σ * (ι ha) c = σ c • (x_AsBasis ha) σ

theorem GoodRep.CrossProduct.x_AsBasis_conj'' {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ : K ≃ₐ[F] K) (c : K) : (x_AsBasis ha) σ * (ι ha) c = (ι ha) (σ c) * (x_AsBasis ha) σ

theorem GoodRep.CrossProduct.dim_eq_square {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) [IsGalois F K] : Module.finrank F (CrossProduct ha) = Module.finrank F K ^ 2

theorem GoodRep.CrossProduct.one_def {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : 1 = (↑(a 1))⁻¹ • (x_AsBasis ha) 1

theorem GoodRep.CrossProduct.x__conj'' {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ : K ≃ₐ[F] K) (c : K) : (x_AsBasis ha) σ * (ι ha) c = σ c • (x_AsBasis ha) σ

theorem GoodRep.CrossProduct.x_AsBasis_mul {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) (σ τ : K ≃ₐ[F] K) : (x_AsBasis ha) σ * (x_AsBasis ha) τ = ↑(a (σ, τ)) • (x_AsBasis ha) (σ * τ)

theorem GoodRep.CrossProduct.is_central {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) [IsGalois F K] : Subalgebra.center F (CrossProduct ha) ≤ ⊥

instance GoodRep.CrossProduct.instNontrivial {F K : Type} [Field K] [Field F] [Algebra F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : Nontrivial (CrossProduct ha)

noncomputable def GoodRep.CrossProduct.is_simple_proofs.π {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) : CrossProduct ha →+* I.ringCon.Quotient

Equations

• GoodRep.CrossProduct.is_simple_proofs.π I = I.ringCon.mk'

noncomputable def GoodRep.CrossProduct.is_simple_proofs.πRes {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) : ↥(ι ha).range →+* I.ringCon.Quotient

Equations

• GoodRep.CrossProduct.is_simple_proofs.πRes I = (GoodRep.CrossProduct.is_simple_proofs.π I).domRestrict (GoodRep.CrossProduct.ι ha).range

noncomputable def GoodRep.CrossProduct.is_simple_proofs.x {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} {I : TwoSidedIdeal (CrossProduct ha)} : ↥(πRes I).range → K

Equations

• GoodRep.CrossProduct.is_simple_proofs.x x = Exists.choose ⋯

theorem GoodRep.CrossProduct.is_simple_proofs.hx {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) (a✝ : ↥(πRes I).range) : (πRes I) ⟨(ι ha) (x a✝), ⋯⟩ = ↑a✝

theorem GoodRep.CrossProduct.is_simple_proofs.hx' {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) (a✝ : K) : (πRes I) ⟨(ι ha) a✝, ⋯⟩ = I.ringCon.mk' ((ι ha) a✝)

theorem GoodRep.CrossProduct.is_simple_proofs.x_wd {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) (c c' : K) (eq : (πRes I) ⟨(ι ha) c, ⋯⟩ = (πRes I) ⟨(ι ha) c', ⋯⟩) (y : CrossProduct ha) : (c - c') • y ∈ I

@[instance 10000]

noncomputable instance GoodRep.CrossProduct.is_simple_proofs.instSMulSubtypeQuotientRingConMemSubringRangeSubalgebraRangeιπRes {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) : SMul (↥(πRes I).range) I.ringCon.Quotient

Equations

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

theorem GoodRep.CrossProduct.is_simple_proofs.smul_def_quot {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) (a✝ : ↥(πRes I).range) (y : CrossProduct ha) : a✝ • I.ringCon.mk' y = Quotient.mk'' (x a✝ • y)

theorem GoodRep.CrossProduct.is_simple_proofs.smul_def_quot' {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) (a✝ : K) (y : CrossProduct ha) : ⟨(π I) ((ι ha) a✝), ⋯⟩ • I.ringCon.mk' y = I.ringCon.mk' (a✝ • y)

theorem GoodRep.CrossProduct.is_simple_proofs.smul_def_quot'' {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) (a✝ : K) (y : CrossProduct ha) : ⟨(π I) ((ι ha) a✝), ⋯⟩ • Quotient.mk'' y = Quotient.mk'' (a✝ • y)

noncomputable instance GoodRep.CrossProduct.is_simple_proofs.instModuleSubtypeQuotientRingConMemSubringRangeSubalgebraRangeιπRes {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) : Module (↥(πRes I).range) I.ringCon.Quotient

Equations

• GoodRep.CrossProduct.is_simple_proofs.instModuleSubtypeQuotientRingConMemSubringRangeSubalgebraRangeιπRes I = Module.mk ⋯ ⋯

noncomputable instance GoodRep.CrossProduct.is_simple_proofs.instModuleQuotientRingCon {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) : Module K I.ringCon.Quotient

Equations

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

theorem GoodRep.CrossProduct.is_simple_proofs.K_smul_quot {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) (c : K) (x : I.ringCon.Quotient) : c • x = ⟨(π I) ((ι ha) c), ⋯⟩ • x

noncomputable def GoodRep.CrossProduct.is_simple_proofs.basis {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) (ne_top : I ≠ ⊤) : Basis (K ≃ₐ[F] K) K I.ringCon.Quotient

Equations

• GoodRep.CrossProduct.is_simple_proofs.basis I ne_top = Basis.mk ⋯ ⋯

noncomputable def GoodRep.CrossProduct.is_simple_proofs.π₁ {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) (ne_top : I ≠ ⊤) : CrossProduct ha ≃ₗ[K] I.ringCon.Quotient

Equations

• GoodRep.CrossProduct.is_simple_proofs.π₁ I ne_top = (GoodRep.CrossProduct.x_AsBasis ha).equiv (GoodRep.CrossProduct.is_simple_proofs.basis I ne_top) (Equiv.refl (K ≃ₐ[F] K))

noncomputable def GoodRep.CrossProduct.is_simple_proofs.π₂ {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) : CrossProduct ha →ₗ[K] I.ringCon.Quotient

Equations

• GoodRep.CrossProduct.is_simple_proofs.π₂ I = { toFun := (↑↑(GoodRep.CrossProduct.is_simple_proofs.π I)).toFun, map_add' := ⋯, map_smul' := ⋯ }

theorem GoodRep.CrossProduct.is_simple_proofs.equal {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) (ne_top : I ≠ ⊤) : ↑(π₁ I ne_top) = π₂ I

theorem GoodRep.CrossProduct.is_simple_proofs.π_inj {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} {ha : groupCohomology.IsMulTwoCocycle a} (I : TwoSidedIdeal (CrossProduct ha)) (ne_top : I ≠ ⊤) : Function.Injective ⇑(π I)

instance GoodRep.CrossProduct.is_simple {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) : IsSimpleRing (CrossProduct ha)

instance GoodRep.CrossProduct.instIsCentralOfIsGalois {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) [IsGalois F K] : Algebra.IsCentral F (CrossProduct ha)

instance GoodRep.CrossProduct.instFiniteDimensionalOfIsGalois {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) [IsGalois F K] : FiniteDimensional F (CrossProduct ha)

noncomputable def GoodRep.CrossProduct.asCSA {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] {a : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (ha : groupCohomology.IsMulTwoCocycle a) [IsGalois F K] : CSA F

Equations

• GoodRep.CrossProduct.asCSA ha = CSA.mk (GoodRep.CrossProduct ha)

noncomputable def RelativeBrGroup.fromTwoCocycles {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] [DecidableEq (K ≃ₐ[F] K)] (a : ↥(groupCohomology.twoCocycles (galAct F K))) : ↥(RelativeBrGroup K F)

Equations

• RelativeBrGroup.fromTwoCocycles a = ⟨Quotient.mk'' (CSA.mk (GoodRep.CrossProduct.asCSA ⋯).carrier), ⋯⟩

noncomputable def RelativeBrGroup.fromSnd (F K : Type) [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] [DecidableEq (K ≃ₐ[F] K)] : groupCohomology.H2 (galAct F K) → ↥(RelativeBrGroup K F)

Equations

• RelativeBrGroup.fromSnd F K = Quotient.lift RelativeBrGroup.fromTwoCocycles ⋯

theorem RelativeBrGroup.fromSnd_wd {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] [DecidableEq (K ≃ₐ[F] K)] (a : ↥(groupCohomology.twoCocycles (galAct F K))) : fromSnd F K (Quotient.mk'' a) = ⟨Quotient.mk'' (GoodRep.CrossProduct.asCSA ⋯), ⋯⟩

theorem RelativeBrGroup.toSnd_fromSnd {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] [DecidableEq (K ≃ₐ[F] K)] : toSnd ∘ fromSnd F K = id

theorem RelativeBrGroup.fromSnd_toSnd {F K : Type} [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] [DecidableEq (K ≃ₐ[F] K)] : fromSnd F K ∘ toSnd = id

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

Equations

• RelativeBrGroup.equivSnd = { toFun := RelativeBrGroup.toSnd, invFun := RelativeBrGroup.fromSnd F K, left_inv := ⋯, right_inv := ⋯ }